diff --git a/src/spatialcf/adapters/ai2thor/adapter.py b/src/spatialcf/adapters/ai2thor/adapter.py index cf7de90..41da767 100644 --- a/src/spatialcf/adapters/ai2thor/adapter.py +++ b/src/spatialcf/adapters/ai2thor/adapter.py @@ -173,9 +173,13 @@ def _normalized_protocol_error( if isinstance(error, AdapterSettlementTimeout): return error origin = error.__cause__ if isinstance(error.__cause__, Exception) else error - if isinstance(origin, AI2ThorNativeReturnError): + if isinstance(error, AI2ThorNativeReturnError) or isinstance( + origin, AI2ThorNativeReturnError + ): + native_error = error if isinstance(error, AI2ThorNativeReturnError) else origin + assert isinstance(native_error, AI2ThorNativeReturnError) return AdapterReturnRejected( - f"{type(origin).__name__}:{' '.join(str(origin).split())}" + f"{type(native_error).__name__}:{' '.join(str(native_error).split())}" ) event = adapter._latest_event metadata = getattr(event, "metadata", None) @@ -281,6 +285,7 @@ def _apply_certified_edit_observed( ai2thor_spawn_map_from_adapter(application.spawn_map), x=subject.position.x + application.edit.translation_xy_m.x, y=subject.position.y + application.edit.translation_xy_m.y, + _defer_subject_pose_validation=True, ) applied = applied_certified_edit_from_native(native, application=application) except AI2ThorSettlementTimeout as error: diff --git a/src/spatialcf/adapters/ai2thor/execution.py b/src/spatialcf/adapters/ai2thor/execution.py index 7b8189c..6aeed1b 100644 --- a/src/spatialcf/adapters/ai2thor/execution.py +++ b/src/spatialcf/adapters/ai2thor/execution.py @@ -682,6 +682,7 @@ def _validate_returned_state( expected_positions: dict[str, Vec3], expected_rotations: dict[str, dict[str, float]], *, + deferred_pose_name: str | None = None, total_position_residual_limits_by_name: Mapping[str, float] | None = None, rotation_residual_limits_by_name: Mapping[str, float] | None = None, ) -> None: @@ -699,6 +700,12 @@ def _validate_returned_state( raise AI2ThorNativeReturnError( "stable object names changed during pose application" ) + if deferred_pose_name is not None and ( + deferred_pose_name not in expected_by_name + or deferred_pose_name not in expected_positions + or deferred_pose_name not in expected_rotations + ): + raise ValueError("deferred pose name is not an expected stable object") for name in expected_by_name: metadata = by_name[name] try: @@ -710,6 +717,18 @@ def _validate_returned_state( raise AI2ThorNativeReturnError( f"object {name!r} returned an invalid pose" ) from exc + if not all( + math.isfinite(value) + for value in ( + position.x, + position.y, + position.z, + *native_rotation.values(), + ) + ): + raise AI2ThorNativeReturnError( + f"object {name!r} returned an invalid pose" + ) expected_position = expected_positions[name] expected_rotation = expected_rotations[name] expected_coordinates = ( @@ -747,6 +766,8 @@ def _validate_returned_state( _OBJECT_ROTATION_TOLERANCE_DEGREES, ) ) + if name == deferred_pose_name: + continue if not position_matches or not all( self._angles_close( native_rotation[axis], @@ -960,6 +981,7 @@ def apply_receptacle_endpoint_observed( *, x: float, y: float, + _defer_subject_pose_validation: bool = False, ) -> AI2ThorPoseApplication: """Audit one exact world-XY endpoint without snapping or searching. @@ -989,6 +1011,7 @@ def apply_receptacle_endpoint_observed( y=next(iter(native_heights)), z=endpoint_y, ), + deferred_pose_name=(subject.name if _defer_subject_pose_validation else None), ) def apply_receptacle_endpoint_settled_observed( @@ -1080,6 +1103,7 @@ def _apply_receptacle_native_position_observed( *, max_pass_steps: int | None = None, max_subject_rotation_residual_degrees: float | None = None, + deferred_pose_name: str | None = None, ) -> AI2ThorPoseApplication: controller = self._require_active() commanded_position = Vec3( @@ -1129,6 +1153,7 @@ def _apply_receptacle_native_position_observed( event, expected_positions, expected_rotations, + deferred_pose_name=deferred_pose_name, ) else: immediate_native = self._scene_from_event(scene.scene_id, event) diff --git a/src/spatialcf/core/backends.py b/src/spatialcf/core/backends.py new file mode 100644 index 0000000..a759526 --- /dev/null +++ b/src/spatialcf/core/backends.py @@ -0,0 +1,579 @@ +"""Pure capability matching and protocol declarations for M1 backends. + +This module deliberately contains no backend discovery, compilation, solving, +or proof checking. It works only over records supplied by the caller. +""" + +from __future__ import annotations + +from typing import Protocol, runtime_checkable + +from spatialcf.domain.counterfactual import CounterfactualSolveRequest +from spatialcf.domain.definitions import ( + HashBoundCanonicalModel, + ValueKind, + canonical_json_bytes, +) +from spatialcf.domain.operators import OperatorDefinition +from spatialcf.domain.outcomes import ( + BackendProposal, + CapabilityMatch, + CapabilityMismatch, + TypedCompilationOutcome, +) +from spatialcf.domain.predicates import PredicateDefinition +from spatialcf.domain.profiles import ( + ActionSpaceProfile, + CounterfactualSolverConfig, + SemanticsProfile, + SolverBackendDescriptor, +) +from spatialcf.domain.serialization import canonical_sha256 + +__all__ = ( + "CompiledProblemProtocol", + "SolverBackendProtocol", + "match_backend_capabilities", + "order_backend_matches", +) + +_MISMATCH_ORDER = ( + "profile", + "predicate", + "operator", + "objective", + "numeric", + "proof", + "resource", + "backend", +) + +_PROOF_MATERIAL_ROLE = "definition-kind:proof-material" +_CERTIFIED_SOLUTION_ROLE = "definition-kind:claim-certified-solution" +_PROVEN_UNSAT_ROLE = "definition-kind:claim-proven-unsat" +_ROUTING_POLICY_ROLE = "definition-kind:routing-policy" +_ROUTING_MATCH_ROLE = "definition-kind:routing-match" +_ROUTING_MISMATCH_ROLE = "definition-kind:routing-mismatch" +_RECORD_BINDING_ROLE = "definition-kind:record-binding" +_RECORD_KIND_FIELD = "field:definition-kind" +_RECORD_REFERENCE_FIELD = "field:definition-reference" +_RECORD_BOUND_REFERENCE_FIELD = "field:bound-record-ref" +_RECORD_BOUND_SHA256_FIELD = "field:bound-record-sha256" +_ROUTING_MATCH_CLAIM_FIELD = "field:routing-match-claim" +_ROUTING_MISMATCH_CLAIM_FIELD = "field:routing-mismatch-claim" +_CLAIM_PROOF_MATERIAL_FIELD = "field:claim-proof-material-definition" + + +@runtime_checkable +class CompiledProblemProtocol(Protocol): + """The minimal hash-only product passed from compile to solve.""" + + @property + def semantic_problem_sha256(self) -> str: ... + + @property + def solve_request_sha256(self) -> str: ... + + @property + def selected_backend_descriptor_sha256(self) -> str: ... + + @property + def grounded_obligation_set_sha256(self) -> str: ... + + @property + def compiled_artifact_sha256s(self) -> tuple[str, ...]: ... + + +@runtime_checkable +class SolverBackendProtocol(Protocol): + """A declaration-only backend boundary; concrete solving lives elsewhere.""" + + def inspect( + self, + solve_request: CounterfactualSolveRequest, + ) -> CapabilityMatch | CapabilityMismatch: ... + + def compile( + self, + solve_request: CounterfactualSolveRequest, + ) -> CompiledProblemProtocol | TypedCompilationOutcome: ... + + def solve( + self, + compiled: CompiledProblemProtocol, + config: CounterfactualSolverConfig, + ) -> BackendProposal: ... + + +def _self_digest_matches(model: HashBoundCanonicalModel) -> bool: + """Check a submitted hash-bound record without reconstructing it.""" + + digest_field = model.SELF_DIGEST_FIELD + payload = model.model_dump( + mode="python", + by_alias=True, + exclude={digest_field}, + exclude_none=False, + exclude_defaults=False, + exclude_unset=False, + exclude_computed_fields=True, + round_trip=True, + ) + return getattr(model, digest_field) == canonical_sha256( + payload, + domain=model.HASH_DOMAIN, + ) + + +def _sorted_capabilities(values: set[str]) -> tuple[str, ...]: + return tuple(sorted(values, key=canonical_json_bytes)) + + +def _missing_capability(reason: str, value: str) -> str: + """Emit a canonical capability row even when the missing thing is a hash.""" + + digest = canonical_sha256( + (reason, value), + domain="spatialcf/counterfactual/backend-capability-mismatch/3.0", + ) + return f"capability:spatialcf/counterfactual/mismatch/{reason}/{digest}" + + +def _required_predicate_capabilities( + profile: ActionSpaceProfile, + definitions: tuple[PredicateDefinition, ...], +) -> set[str]: + required = set(profile.predicate_capability_refs) + for definition in definitions: + required.add(definition.evaluator_capability_ref) + required.add(definition.verifier_capability_ref) + return required + + +def _required_operator_capabilities( + definitions: tuple[OperatorDefinition, ...], +) -> set[str]: + required: set[str] = set() + for definition in definitions: + required.add(definition.compiler_capability_ref) + required.add(definition.verifier_capability_ref) + return required + + +def _definition_record_role(definition) -> str | None: + """Return a typed-record role, never a semantic inference from an ID.""" + + payload = definition.payload.payload + if payload.kind is not ValueKind.RECORD: + return None + fields = {field.name: field.value.payload for field in payload.fields} + role = fields.get(_RECORD_KIND_FIELD) + identity = fields.get(_RECORD_REFERENCE_FIELD) + if ( + role is None + or role.kind is not ValueKind.ENUM_SYMBOL + or identity is None + or identity.kind is not ValueKind.CANONICAL_ID + or identity.value != definition.definition_ref + ): + return None + return role.symbol + + +def _definition_record_reference(definition, field_name: str) -> str: + """Resolve one explicit reference from a closed definition payload.""" + + payload = definition.payload.payload + if payload.kind is not ValueKind.RECORD: + raise ValueError("definition metadata is not a typed record") + fields = {field.name: field.value.payload for field in payload.fields} + value = fields.get(field_name) + if value is None or value.kind is not ValueKind.CANONICAL_ID: + raise ValueError("definition metadata reference is missing") + return value.value + + +def _definition_record_digest(definition, field_name: str) -> str: + """Resolve one explicit digest from a typed definition record.""" + + payload = definition.payload.payload + if payload.kind is not ValueKind.RECORD: + raise ValueError("definition metadata is not a typed record") + fields = {field.name: field.value.payload for field in payload.fields} + value = fields.get(field_name) + if value is None or value.kind is not ValueKind.DIGEST: + raise ValueError("definition metadata digest is missing") + return value.value + + +def _frozen_definitions( + solve_request: CounterfactualSolveRequest, +) -> dict[str, object]: + """Combine the two explicit roots without allowing one to override another.""" + + definitions: dict[str, object] = {} + for definition in ( + *solve_request.semantic_problem.definition_bundle.definitions, + *solve_request.solve_policy_definition_bundle.definitions, + ): + existing = definitions.get(definition.definition_ref) + if existing is not None: + if canonical_json_bytes(existing) != canonical_json_bytes(definition): + raise ValueError("frozen definition roots conflict") + raise ValueError("frozen definition roots overlap") + definitions[definition.definition_ref] = definition + return definitions + + +def _solve_policy_definitions( + solve_request: CounterfactualSolveRequest, +) -> dict[str, object]: + """Compatibility name for the request's explicit combined closure.""" + + return _frozen_definitions(solve_request) + + +def _frozen_definition_bindings( + solve_request: CounterfactualSolveRequest, +) -> dict[str, str]: + """Return exact record digests declared by the request semantic root.""" + + definitions = { + definition.definition_ref: definition + for definition in solve_request.semantic_problem.definition_bundle.definitions + } + bindings: dict[str, str] = {} + for definition in definitions.values(): + if _definition_record_role(definition) != _RECORD_BINDING_ROLE: + continue + reference = _definition_record_reference( + definition, + _RECORD_BOUND_REFERENCE_FIELD, + ) + digest = _definition_record_digest( + definition, + _RECORD_BOUND_SHA256_FIELD, + ) + if reference in bindings and bindings[reference] != digest: + raise ValueError("frozen definition bindings conflict") + bindings[reference] = digest + return bindings + + +def _required_proof_material_definitions( + solve_request: CounterfactualSolveRequest, + action_space_profile: ActionSpaceProfile, +) -> set[str]: + definitions = _solve_policy_definitions(solve_request) + accepted_claims = set(solve_request.proof_policy.accepted_claim_definition_refs) + if not accepted_claims <= set(action_space_profile.allowed_claim_definition_refs): + raise ValueError("proof policy claims do not match the frozen profile") + proof_definitions: set[str] = set() + for claim_ref in accepted_claims: + claim = definitions.get(claim_ref) + if claim is None or _definition_record_role(claim) not in { + _CERTIFIED_SOLUTION_ROLE, + _PROVEN_UNSAT_ROLE, + }: + raise ValueError("accepted claim does not have typed proof semantics") + proof_ref = _definition_record_reference(claim, _CLAIM_PROOF_MATERIAL_FIELD) + proof = definitions.get(proof_ref) + if proof is None or _definition_record_role(proof) != _PROOF_MATERIAL_ROLE: + raise ValueError("accepted claim proof material is not closed") + proof_definitions.add(proof_ref) + return proof_definitions + + +def _routing_claim_refs( + solve_request: CounterfactualSolveRequest, +) -> tuple[str, str]: + """Bind success/failure claims to the request's frozen routing policy.""" + + routing = solve_request.backend_routing_policy + definitions = _solve_policy_definitions(solve_request) + definition = definitions.get(routing.routing_policy_ref) + if ( + definition is None + or _definition_record_role(definition) != _ROUTING_POLICY_ROLE + ): + raise ValueError("routing policy metadata is not closed") + match_ref = _definition_record_reference(definition, _ROUTING_MATCH_CLAIM_FIELD) + mismatch_ref = _definition_record_reference( + definition, + _ROUTING_MISMATCH_CLAIM_FIELD, + ) + match_definition = definitions.get(match_ref) + mismatch_definition = definitions.get(mismatch_ref) + if ( + match_definition is None + or mismatch_definition is None + or _definition_record_role(match_definition) != _ROUTING_MATCH_ROLE + or _definition_record_role(mismatch_definition) != _ROUTING_MISMATCH_ROLE + ): + raise ValueError("routing claim definitions do not have typed routing roles") + return match_ref, mismatch_ref + + +def _require_frozen_match_inputs( + solve_request: CounterfactualSolveRequest, + action_space_profile: ActionSpaceProfile, + semantics_profile: SemanticsProfile, + predicate_definitions: tuple[PredicateDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], +) -> None: + """Bind matcher inputs to the supplied request before comparing support.""" + + problem = solve_request.semantic_problem + if solve_request.semantic_problem_sha256 != problem.semantic_problem_sha256: + raise ValueError("shared roots do not match the embedded semantic problem") + records = ( + solve_request, + problem, + solve_request.implementation_registry_snapshot, + solve_request.backend_descriptor_bundle, + solve_request.backend_routing_policy, + solve_request.proof_policy, + solve_request.resource_policy, + action_space_profile, + semantics_profile, + *predicate_definitions, + *operator_definitions, + ) + if any(not _self_digest_matches(record) for record in records): + raise ValueError("frozen matcher input hash") + if ( + action_space_profile.action_space_profile_ref + != problem.action_space_profile_ref + or semantics_profile.semantics_profile_ref != problem.semantics_profile_ref + or action_space_profile.numeric_semantics_ref != problem.numeric_semantics_ref + or semantics_profile.numeric_semantics_ref != problem.numeric_semantics_ref + ): + raise ValueError("profile roots do not match the frozen semantic problem") + profile_bindings = _frozen_definition_bindings(solve_request) + if ( + profile_bindings.get(semantics_profile.semantics_profile_ref) + != semantics_profile.semantics_profile_sha256 + or profile_bindings.get(action_space_profile.action_space_profile_ref) + != action_space_profile.action_space_profile_sha256 + ): + raise ValueError("profile hashes do not match the frozen definition binding") + if {definition.predicate_ref for definition in predicate_definitions} != set( + semantics_profile.predicate_definition_refs + ): + raise ValueError("predicate definitions do not match the frozen profile") + if {definition.operator_ref for definition in operator_definitions} != set( + action_space_profile.allowed_operator_refs + ): + raise ValueError("operator definitions do not match the frozen profile") + definition_refs = set(_frozen_definitions(solve_request)) + if not set(_routing_claim_refs(solve_request)) <= definition_refs: + raise ValueError("routing definitions do not match the frozen policy") + + +def _backend_requirements_for_descriptor_build( + solve_request: CounterfactualSolveRequest, + action_space_profile: ActionSpaceProfile, + descriptor: SolverBackendDescriptor, +) -> tuple[set[str], set[str], set[str]]: + """Partition requirements into this build, another build, and unresolved rows.""" + + snapshot = solve_request.implementation_registry_snapshot + owner_by_capability = { + binding.definition_or_capability_ref: binding.implementation_owner_ref + for binding in snapshot.definition_and_capability_owner_bindings + if binding.definition_or_capability_ref.startswith("capability:") + } + build_by_owner = dict(snapshot.implementation_build_hashes) + matched_for_this_build: set[str] = set() + other_valid_build: set[str] = set() + structurally_unresolved: set[str] = set() + for capability in action_space_profile.backend_capability_requirements: + owner_ref = owner_by_capability.get(capability) + if owner_ref is None: + structurally_unresolved.add(capability) + continue + owner_build = build_by_owner.get(owner_ref) + if owner_build is None: + structurally_unresolved.add(capability) + elif owner_build == descriptor.implementation_build_sha256: + matched_for_this_build.add(capability) + else: + other_valid_build.add(capability) + return ( + matched_for_this_build, + other_valid_build, + structurally_unresolved, + ) + + +def match_backend_capabilities( + solve_request: CounterfactualSolveRequest, + action_space_profile: ActionSpaceProfile, + semantics_profile: SemanticsProfile, + predicate_definitions: tuple[PredicateDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], + descriptor: SolverBackendDescriptor, +) -> CapabilityMatch | CapabilityMismatch: + """Compare one descriptor against only the supplied frozen records. + + A non-support result is data, not control flow: all mismatch dimensions are + represented in the returned canonical row in the fixed order above. + """ + + _require_frozen_match_inputs( + solve_request, + action_space_profile, + semantics_profile, + predicate_definitions, + operator_definitions, + ) + match_claim, mismatch_claim = _routing_claim_refs(solve_request) + if not _self_digest_matches(descriptor): + return CapabilityMismatch( + backend_ref=descriptor.backend_ref, + backend_descriptor_sha256=descriptor.backend_descriptor_sha256, + missing_capability_refs=( + _missing_capability("descriptor", descriptor.backend_ref), + ), + reason_claim_definition_ref=mismatch_claim, + ) + + missing_by_reason: dict[str, set[str]] = {} + + if action_space_profile.action_space_profile_sha256 not in set( + descriptor.supported_profile_hashes + ): + missing_by_reason["profile"] = { + _missing_capability( + "profile", + action_space_profile.action_space_profile_sha256, + ) + } + + predicate_required = _required_predicate_capabilities( + action_space_profile, + predicate_definitions, + ) + predicate_missing = predicate_required - set( + descriptor.supported_predicate_capabilities + ) + if predicate_missing: + missing_by_reason["predicate"] = set(predicate_missing) + + operator_required = _required_operator_capabilities(operator_definitions) + operator_missing = operator_required - set( + descriptor.supported_operator_capabilities + ) + if operator_missing: + missing_by_reason["operator"] = set(operator_missing) + + objective_missing = set(action_space_profile.objective_capability_refs) - set( + descriptor.supported_objective_capabilities + ) + if objective_missing: + missing_by_reason["objective"] = set(objective_missing) + + numeric_required = { + semantics_profile.numeric_semantics_ref, + solve_request.semantic_problem.numeric_semantics_ref, + } + numeric_missing = numeric_required - set(descriptor.supported_numeric_semantics) + if numeric_missing: + missing_by_reason["numeric"] = { + _missing_capability("numeric", reference) for reference in numeric_missing + } + + proof_missing = set( + solve_request.proof_policy.required_checker_capability_refs + ) - set(descriptor.compatible_checker_capability_refs) + proof_definition_missing = _required_proof_material_definitions( + solve_request, + action_space_profile, + ) - set(descriptor.emitted_proof_material_definition_refs) + if proof_definition_missing: + proof_missing |= { + _missing_capability("proof-material", reference) + for reference in proof_definition_missing + } + if proof_missing: + missing_by_reason["proof"] = set(proof_missing) + + resource_missing = { + limit.definition_ref for limit in solve_request.resource_policy.limits + } - set(descriptor.resource_definition_refs) + if resource_missing: + missing_by_reason["resource"] = { + _missing_capability("resource", reference) for reference in resource_missing + } + + ( + matched_backend_requirements, + _other_valid_build_requirements, + structurally_unresolved_backend_requirements, + ) = _backend_requirements_for_descriptor_build( + solve_request, + action_space_profile, + descriptor, + ) + if not matched_backend_requirements: + missing_by_reason["backend"] = set( + action_space_profile.backend_capability_requirements + ) + elif structurally_unresolved_backend_requirements: + missing_by_reason["backend"] = set(structurally_unresolved_backend_requirements) + + registered = next( + ( + item + for item in solve_request.backend_descriptor_bundle.backend_descriptors + if item.backend_ref == descriptor.backend_ref + ), + None, + ) + if ( + registered is None + or registered.backend_descriptor_sha256 != descriptor.backend_descriptor_sha256 + or canonical_json_bytes(registered) != canonical_json_bytes(descriptor) + ): + missing_by_reason.setdefault("backend", set()).add( + _missing_capability("backend", descriptor.backend_ref) + ) + + if missing_by_reason: + return CapabilityMismatch( + backend_ref=descriptor.backend_ref, + backend_descriptor_sha256=descriptor.backend_descriptor_sha256, + missing_capability_refs=_sorted_capabilities( + { + capability + for reason_name in _MISMATCH_ORDER + for capability in missing_by_reason.get(reason_name, set()) + } + ), + reason_claim_definition_ref=mismatch_claim, + ) + + matched = ( + matched_backend_requirements + | predicate_required + | operator_required + | set(action_space_profile.objective_capability_refs) + | set(solve_request.proof_policy.required_checker_capability_refs) + ) + return CapabilityMatch( + backend_ref=descriptor.backend_ref, + backend_descriptor_sha256=descriptor.backend_descriptor_sha256, + matched_capability_refs=_sorted_capabilities(matched), + match_claim_definition_ref=match_claim, + ) + + +def order_backend_matches( + rows: tuple[CapabilityMatch | CapabilityMismatch, ...], +) -> tuple[CapabilityMatch | CapabilityMismatch, ...]: + """Return the one stable routing order without selecting a backend.""" + + backend_refs = tuple(row.backend_ref for row in rows) + if len(set(backend_refs)) != len(backend_refs): + raise ValueError("backend matches must not duplicate one backend") + return tuple(sorted(rows, key=lambda row: canonical_json_bytes(row.backend_ref))) diff --git a/src/spatialcf/core/registry.py b/src/spatialcf/core/registry.py new file mode 100644 index 0000000..db2f2cb --- /dev/null +++ b/src/spatialcf/core/registry.py @@ -0,0 +1,4187 @@ +"""Static, explicit cross-record validation for M1 counterfactual records. + +The registry is deliberately a closed composition-time object. It resolves +only the direct trusted objects supplied in :class:`StaticOwner` rows and never +loads a module, probes a machine, or performs a backend/checker operation. +""" + +from __future__ import annotations + +from dataclasses import dataclass + +from pydantic import BaseModel, TypeAdapter, ValidationError + +from spatialcf.domain.counterfactual import ( + CounterfactualProblemIR, + CounterfactualSolveRequest, + EditProgram, + SceneStateEnvelope, +) +from spatialcf.domain.definitions import ( + BOOTSTRAP_SCHEMA_SHA256, + CanonicalDefinitionEnvelope, + CapabilityRef, + DefinitionBundle, + HashBoundCanonicalModel, + TypedValue, + ValueKind, + ValueSchemaDefinition, + canonical_json_bytes, +) +from spatialcf.domain.operators import ( + DerivedFactRuleDefinition, + OperatorDefinition, + StateVariableDefinition, + StateVariableRef, + WriteAuthority, +) +from spatialcf.domain.outcomes import ( + BackendProposal, + BackendSelectionRecord, + CapabilityMatch, + CapabilityMismatch, + CertifiedSolutionCertificate, + CertifiedSolutionResult, + CheckedProofOutcome, + CheckerDisposition, + NoncertifiedWitnessResult, + ProofMaterialEnvelope, + ProvenUnsatCertificate, + ProvenUnsatResult, + ResourceUsage, + UnknownResult, + VerifierDispatchRecord, +) +from spatialcf.domain.predicates import ( + GroundedObligationSet, + PredicateAtom, + PredicateDefinition, +) +from spatialcf.domain.profiles import ( + ActionSpaceProfile, + BackendDescriptorBundle, + BackendRoutingPolicy, + CounterfactualSolverConfig, + ImplementationRegistrySnapshot, + InterventionAuthorization, + OwnerRef, + ProofPolicy, + ResourcePolicy, + SemanticsProfile, + SolverBackendDescriptor, +) +from spatialcf.domain.scene import CanonicalScene +from spatialcf.domain.serialization import canonical_sha256 + +__all__ = ( + "DefinitionClosureError", + "ImplementationResolutionError", + "SemanticContractError", + "StaticImplementationRegistry", + "StaticOwner", +) + +_UNCHANGED_LEAF_DOMAIN = "spatialcf/counterfactual/unchanged-leaves/3.0" +_FROZEN_LEAF_PATH_DOMAIN = "spatialcf/counterfactual/frozen-scene-leaf-path/3.0" +_EXTENSION_FACT_ADDRESS_DOMAIN = "spatialcf/counterfactual/extension-fact-address/3.0" +_ROLE_CERTIFIED_SOLUTION = "definition-kind:claim-certified-solution" +_ROLE_PROVEN_UNSAT = "definition-kind:claim-proven-unsat" +_ROLE_NONCERTIFIED_WITNESS = "definition-kind:claim-noncertified-witness" +_ROLE_UNKNOWN = "definition-kind:claim-unknown" +_ROLE_COMPLETE_DOMAIN = "definition-kind:complete-domain" +_ROLE_SOUND_COMPLETE_DOMAIN = "definition-kind:sound-complete-domain" +_ROLE_PROOF_MATERIAL = "definition-kind:proof-material" +_ROLE_RECORD_BINDING = "definition-kind:record-binding" +_ROLE_RESOURCE_ACCOUNTING = "definition-kind:resource-accounting" +_ROLE_RESOURCE_POLICY = "definition-kind:resource-policy" +_ROLE_ROUTING_POLICY = "definition-kind:routing-policy" +_ROLE_ROUTING_MATCH = "definition-kind:routing-match" +_ROLE_ROUTING_MISMATCH = "definition-kind:routing-mismatch" +_ROLE_ROUTING_SELECTION_DISPOSITION = "definition-kind:routing-selection-disposition" +_ROLE_ROUTING_SELECTION_REASON = "definition-kind:routing-selection-reason" +_MISMATCH_ORDER = ( + "profile", + "predicate", + "operator", + "objective", + "numeric", + "proof", + "resource", + "backend", +) +_RECORD_KIND_FIELD = "field:definition-kind" +_RECORD_REFERENCE_FIELD = "field:definition-reference" +_RECORD_BOUND_REFERENCE_FIELD = "field:bound-record-ref" +_RECORD_BOUND_SHA256_FIELD = "field:bound-record-sha256" +_STATE_SCHEMA_FIELD = "field:state-variable-schema" +_STATE_LEAF_SCHEMA_FIELD = "field:state-leaf-schema" +_STATE_FACT_FAMILY_FIELD = "field:state-fact-family" +_STATE_ENTITY_KEY_FIELD = "field:state-entity-key" +_STATE_FIELD_PATH_FIELD = "field:state-field-path" +_STATE_VALUE_SCHEMA_FIELD = "field:state-value-schema" +_STATE_FRAME_FIELD = "field:state-frame" +_STATE_UNIT_FIELD = "field:state-unit" +_STATE_TOPOLOGY_FIELD = "field:state-topology" +_PREREQUISITE_FACT_FAMILY_FIELD = "field:prerequisite-fact-family" +_OBJECTIVE_INPUT_SELECTOR_FIELD = "field:objective-input-selector" +_OBJECTIVE_UNIT_FIELD = "field:objective-unit" +_OBJECTIVE_NORMALIZATION_FIELD = "field:objective-normalization" +_PROOF_PAYLOAD_SCHEMA_FIELD = "field:proof-payload-schema" +_PROOF_CHECKER_CAPABILITY_FIELD = "field:proof-checker-capability" +_CLAIM_PROOF_MATERIAL_FIELD = "field:claim-proof-material-definition" +_CLAIM_CHECKER_CAPABILITY_FIELD = "field:claim-checker-capability" +_COMPLETE_DOMAIN_CLAIM_FIELD = "field:complete-domain-claim" +_ROUTING_MATCH_CLAIM_FIELD = "field:routing-match-claim" +_ROUTING_MISMATCH_CLAIM_FIELD = "field:routing-mismatch-claim" +_RESOURCE_ACCOUNTING_CLAIM_FIELD = "field:resource-accounting-claim" +_STATE_METADATA_FIELDS = ( + _STATE_SCHEMA_FIELD, + _STATE_LEAF_SCHEMA_FIELD, + _STATE_FACT_FAMILY_FIELD, + _STATE_ENTITY_KEY_FIELD, + _STATE_FIELD_PATH_FIELD, + _STATE_VALUE_SCHEMA_FIELD, +) +_OWNER_REF_ADAPTER = TypeAdapter(OwnerRef) +_CAPABILITY_REF_ADAPTER = TypeAdapter(CapabilityRef) + + +class DefinitionClosureError(ValueError): + """A definition, schema, canonical-byte, or typed-value closure failed.""" + + +class SemanticContractError(ValueError): + """A cross-record semantic, policy, program, or outcome contract failed.""" + + +class ImplementationResolutionError(ValueError): + """A supplied static owner, build, or capability binding did not resolve.""" + + +def _is_sha256(value: str) -> bool: + return len(value) == 64 and all( + character in "0123456789abcdef" for character in value + ) + + +def _ref_key(value: object) -> bytes: + return canonical_json_bytes(value) + + +def _state_key(value: StateVariableRef) -> bytes: + return canonical_json_bytes( + ( + value.state_schema_ref, + value.fact_family_ref, + value.entity_or_fact_key, + value.field_path_ref, + ) + ) + + +def _self_digest_matches(model: HashBoundCanonicalModel) -> bool: + field_name = model.SELF_DIGEST_FIELD + payload = model.model_dump( + mode="python", + by_alias=True, + exclude={field_name}, + exclude_none=False, + exclude_defaults=False, + exclude_unset=False, + exclude_computed_fields=True, + round_trip=True, + # Registry validators intentionally inspect already-decoded hostile + # wires. Pydantic's serializer warning is not a semantic verdict and + # must not prevent the closure checks below from rejecting the wire. + warnings=False, + ) + return getattr(model, field_name) == canonical_sha256( + payload, + domain=model.HASH_DOMAIN, + ) + + +def _walk_values(value: object): + """Yield closed values recursively without interpreting an open mapping.""" + + yield value + if isinstance(value, BaseModel): + for field_name in type(value).model_fields: + yield from _walk_values(getattr(value, field_name)) + elif isinstance(value, tuple | list | frozenset | set): + for item in value: + yield from _walk_values(item) + elif isinstance(value, dict): + for item in value.values(): + yield from _walk_values(item) + + +def _references(value: object, prefix: str) -> set[str]: + return { + item + for item in _walk_values(value) + if isinstance(item, str) and item.startswith(prefix) + } + + +def _schema_dependency_refs(schema: ValueSchemaDefinition) -> tuple[str, ...]: + """Return every schema edge declared by one immutable value schema.""" + + refs = [field.value_schema_ref for field in schema.fields] + for attribute in ( + "unit_schema_ref", + "dimension_schema_ref", + "frame_schema_ref", + "endpoint_schema_ref", + "element_schema_ref", + ): + reference = getattr(schema, attribute) + if reference is not None: + refs.append(reference) + return tuple(refs) + + +def _semantic_schema_definition_closure( + semantic_definitions: dict[str, CanonicalDefinitionEnvelope], + schemas: dict[str, ValueSchemaDefinition], + root_records: tuple[object, ...], +) -> set[str]: + """Resolve schema meaning from semantic wires, never from supplied schemas. + + A :class:`ValueSchemaDefinition` is an implementation-side record, not a + semantic root. Its own record-binding envelope therefore cannot establish + why it is present. Start at the submitted semantic records, follow only + non-binding semantic definition records, and then close the resulting + schema graph through each declared schema dependency. + """ + + roles = _definition_roles(semantic_definitions) + reachable_definitions: set[str] = set() + schema_refs: set[str] = set() + for record in root_records: + reachable_definitions.update( + reference + for reference in _references(record, "definition:") + if reference in semantic_definitions + ) + schema_refs.update(_references(record, "schema:")) + + while True: + before = len(reachable_definitions) + for reference in tuple(reachable_definitions): + if roles.get(reference) == _ROLE_RECORD_BINDING: + continue + definition = semantic_definitions[reference] + schema_refs.update(_references(definition, "schema:")) + reachable_definitions.update( + dependency + for dependency in ( + _definition_payload_dependency_refs(definition) + | {definition.definition_kind_ref} + ) + if dependency in semantic_definitions + ) + for reference, role in roles.items(): + if role not in {_ROLE_COMPLETE_DOMAIN, _ROLE_SOUND_COMPLETE_DOMAIN}: + continue + claim_ref = _definition_record_reference( + semantic_definitions[reference], + _COMPLETE_DOMAIN_CLAIM_FIELD, + ) + if claim_ref in reachable_definitions: + reachable_definitions.add(reference) + if len(reachable_definitions) == before: + break + + expected_schema_refs: set[str] = set() + pending_schema_refs = list(schema_refs) + while pending_schema_refs: + reference = pending_schema_refs.pop() + if reference in expected_schema_refs: + continue + schema = schemas.get(reference) + if schema is None: + raise DefinitionClosureError("schema reference") + expected_schema_refs.add(reference) + pending_schema_refs.extend(_schema_dependency_refs(schema)) + return expected_schema_refs + + +def _validate_typed_value( + value: TypedValue, + schemas: dict[str, ValueSchemaDefinition], +) -> None: + """Recursively validate a typed wire node against its exact schema graph. + + Pydantic validates the shape of each union member locally. This helper is + deliberately the cross-record half: it resolves every schema edge, rejects + record additions/omissions, and binds dimensional metadata to the declared + schema instead of trusting an opaque ``value_schema_ref`` label. + """ + + schema = schemas.get(value.value_schema_ref) + if schema is None: + raise DefinitionClosureError("typed value schema") + payload = value.payload + if schema.value_kind is not payload.kind: + raise DefinitionClosureError("typed value kind") + + if payload.kind is ValueKind.ENUM_SYMBOL: + if payload.symbol not in schema.enum_symbols: + raise DefinitionClosureError("enum symbol") + return + + if payload.kind is ValueKind.RECORD: + declared = {field.field_name: field for field in schema.fields} + supplied = {field.name: field.value for field in payload.fields} + if set(supplied) - set(declared): + raise DefinitionClosureError("record extra field") + missing = { + name + for name, field in declared.items() + if field.required and name not in supplied + } + if missing: + raise DefinitionClosureError("record required field") + for name, child in supplied.items(): + if child.value_schema_ref != declared[name].value_schema_ref: + raise DefinitionClosureError("record field schema") + _validate_typed_value(child, schemas) + return + + if ( + payload.kind + in { + ValueKind.LENGTH, + ValueKind.AREA, + ValueKind.ANGLE, + ValueKind.TIME, + ValueKind.PIXEL, + ValueKind.UNIT_INTERVAL, + } + and getattr(payload, "unit_schema_ref", None) != schema.unit_schema_ref + ): + raise DefinitionClosureError("typed value unit") + + if payload.kind in { + ValueKind.POINT_2D, + ValueKind.POINT_3D, + ValueKind.VECTOR_2D, + ValueKind.VECTOR_3D, + ValueKind.RIGID_POSE, + ValueKind.CLOSED_BOX, + }: + if ( + getattr(payload, "dimension_schema_ref", None) + != schema.dimension_schema_ref + ): + raise DefinitionClosureError("typed value dimension") + if getattr(payload, "frame_schema_ref", None) != schema.frame_schema_ref: + raise DefinitionClosureError("typed value frame") + + if payload.kind is ValueKind.INTERVAL: + if ( + payload.endpoint_schema_ref != schema.endpoint_schema_ref + or payload.lower_closed != schema.lower_closed + or payload.upper_closed != schema.upper_closed + ): + raise DefinitionClosureError("interval schema") + endpoint = schemas.get(payload.endpoint_schema_ref) + if endpoint is None: + raise DefinitionClosureError("schema reference") + if ( + endpoint.value_kind is not payload.lower.kind + or endpoint.value_kind is not payload.upper.kind + ): + raise DefinitionClosureError("interval endpoint schema") + # M1 intentionally represents interval endpoints through the closed + # ScalarPayload union. Validate each endpoint as its own typed value + # so enum membership and any future scalar closure are not bypassed by + # the enclosing interval record. + for endpoint_payload in (payload.lower, payload.upper): + _validate_typed_value( + TypedValue( + value_schema_ref=payload.endpoint_schema_ref, + payload=endpoint_payload, + ), + schemas, + ) + return + + if payload.kind in {ValueKind.FINITE_SET, ValueKind.FINITE_ORDERED_TUPLE}: + if payload.element_schema_ref != schema.element_schema_ref: + raise DefinitionClosureError("sequence element schema") + items = ( + payload.elements if payload.kind is ValueKind.FINITE_SET else payload.items + ) + if schema.min_cardinality is not None and len(items) < schema.min_cardinality: + raise DefinitionClosureError("sequence cardinality") + if schema.max_cardinality is not None and len(items) > schema.max_cardinality: + raise DefinitionClosureError("sequence cardinality") + for item in items: + if item.value_schema_ref != schema.element_schema_ref: + raise DefinitionClosureError("sequence element schema") + _validate_typed_value(item, schemas) + + +def _definition_record_fields( + definition: CanonicalDefinitionEnvelope, +) -> dict[str, object]: + """Return the scalar payloads of one closed typed definition record.""" + + payload = definition.payload.payload + if payload.kind is not ValueKind.RECORD: + raise DefinitionClosureError("definition record payload") + return {field.name: field.value.payload for field in payload.fields} + + +def _definition_record_reference( + definition: CanonicalDefinitionEnvelope, + field_name: str, +) -> str: + """Resolve one explicit canonical-reference field from a typed record.""" + + value = _definition_record_fields(definition).get(field_name) + if value is None or getattr(value, "kind", None) is not ValueKind.CANONICAL_ID: + raise DefinitionClosureError("definition record metadata") + return value.value + + +def _definition_record_digest( + definition: CanonicalDefinitionEnvelope, + field_name: str, +) -> str: + """Resolve one explicit digest field from a typed definition record.""" + + value = _definition_record_fields(definition).get(field_name) + if value is None or getattr(value, "kind", None) is not ValueKind.DIGEST: + raise DefinitionClosureError("definition record metadata") + return value.value + + +def _definition_record_role( + definition: CanonicalDefinitionEnvelope, +) -> str: + """Read an explicit typed definition-record role without parsing its ID.""" + + fields = _definition_record_fields(definition) + role_value = fields.get(_RECORD_KIND_FIELD) + identity_value = fields.get(_RECORD_REFERENCE_FIELD) + if ( + role_value is None + or role_value.kind is not ValueKind.ENUM_SYMBOL + or identity_value is None + or identity_value.kind is not ValueKind.CANONICAL_ID + or identity_value.value != definition.definition_ref + ): + raise DefinitionClosureError("definition record identity") + return role_value.symbol + + +def _definition_roles( + definitions: dict[str, CanonicalDefinitionEnvelope], +) -> dict[str, str]: + return { + reference: _definition_record_role(definition) + for reference, definition in definitions.items() + } + + +def _definition_payload_dependency_refs( + definition: CanonicalDefinitionEnvelope, +) -> set[str]: + """Return payload edges while excluding only its required record identity. + + A typed definition record necessarily names its own envelope in + ``field:definition-reference``. That one structural identity field is not + a dependency. A self reference anywhere else in the payload remains a + real cycle edge. + """ + + payload = definition.payload.payload + if payload.kind is not ValueKind.RECORD: + return _references(definition.payload, "definition:") + references: set[str] = set() + skipped_identity = False + for field in payload.fields: + field_payload = field.value.payload + if ( + not skipped_identity + and field.name == _RECORD_REFERENCE_FIELD + and field_payload.kind is ValueKind.CANONICAL_ID + and field_payload.value == definition.definition_ref + ): + skipped_identity = True + continue + references.update(_references(field.value, "definition:")) + return references + + +def _root_bootstrap_anchor( + definitions: dict[str, CanonicalDefinitionEnvelope], +) -> str | None: + """Identify the one root-local self-kind anchor used by typed envelopes.""" + + kind_counts: dict[str, int] = {} + for definition in definitions.values(): + kind_counts[definition.definition_kind_ref] = ( + kind_counts.get(definition.definition_kind_ref, 0) + 1 + ) + highest_count = max(kind_counts.values(), default=0) + candidates = tuple( + reference for reference, count in kind_counts.items() if count == highest_count + ) + if len(candidates) != 1: + return None + anchor = candidates[0] + anchor_definition = definitions.get(anchor) + if anchor_definition is None or anchor_definition.definition_kind_ref != anchor: + return None + return anchor + + +def _has_exact_root_bootstrap_shape( + definitions: dict[str, CanonicalDefinitionEnvelope], + anchor: str | None, +) -> bool: + """Require one self-kind anchor and no alternate envelope kind edge.""" + + return anchor is not None and all( + definition.definition_kind_ref == anchor for definition in definitions.values() + ) + + +def _definition_root_maps( + semantic_definition_bundle: DefinitionBundle, + solve_policy_definition_bundle: DefinitionBundle, +) -> tuple[ + dict[str, CanonicalDefinitionEnvelope], + dict[str, CanonicalDefinitionEnvelope], + dict[str, CanonicalDefinitionEnvelope], +]: + """Return the two explicit roots and their non-overriding union.""" + + semantic = { + definition.definition_ref: definition + for definition in semantic_definition_bundle.definitions + } + solve = { + definition.definition_ref: definition + for definition in solve_policy_definition_bundle.definitions + } + if semantic.keys() & solve.keys(): + raise DefinitionClosureError("definition bundle overlap") + return semantic, solve, semantic | solve + + +def _definition_record_bindings( + definitions: dict[str, CanonicalDefinitionEnvelope], + roles: dict[str, str], +) -> dict[str, str]: + """Read explicit record identity bindings from the frozen definition DAG.""" + + bindings: dict[str, str] = {} + for reference, role in roles.items(): + if role != _ROLE_RECORD_BINDING: + continue + definition = definitions[reference] + bound_reference = _definition_record_reference( + definition, + _RECORD_BOUND_REFERENCE_FIELD, + ) + bound_digest = _definition_record_digest( + definition, + _RECORD_BOUND_SHA256_FIELD, + ) + if bound_reference in bindings: + raise DefinitionClosureError("duplicate definition record binding") + bindings[bound_reference] = bound_digest + return bindings + + +def _validate_exact_root_definition_closure( + definitions: dict[str, CanonicalDefinitionEnvelope], + *, + root_records: tuple[object, ...], + record_binding_targets: set[str], + root_label: str, + include_complete_domain_dependents: bool = False, +) -> None: + """Require a bundle to be exactly reachable from explicit wire records. + + A definition bundle is an input container, not a source of its own + authority. The traversal starts at the submitted problem/profile/policy + records and their supplied specialized records; record-binding envelopes + become reachable only through the record identity they bind. In + particular, an otherwise well-formed generic envelope cannot make itself + reachable merely by being embedded in the bundle. + """ + + roles = _definition_roles(definitions) + binding_target_by_envelope = { + reference: _definition_record_reference( + definitions[reference], _RECORD_BOUND_REFERENCE_FIELD + ) + for reference, role in roles.items() + if role == _ROLE_RECORD_BINDING + } + explicit_targets = set(record_binding_targets) + for record in root_records: + explicit_targets.update(_references(record, "definition:")) + explicit_targets.update(_references(record, "schema:")) + + anchor = _root_bootstrap_anchor(definitions) + reachable = { + reference for reference in explicit_targets if reference in definitions + } + if anchor is not None: + reachable.add(anchor) + + while True: + before = len(reachable) + for reference in tuple(reachable): + definition = definitions[reference] + reachable.update( + dependency + for dependency in ( + _definition_payload_dependency_refs(definition) + | {definition.definition_kind_ref} + ) + if dependency in definitions + ) + reachable.update( + envelope_ref + for envelope_ref, target in binding_target_by_envelope.items() + if target in explicit_targets or target in reachable + ) + if include_complete_domain_dependents: + for reference, role in roles.items(): + if role not in {_ROLE_COMPLETE_DOMAIN, _ROLE_SOUND_COMPLETE_DOMAIN}: + continue + claim_ref = _definition_record_reference( + definitions[reference], _COMPLETE_DOMAIN_CLAIM_FIELD + ) + if claim_ref in explicit_targets or claim_ref in reachable: + reachable.add(reference) + if len(reachable) == before: + break + if set(definitions) != reachable: + raise DefinitionClosureError(f"unreachable {root_label} definition") + + +def _require_definition_role( + roles: dict[str, str], + reference: str, + *permitted: str, +) -> None: + if roles.get(reference) not in permitted: + raise DefinitionClosureError("definition record role") + + +def _require_outcome_definition_role( + roles: dict[str, str], + reference: str, + permitted: tuple[str, ...], + reason: str, +) -> None: + """Keep valid-but-inadmissible terminal claims in the outcome error family.""" + + if roles.get(reference) not in permitted: + raise SemanticContractError(reason) + + +def _validate_resource_usage( + usage: ResourceUsage, + resource_policy: ResourcePolicy, + definitions: dict[str, CanonicalDefinitionEnvelope], +) -> None: + """Bind every submitted accounting row to the frozen resource policy.""" + + policy_definition = definitions.get(resource_policy.resource_policy_ref) + if ( + policy_definition is None + or _definition_record_role(policy_definition) != _ROLE_RESOURCE_POLICY + ): + raise SemanticContractError("resource usage") + accounting_ref = _definition_record_reference( + policy_definition, + _RESOURCE_ACCOUNTING_CLAIM_FIELD, + ) + if ( + usage.accounting_claim_definition_ref != accounting_ref + or _definition_roles(definitions).get(accounting_ref) + != _ROLE_RESOURCE_ACCOUNTING + or {entry.resource_definition_ref for entry in usage.entries} + != {limit.definition_ref for limit in resource_policy.limits} + ): + raise SemanticContractError("resource usage") + limits_by_ref = { + limit.definition_ref: limit.finite_limit for limit in resource_policy.limits + } + if any( + entry.used > limits_by_ref[entry.resource_definition_ref] + for entry in usage.entries + ): + raise SemanticContractError("resource usage limit") + exhausted = any( + entry.used == limits_by_ref[entry.resource_definition_ref] + for entry in usage.entries + ) + if usage.exhausted != exhausted: + raise SemanticContractError("resource usage exhaustion") + + +def _state_definition_metadata( + definitions: dict[str, CanonicalDefinitionEnvelope], +) -> dict[str, tuple[str, str, str, str, str, str]]: + """Resolve schema-owned leaf addresses from typed state definition records.""" + + result: dict[str, tuple[str, str, str, str, str]] = {} + for definition_ref, definition in definitions.items(): + if _definition_record_role(definition) != "definition-kind:state-variable": + continue + payload = definition.payload.payload + assert payload.kind is ValueKind.RECORD + fields = {field.name: field.value.payload for field in payload.fields} + values: list[str] = [] + for field_name in _STATE_METADATA_FIELDS: + field = fields.get(field_name) + if field is None or field.kind is not ValueKind.CANONICAL_ID: + # Ordinary state definitions may remain shape-only, but they + # cannot own a submitted scene leaf until metadata is present. + break + values.append(field.value) + else: + result[definition_ref] = tuple(values) # type: ignore[assignment] + return result + + +def _state_definition_semantics( + definitions: dict[str, CanonicalDefinitionEnvelope], +) -> dict[str, tuple[str, str, str]]: + """Resolve the non-address state meaning carried by its typed record.""" + + result: dict[str, tuple[str, str, str]] = {} + for definition_ref, definition in definitions.items(): + if _definition_record_role(definition) != "definition-kind:state-variable": + continue + fields = _definition_record_fields(definition) + values: list[str] = [] + for field_name in ( + _STATE_FRAME_FIELD, + _STATE_UNIT_FIELD, + _STATE_TOPOLOGY_FIELD, + ): + field = fields.get(field_name) + if ( + field is None + or getattr(field, "kind", None) is not ValueKind.CANONICAL_ID + ): + break + values.append(field.value) + else: + result[definition_ref] = tuple(values) # type: ignore[assignment] + return result + + +def _raw_value_matches_schema(value: object, schema: ValueSchemaDefinition) -> bool: + """Check the frozen raw scene scalar against its declared leaf schema.""" + + if value is None: + return True + if schema.value_kind is ValueKind.BOOLEAN: + return isinstance(value, bool) + if schema.value_kind is ValueKind.INTEGER: + return isinstance(value, int) and not isinstance(value, bool) + if schema.value_kind is ValueKind.FINITE_REAL: + return isinstance(value, float) + if schema.value_kind is ValueKind.CANONICAL_ID: + return isinstance(value, str) + return False + + +def _validate_state_leaf_value_wires( + leaves: tuple[StateVariableRef, ...], + values: dict[bytes, object], + definitions_by_leaf: dict[bytes, StateVariableDefinition], + schemas: dict[str, ValueSchemaDefinition], + actual_extension_addresses: set[tuple[str, str]], + absent_extension_addresses: set[tuple[str, str]], +) -> None: + """Validate values by their exact base/extension ownership category. + + Frozen base leaves encode their canonical scene scalars directly. An + actually present extension fact, in contrast, must carry a ``TypedValue`` + on each non-presence leaf. A schema-declared but absent extension address + is the only place where the explicit ``None`` value sentinel is legal; + its presence leaf remains a raw boolean. Keeping this distinction here + makes the before, semantic, and after closures agree on the same wire. + """ + + for leaf in leaves: + key = _state_key(leaf) + state_definition = definitions_by_leaf.get(key) + if state_definition is None or key not in values: + raise DefinitionClosureError("state leaf value schema") + value = values[key] + owner = (leaf.fact_family_ref, leaf.entity_or_fact_key) + presence_leaf = leaf.field_path_ref.startswith("field-path:presence-") + + if owner in actual_extension_addresses and not presence_leaf: + if not isinstance(value, TypedValue): + raise DefinitionClosureError("state leaf value schema") + if value.value_schema_ref != state_definition.value_schema_ref: + raise DefinitionClosureError("state leaf value schema") + _validate_typed_value(value, schemas) + continue + + if owner in absent_extension_addresses and not presence_leaf: + if value is None: + continue + raise DefinitionClosureError("state leaf value schema") + + if isinstance(value, TypedValue): + if value.value_schema_ref != state_definition.value_schema_ref: + raise DefinitionClosureError("state leaf value schema") + _validate_typed_value(value, schemas) + continue + + schema = schemas.get(state_definition.value_schema_ref) + if schema is None or not _raw_value_matches_schema(value, schema): + raise DefinitionClosureError("state leaf value schema") + + +def _base_fact_rows(scene: object) -> tuple[tuple[str, str, object], ...]: + """Read the finite current scene as data, never through a runtime adapter.""" + + families = ( + ( + "definition:spatialcf/counterfactual/base-scene/objects/3.0", + "objects", + "object_id", + ), + ( + "definition:spatialcf/counterfactual/base-scene/geometry-instances/3.0", + "geometry_instances", + "geometry_id", + ), + ( + "definition:spatialcf/counterfactual/base-scene/collision-bodies/3.0", + "collision_bodies", + "body_id", + ), + ( + "definition:spatialcf/counterfactual/base-scene/workspace-boundaries/3.0", + "workspace_boundaries", + "fact_id", + ), + ( + "definition:spatialcf/counterfactual/base-scene/known-free-spaces/3.0", + "known_free_spaces", + "fact_id", + ), + ( + "definition:spatialcf/counterfactual/base-scene/support-surfaces/3.0", + "support_surfaces", + "surface_id", + ), + ( + "definition:spatialcf/counterfactual/base-scene/cameras/3.0", + "cameras", + "camera_id", + ), + ( + "definition:spatialcf/counterfactual/base-scene/baseline-observations/3.0", + "baseline_observations", + "observation_id", + ), + ) + rows: list[tuple[str, str, object]] = [] + for family, attribute, identifier in families: + fact_set = getattr(scene, attribute) + for values in (fact_set.values, fact_set.inner_values, fact_set.outer_values): + if values: + rows.extend( + (family, getattr(item, identifier), item) for item in values + ) + return tuple(rows) + + +def _frozen_scalar_values( + value: object, + path: tuple[str, ...] = (), +) -> tuple[tuple[tuple[str, ...], object], ...]: + """Flatten canonical facts into their actual scalar field leaves.""" + + if isinstance(value, BaseModel): + value = value.model_dump(mode="python") + if isinstance(value, dict): + return tuple( + item + for name, child in value.items() + for item in _frozen_scalar_values(child, (*path, str(name))) + ) + if isinstance(value, tuple | list): + return tuple( + item + for index, child in enumerate(value) + for item in _frozen_scalar_values(child, (*path, str(index))) + ) + if hasattr(value, "value") and type(value).__module__ != "builtins": + value = value.value + return ((path, value),) + + +def _frozen_leaf_token( + fact_family_ref: str, + entity_or_fact_key: str, + path: tuple[str, ...], +) -> str: + return canonical_sha256( + (fact_family_ref, entity_or_fact_key, path), + domain=_FROZEN_LEAF_PATH_DOMAIN, + ) + + +def _extension_fact_address( + fact_family_ref: str, + subject_entity_id: str, + fact_key: str, +) -> str: + """Derive the one state address for a full extension ownership triple. + + ``StateVariableRef`` intentionally has one canonical address field rather + than an open selector map. Extension facts therefore encode their full + ``(family, subject, key)`` ownership tuple into that field. A fact key + alone is not an ownership identity because the same key may occur for two + independently editable subjects. + """ + + return "fact-address:spatialcf/counterfactual/" + canonical_sha256( + (fact_family_ref, subject_entity_id, fact_key), + domain=_EXTENSION_FACT_ADDRESS_DOMAIN, + ) + + +def _extension_facts_by_address( + state: SceneStateEnvelope, +) -> dict[tuple[str, str], object]: + """Index extension facts by their derived address and reject a hash alias.""" + + facts: dict[tuple[str, str], object] = {} + ownership_by_address: dict[tuple[str, str], tuple[str, str, str]] = {} + for bundle in state.extension_fact_bundles: + for fact in bundle.facts: + address = _extension_fact_address( + fact.fact_family_ref, + fact.subject_entity_id, + fact.fact_key, + ) + key = (fact.fact_family_ref, address) + ownership = ( + fact.fact_family_ref, + fact.subject_entity_id, + fact.fact_key, + ) + previous = ownership_by_address.get(key) + if previous is not None and previous != ownership: + raise SemanticContractError("extension fact address") + if previous is not None: + raise SemanticContractError("extension fact address") + ownership_by_address[key] = ownership + facts[key] = fact + return facts + + +def _state_leaf_owners( + leaves: tuple[StateVariableRef, ...], +) -> dict[tuple[str, str], tuple[StateVariableRef, ...]]: + """Group the frozen state-index leaves by their complete fact address.""" + + owners: dict[tuple[str, str], tuple[StateVariableRef, ...]] = {} + for leaf in leaves: + address = (leaf.fact_family_ref, leaf.entity_or_fact_key) + owners[address] = owners.get(address, ()) + (leaf,) + return owners + + +def _declared_extension_leaf_owners( + leaves: tuple[StateVariableRef, ...], + base_owners: set[tuple[str, str]], +) -> dict[tuple[str, str], tuple[StateVariableRef, ...]]: + """Return schema-declared non-base fact addresses from the frozen index. + + A state schema owns the full extension address universe. A particular + scene can legitimately omit one of those facts, in which case its presence + leaf is false and its value leaf carries the explicit ``None`` absence + sentinel. The scene facts may therefore be a strict subset of this map; + facts outside it are never admitted. + """ + + return { + address: owned + for address, owned in _state_leaf_owners(leaves).items() + if address not in base_owners + } + + +def _expected_base_leaf_addresses(scene: object) -> set[tuple[str, str, str]]: + """Return the finite frozen base-scene leaf address universe. + + Canonical v2 fact identities are closed data. M1 adds an explicit + presence and value leaf for each fact; treating the index as a merely + non-empty collection would permit hidden state to alter a hash partition. + """ + + addresses: set[tuple[str, str, str]] = set() + for family, identifier, fact in _base_fact_rows(scene): + membership_token = _frozen_leaf_token( + family, + identifier, + ("membership",), + ) + addresses.add((family, identifier, f"field-path:presence-{membership_token}")) + addresses.update( + ( + family, + identifier, + f"field-path:{_frozen_leaf_token(family, identifier, path)}", + ) + for path, _value in _frozen_scalar_values(fact) + ) + return addresses + + +def _validated_base_scene_payload(payload: object) -> CanonicalScene: + """Return the exact, independently revalidated frozen base-scene contract. + + ``SceneStateEnvelope.model_construct`` can bypass the domain field + validator. A lookalike Pydantic model may serialize to the same bytes as + a scene while carrying a weaker schema, so byte equality alone is not a + substitute for the exact CanonicalScene type and its full validator. + """ + + if type(payload) is not CanonicalScene: + raise ValueError("base scene payload must be an exact CanonicalScene") + round_trip = CanonicalScene.model_validate( + payload.model_dump( + mode="python", + by_alias=True, + exclude_none=False, + exclude_defaults=False, + exclude_unset=False, + exclude_computed_fields=True, + round_trip=True, + ), + strict=True, + ) + if canonical_json_bytes(payload) != canonical_json_bytes(round_trip): + raise ValueError("base scene payload canonical round trip") + return round_trip + + +def _leaf_values( + state: SceneStateEnvelope, + base_scene: CanonicalScene, +) -> dict[bytes, object]: + base_values = { + (family, identifier, _frozen_leaf_token(family, identifier, path)): value + for family, identifier, fact in _base_fact_rows(base_scene) + for path, value in _frozen_scalar_values(fact) + } + base_owners = { + (family, identifier) + for family, identifier, _fact in _base_fact_rows(base_scene) + } + extension_values = { + address: fact.value + for address, fact in _extension_facts_by_address(state).items() + } + values: dict[bytes, object] = {} + for leaf in state.canonical_state_leaf_index.leaves: + key = _state_key(leaf) + owner = (leaf.fact_family_ref, leaf.entity_or_fact_key) + token = leaf.field_path_ref.removeprefix("field-path:presence-").removeprefix( + "field-path:" + ) + present = owner in base_owners or owner in extension_values + if leaf.field_path_ref.startswith("field-path:presence-"): + values[key] = present + elif owner in extension_values: + values[key] = extension_values[owner] + elif ( + leaf.fact_family_ref, + leaf.entity_or_fact_key, + token, + ) in base_values: + values[key] = base_values[ + (leaf.fact_family_ref, leaf.entity_or_fact_key, token) + ] + else: + # ``None`` is an explicit absence payload in the partition, never a + # silently fabricated presence bit. Its canonical encoding makes + # extension removals observable to the delta reconstruction. + values[key] = None + return values + + +def _validate_scene_state_envelope( + state: SceneStateEnvelope, + state_variable_definitions: tuple[StateVariableDefinition, ...], + value_schema_definitions: tuple[ValueSchemaDefinition, ...], + semantic_definitions: dict[str, CanonicalDefinitionEnvelope], + *, + after_state: bool, +) -> tuple[dict[bytes, StateVariableRef], dict[bytes, object], CanonicalScene]: + """Close one complete scene envelope without treating an index as opaque. + + The problem's frozen before scene and an edit program's after scene use the + same address universe and typed state definitions. They differ in values, + not in whether a nested bundle, base payload, entity index, or leaf index + is independently hash-bound and schema-owned. + """ + + def fail(detail: str) -> None: + raise SemanticContractError("complete after state" if after_state else detail) + + if not _self_digest_matches(state): + fail("scene state hash") + if not _self_digest_matches(state.canonical_state_leaf_index): + fail("state leaf index hash") + if any(not _self_digest_matches(bundle) for bundle in state.extension_fact_bundles): + fail("extension fact bundle hash") + try: + base_scene = _validated_base_scene_payload(state.base_scene_payload) + except (TypeError, ValidationError, ValueError) as error: + raise SemanticContractError( + "complete after state" if after_state else "base scene hash" + ) from error + if state.base_scene_sha256 != canonical_sha256( + base_scene, + domain="spatialcf/counterfactual/base-scene-payload/3.0", + ): + fail("base scene hash") + + expected_entities = { + identifier for _family, identifier, _value in _base_fact_rows(base_scene) + } | { + fact.subject_entity_id + for bundle in state.extension_fact_bundles + for fact in bundle.facts + } + if set(state.closed_entity_index) != expected_entities: + fail("complete scene entity index") + + leaves = state.canonical_state_leaf_index.leaves + leaf_keys = {_state_key(leaf) for leaf in leaves} + if len(leaf_keys) != len(leaves) or tuple(leaves) != tuple( + sorted(leaves, key=canonical_json_bytes) + ): + fail("exact state leaf index") + base_owners = { + (family, identifier) + for family, identifier, _fact in _base_fact_rows(base_scene) + } + extension_facts = _extension_facts_by_address(state) + base_addresses = { + (leaf.fact_family_ref, leaf.entity_or_fact_key, leaf.field_path_ref) + for leaf in leaves + if (leaf.fact_family_ref, leaf.entity_or_fact_key) in base_owners + } + if base_addresses != _expected_base_leaf_addresses(base_scene): + fail("exact state leaf index") + by_family_identifier = _state_leaf_owners(leaves) + for family, identifier, _value in _base_fact_rows(base_scene): + owned = by_family_identifier.get((family, identifier), ()) + if not any( + leaf.field_path_ref.startswith("field-path:presence-") for leaf in owned + ): + fail("complete state leaf presence") + if not any( + not leaf.field_path_ref.startswith("field-path:presence-") for leaf in owned + ): + fail("complete state leaf value") + + state_by_schema = { + definition.state_variable_schema_ref: definition + for definition in state_variable_definitions + } + state_by_ref = { + definition.state_variable_ref: definition + for definition in state_variable_definitions + } + if len(state_by_schema) != len(state_variable_definitions) or len( + state_by_ref + ) != len(state_variable_definitions): + fail("state leaf definition") + if any(leaf.state_variable_schema_ref not in state_by_schema for leaf in leaves): + fail("state leaf definition") + if not leaf_keys: + fail("complete state leaf index") + + metadata_by_ref = _state_definition_metadata(semantic_definitions) + if set(metadata_by_ref) != set(state_by_ref): + fail("schema-owned field path") + metadata_by_address: dict[ + tuple[str, str, str, str, str], StateVariableDefinition + ] = {} + for definition_ref, state_definition in state_by_ref.items(): + ( + state_variable_schema_ref, + state_schema_ref, + fact_family_ref, + entity_or_fact_key, + field_path_ref, + value_schema_ref, + ) = metadata_by_ref[definition_ref] + if ( + state_variable_schema_ref != state_definition.state_variable_schema_ref + or value_schema_ref != state_definition.value_schema_ref + ): + fail("schema-owned field path") + address = ( + state_variable_schema_ref, + state_schema_ref, + fact_family_ref, + entity_or_fact_key, + field_path_ref, + ) + if address in metadata_by_address: + fail("schema-owned field path") + metadata_by_address[address] = state_definition + leaf_by_address = { + ( + leaf.state_variable_schema_ref, + leaf.state_schema_ref, + leaf.fact_family_ref, + leaf.entity_or_fact_key, + leaf.field_path_ref, + ): leaf + for leaf in leaves + } + if len(leaf_by_address) != len(leaves) or set(leaf_by_address) != set( + metadata_by_address + ): + fail("schema-owned field path") + extension_leaf_owners = _declared_extension_leaf_owners(leaves, base_owners) + if not set(extension_facts) <= set(extension_leaf_owners): + fail("extension fact address") + for owned in extension_leaf_owners.values(): + if ( + len(owned) != 2 + or sum( + leaf.field_path_ref.startswith("field-path:presence-") for leaf in owned + ) + != 1 + ): + fail("complete extension state leaf") + absent_extension_addresses = set(extension_leaf_owners) - set(extension_facts) + semantics_by_ref = _state_definition_semantics(semantic_definitions) + if set(semantics_by_ref) != set(state_by_ref): + fail("state leaf semantics") + for definition_ref, state_definition in state_by_ref.items(): + if semantics_by_ref[definition_ref] != ( + state_definition.frame_ref, + state_definition.unit_ref, + state_definition.topology_ref, + ): + fail("state leaf semantics") + + schemas = {schema.value_schema_ref: schema for schema in value_schema_definitions} + values = _leaf_values(state, base_scene) + try: + _validate_state_leaf_value_wires( + leaves, + values, + { + _state_key(leaf): metadata_by_address[address] + for address, leaf in leaf_by_address.items() + }, + schemas, + set(extension_facts), + absent_extension_addresses, + ) + except DefinitionClosureError: + fail("state leaf value schema") + return ({_state_key(leaf): leaf for leaf in leaves}, values, base_scene) + + +def _formula_predicate_refs(value: object) -> set[str]: + return { + item.predicate_ref + for item in _walk_values(value) + if isinstance(item, PredicateAtom) + } + + +def _formula_atoms(value: object) -> tuple[PredicateAtom, ...]: + """Return every atom in a closed formula tree without reinterpreting IDs.""" + + return tuple( + item for item in _walk_values(value) if isinstance(item, PredicateAtom) + ) + + +def _formula_is_fully_grounded(formula: object) -> bool: + """Require a semantic root to carry the finite grounded formula, not a template.""" + + if type(formula) is bool: + return True + ground = getattr(formula, "ground", None) + if ground is None: + return False + try: + return canonical_json_bytes(formula) == canonical_json_bytes(ground()) + except ValueError: + return False + + +def _selection_missing_capability(reason: str, value: str) -> str: + """Encode one deterministic unsupported requirement for selection replay.""" + + digest = canonical_sha256( + (reason, value), + domain="spatialcf/counterfactual/backend-capability-mismatch/3.0", + ) + return f"capability:spatialcf/counterfactual/mismatch/{reason}/{digest}" + + +def _selection_routing_claim_refs( + definitions: dict[str, CanonicalDefinitionEnvelope], + roles: dict[str, str], + routing_policy: BackendRoutingPolicy, +) -> tuple[str, str]: + """Resolve typed routing claims while replaying a sealed selection.""" + + try: + routing_definition = definitions[routing_policy.routing_policy_ref] + match_ref = _definition_record_reference( + routing_definition, + _ROUTING_MATCH_CLAIM_FIELD, + ) + mismatch_ref = _definition_record_reference( + routing_definition, + _ROUTING_MISMATCH_CLAIM_FIELD, + ) + except (DefinitionClosureError, KeyError) as error: + raise SemanticContractError("routing policy semantics") from error + if ( + roles.get(routing_policy.routing_policy_ref) != _ROLE_ROUTING_POLICY + or roles.get(match_ref) != _ROLE_ROUTING_MATCH + or roles.get(mismatch_ref) != _ROLE_ROUTING_MISMATCH + ): + raise SemanticContractError("routing policy semantics") + return match_ref, mismatch_ref + + +def _selection_proof_material_refs( + definitions: dict[str, CanonicalDefinitionEnvelope], + roles: dict[str, str], + proof_policy: ProofPolicy, +) -> set[str]: + """Resolve only proof material bound to the policy's accepted claims.""" + + proof_material_refs: set[str] = set() + for claim_ref in proof_policy.accepted_claim_definition_refs: + try: + claim_definition = definitions[claim_ref] + proof_material_ref = _definition_record_reference( + claim_definition, + _CLAIM_PROOF_MATERIAL_FIELD, + ) + except (DefinitionClosureError, KeyError) as error: + raise SemanticContractError("proof policy claim metadata") from error + if ( + roles.get(claim_ref) not in {_ROLE_CERTIFIED_SOLUTION, _ROLE_PROVEN_UNSAT} + or roles.get(proof_material_ref) != _ROLE_PROOF_MATERIAL + ): + raise SemanticContractError("proof policy claim metadata") + proof_material_refs.add(proof_material_ref) + return proof_material_refs + + +def _selection_backend_requirements_for_descriptor_build( + request: CounterfactualSolveRequest, + action_space_profile: ActionSpaceProfile, + descriptor: SolverBackendDescriptor, +) -> tuple[set[str], set[str], set[str]]: + """Partition requirements into this build, another build, and unresolved rows.""" + + snapshot = request.implementation_registry_snapshot + owner_by_capability = { + binding.definition_or_capability_ref: binding.implementation_owner_ref + for binding in snapshot.definition_and_capability_owner_bindings + if binding.definition_or_capability_ref.startswith("capability:") + } + build_by_owner = dict(snapshot.implementation_build_hashes) + matched_for_this_build: set[str] = set() + other_valid_build: set[str] = set() + structurally_unresolved: set[str] = set() + for capability in action_space_profile.backend_capability_requirements: + owner_ref = owner_by_capability.get(capability) + if owner_ref is None: + structurally_unresolved.add(capability) + continue + owner_build = build_by_owner.get(owner_ref) + if owner_build is None: + structurally_unresolved.add(capability) + elif owner_build == descriptor.implementation_build_sha256: + matched_for_this_build.add(capability) + else: + other_valid_build.add(capability) + return ( + matched_for_this_build, + other_valid_build, + structurally_unresolved, + ) + + +def _reconstruct_backend_match( + request: CounterfactualSolveRequest, + action_space_profile: ActionSpaceProfile, + semantics_profile: SemanticsProfile, + predicate_definitions: tuple[PredicateDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], + descriptor: SolverBackendDescriptor, + definitions: dict[str, CanonicalDefinitionEnvelope], + roles: dict[str, str], +) -> CapabilityMatch | CapabilityMismatch: + """Recompute one submitted routing row without importing the backend owner. + + ``spatialcf.core.backends`` remains the public matcher and protocol owner. + The registry duplicates this small, pure comparison only to reconstruct the + candidate rows it must verify in an outcome DAG; it never delegates to, or + imports, another core module. + """ + + match_claim, mismatch_claim = _selection_routing_claim_refs( + definitions, + roles, + request.backend_routing_policy, + ) + if not _self_digest_matches(descriptor): + return CapabilityMismatch( + backend_ref=descriptor.backend_ref, + backend_descriptor_sha256=descriptor.backend_descriptor_sha256, + missing_capability_refs=( + _selection_missing_capability("descriptor", descriptor.backend_ref), + ), + reason_claim_definition_ref=mismatch_claim, + ) + + predicate_required = set(action_space_profile.predicate_capability_refs) + for definition in predicate_definitions: + predicate_required.add(definition.evaluator_capability_ref) + predicate_required.add(definition.verifier_capability_ref) + operator_required = { + capability + for definition in operator_definitions + for capability in ( + definition.compiler_capability_ref, + definition.verifier_capability_ref, + ) + } + missing_by_reason: dict[str, set[str]] = {} + if action_space_profile.action_space_profile_sha256 not in set( + descriptor.supported_profile_hashes + ): + missing_by_reason["profile"] = { + _selection_missing_capability( + "profile", + action_space_profile.action_space_profile_sha256, + ) + } + predicate_missing = predicate_required - set( + descriptor.supported_predicate_capabilities + ) + if predicate_missing: + missing_by_reason["predicate"] = predicate_missing + operator_missing = operator_required - set( + descriptor.supported_operator_capabilities + ) + if operator_missing: + missing_by_reason["operator"] = operator_missing + objective_missing = set(action_space_profile.objective_capability_refs) - set( + descriptor.supported_objective_capabilities + ) + if objective_missing: + missing_by_reason["objective"] = objective_missing + numeric_missing = { + semantics_profile.numeric_semantics_ref, + request.semantic_problem.numeric_semantics_ref, + } - set(descriptor.supported_numeric_semantics) + if numeric_missing: + missing_by_reason["numeric"] = { + _selection_missing_capability("numeric", reference) + for reference in numeric_missing + } + proof_missing = set( + proof_policy_capabilities + := request.proof_policy.required_checker_capability_refs + ) - set(descriptor.compatible_checker_capability_refs) + proof_material_missing = _selection_proof_material_refs( + definitions, + roles, + request.proof_policy, + ) - set(descriptor.emitted_proof_material_definition_refs) + if proof_material_missing: + proof_missing.update( + _selection_missing_capability("proof-material", reference) + for reference in proof_material_missing + ) + if proof_missing: + missing_by_reason["proof"] = proof_missing + resource_missing = { + limit.definition_ref for limit in request.resource_policy.limits + } - set(descriptor.resource_definition_refs) + if resource_missing: + missing_by_reason["resource"] = { + _selection_missing_capability("resource", reference) + for reference in resource_missing + } + ( + matched_backend_requirements, + _other_valid_build_requirements, + structurally_unresolved_backend_requirements, + ) = _selection_backend_requirements_for_descriptor_build( + request, + action_space_profile, + descriptor, + ) + if not matched_backend_requirements: + missing_by_reason["backend"] = set( + action_space_profile.backend_capability_requirements + ) + elif structurally_unresolved_backend_requirements: + missing_by_reason["backend"] = set(structurally_unresolved_backend_requirements) + registered = next( + ( + candidate + for candidate in request.backend_descriptor_bundle.backend_descriptors + if candidate.backend_ref == descriptor.backend_ref + ), + None, + ) + if ( + registered is None + or registered.backend_descriptor_sha256 != descriptor.backend_descriptor_sha256 + or canonical_json_bytes(registered) != canonical_json_bytes(descriptor) + ): + missing_by_reason.setdefault("backend", set()).add( + _selection_missing_capability("backend", descriptor.backend_ref) + ) + if missing_by_reason: + return CapabilityMismatch( + backend_ref=descriptor.backend_ref, + backend_descriptor_sha256=descriptor.backend_descriptor_sha256, + missing_capability_refs=tuple( + sorted( + { + capability + for reason in _MISMATCH_ORDER + for capability in missing_by_reason.get(reason, set()) + }, + key=_ref_key, + ) + ), + reason_claim_definition_ref=mismatch_claim, + ) + matched = ( + matched_backend_requirements + | predicate_required + | operator_required + | set(action_space_profile.objective_capability_refs) + | set(proof_policy_capabilities) + ) + return CapabilityMatch( + backend_ref=descriptor.backend_ref, + backend_descriptor_sha256=descriptor.backend_descriptor_sha256, + matched_capability_refs=tuple(sorted(matched, key=_ref_key)), + match_claim_definition_ref=match_claim, + ) + + +def _reconstructed_backend_rows( + request: CounterfactualSolveRequest, + action_space_profile: ActionSpaceProfile, + semantics_profile: SemanticsProfile, + predicate_definitions: tuple[PredicateDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], + definitions: dict[str, CanonicalDefinitionEnvelope], + roles: dict[str, str], +) -> tuple[CapabilityMatch | CapabilityMismatch, ...]: + """Return the exact candidate universe that an outcome record must carry.""" + + rows = tuple( + _reconstruct_backend_match( + request, + action_space_profile, + semantics_profile, + predicate_definitions, + operator_definitions, + descriptor, + definitions, + roles, + ) + for descriptor in request.backend_descriptor_bundle.backend_descriptors + ) + if len({row.backend_ref for row in rows}) != len(rows): + raise SemanticContractError("ordered backend candidates") + return tuple(sorted(rows, key=lambda row: canonical_json_bytes(row.backend_ref))) + + +@dataclass(frozen=True) +class StaticOwner: + """One immutable trusted composition row; its object never enters a wire.""" + + owner_ref: str + implementation_build_sha256: str + capability_refs: tuple[str, ...] + implementation: object + + def __post_init__(self) -> None: + try: + _OWNER_REF_ADAPTER.validate_python(self.owner_ref, strict=True) + except ValidationError: + raise ValueError("static owner ref must be canonical") + if not _is_sha256(self.implementation_build_sha256): + raise ValueError("static owner build must be an exact sha256") + if not isinstance(self.capability_refs, tuple): + raise TypeError("static owner capabilities must be an immutable tuple") + try: + validated_capabilities = tuple( + _CAPABILITY_REF_ADAPTER.validate_python(capability, strict=True) + for capability in self.capability_refs + ) + except ValidationError: + raise ValueError("static owner capabilities must be canonical") + if any("*" in capability for capability in validated_capabilities): + raise ValueError("static owner capabilities must be canonical") + if not validated_capabilities: + raise ValueError("static owner capabilities must be canonical") + canonical = tuple(sorted(validated_capabilities, key=_ref_key)) + if validated_capabilities != canonical or len( + set(validated_capabilities) + ) != len(validated_capabilities): + raise ValueError("static owner capabilities must be sorted and unique") + try: + hash(self.implementation) + except TypeError as error: + raise TypeError("unhashable implementation") from error + + +@dataclass(frozen=True) +class StaticImplementationRegistry: + """A finite immutable map from static capabilities to trusted owners.""" + + owners: tuple[StaticOwner, ...] + + def __post_init__(self) -> None: + if not isinstance(self.owners, tuple) or not all( + isinstance(owner, StaticOwner) for owner in self.owners + ): + raise TypeError("static registry owners must be an immutable tuple") + if not self.owners: + raise ImplementationResolutionError("static registry must not be empty") + owner_refs = tuple(owner.owner_ref for owner in self.owners) + if len(set(owner_refs)) != len(owner_refs): + raise ImplementationResolutionError("duplicate static owner") + capabilities = tuple( + capability for owner in self.owners for capability in owner.capability_refs + ) + if len(set(capabilities)) != len(capabilities): + raise ImplementationResolutionError("single-owner capability") + + def _owners_by_ref(self) -> dict[str, StaticOwner]: + return {owner.owner_ref: owner for owner in self.owners} + + def _owners_by_capability(self) -> dict[str, StaticOwner]: + return { + capability: owner + for owner in self.owners + for capability in owner.capability_refs + } + + def _validate_snapshot( + self, + snapshot: ImplementationRegistrySnapshot, + required_capabilities: set[str], + specialized_records: tuple[object, ...] = (), + ) -> None: + if not _self_digest_matches(snapshot): + raise ImplementationResolutionError("registry snapshot hash") + owners = self._owners_by_ref() + capabilities = self._owners_by_capability() + build_by_owner = dict(snapshot.implementation_build_hashes) + binding_by_ref = { + binding.definition_or_capability_ref: binding.implementation_owner_ref + for binding in snapshot.definition_and_capability_owner_bindings + } + if len(binding_by_ref) != len( + snapshot.definition_and_capability_owner_bindings + ): + raise ImplementationResolutionError("registry snapshot binding") + if not required_capabilities <= capabilities.keys(): + raise ImplementationResolutionError("capability owner") + if any( + not reference.startswith(("capability:", "definition:")) + for reference in binding_by_ref + ): + raise ImplementationResolutionError("registry snapshot binding") + capability_binding_by_ref = { + reference: owner_ref + for reference, owner_ref in binding_by_ref.items() + if reference.startswith("capability:") + } + definition_binding_by_ref = { + reference: owner_ref + for reference, owner_ref in binding_by_ref.items() + if reference.startswith("definition:") + } + static_capability_refs = set(capabilities) + supplied_capability_refs = set(capability_binding_by_ref) + if supplied_capability_refs - static_capability_refs: + raise ImplementationResolutionError("capability owner") + if static_capability_refs - supplied_capability_refs: + raise ImplementationResolutionError("registry snapshot binding") + static_owner_refs = set(owners) + supplied_owner_refs = set(build_by_owner) + if supplied_owner_refs != static_owner_refs: + raise ImplementationResolutionError("registry snapshot build") + for capability, static in capabilities.items(): + if capability_binding_by_ref[capability] != static.owner_ref: + raise ImplementationResolutionError("capability owner") + for owner_ref, static in owners.items(): + if build_by_owner[owner_ref] != static.implementation_build_sha256: + raise ImplementationResolutionError("registry snapshot build") + + definition_capabilities: dict[str, tuple[str, ...]] = {} + for record in specialized_records: + if isinstance(record, PredicateDefinition): + reference = record.predicate_ref + record_capabilities = ( + record.evaluator_capability_ref, + record.verifier_capability_ref, + ) + elif isinstance(record, DerivedFactRuleDefinition): + reference = record.derived_fact_rule_ref + record_capabilities = ( + record.evaluator_capability_ref, + record.verifier_capability_ref, + ) + elif isinstance(record, OperatorDefinition): + reference = record.operator_ref + record_capabilities = ( + record.compiler_capability_ref, + record.verifier_capability_ref, + ) + else: + continue + previous = definition_capabilities.get(reference) + if previous is not None and previous != record_capabilities: + raise ImplementationResolutionError("registry snapshot binding") + definition_capabilities[reference] = record_capabilities + for reference, owner_ref in definition_binding_by_ref.items(): + record_capabilities = definition_capabilities.get(reference) + if not record_capabilities: + raise ImplementationResolutionError("registry snapshot binding") + derived_owners = tuple( + capabilities.get(capability) for capability in record_capabilities + ) + if ( + any(owner is None for owner in derived_owners) + or len( + {owner.owner_ref for owner in derived_owners if owner is not None} + ) + != 1 + ): + raise ImplementationResolutionError("registry snapshot binding") + derived_owner = next(owner for owner in derived_owners if owner is not None) + if owner_ref != derived_owner.owner_ref: + raise ImplementationResolutionError("registry snapshot binding") + + def _validate_definition_hashes( + self, + bundle: DefinitionBundle, + ) -> None: + for definition in bundle.definitions: + if not _self_digest_matches(definition): + raise DefinitionClosureError("definition hash") + if not _self_digest_matches(bundle): + raise DefinitionClosureError("definition bundle hash") + + def _validate_definition_cycles( + self, + semantic_definitions: dict[str, CanonicalDefinitionEnvelope], + solve_definitions: dict[str, CanonicalDefinitionEnvelope], + ) -> None: + """Reject every definition cycle except one typed anchor per root. + + The public backend matcher owns matching. The registry owns this + structural closure and keeps the semantic and operational roots + separate while constructing the combined dependency graph. + """ + + definitions = semantic_definitions | solve_definitions + semantic_anchor = _root_bootstrap_anchor(semantic_definitions) + solve_anchor = _root_bootstrap_anchor(solve_definitions) + anchors = {semantic_anchor, solve_anchor} + graph: dict[str, list[str]] = {} + for reference, definition in definitions.items(): + dependencies = _definition_payload_dependency_refs(definition) + # An envelope's kind reference is a dependency too. The only + # permitted self edge is the unique root-local bootstrap anchor; + # payload self references are deliberately never discarded here. + if not ( + definition.definition_kind_ref == reference and reference in anchors + ): + dependencies.add(definition.definition_kind_ref) + graph[reference] = sorted( + dependencies & definitions.keys(), + key=_ref_key, + ) + visiting: list[str] = [] + visited: set[str] = set() + + def visit(reference: str) -> None: + if reference in visiting: + start = visiting.index(reference) + path = visiting[start:] + [reference] + raise DefinitionClosureError("stable cycle path: " + " -> ".join(path)) + if reference in visited: + return + visiting.append(reference) + for dependency in graph[reference]: + visit(dependency) + visiting.pop() + visited.add(reference) + + for reference in sorted(graph, key=_ref_key): + visit(reference) + if not ( + _has_exact_root_bootstrap_shape(semantic_definitions, semantic_anchor) + and _has_exact_root_bootstrap_shape(solve_definitions, solve_anchor) + ): + raise DefinitionClosureError("root bootstrap anchor") + + def validate_definition_closure( + self, + semantic_definition_bundle: DefinitionBundle, + solve_policy_definition_bundle: DefinitionBundle, + value_schema_definitions: tuple[ValueSchemaDefinition, ...], + predicate_definitions: tuple[PredicateDefinition, ...], + state_variable_definitions: tuple[StateVariableDefinition, ...], + derived_fact_rule_definitions: tuple[DerivedFactRuleDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], + implementation_registry_snapshot: ImplementationRegistrySnapshot, + ) -> DefinitionBundle: + """Validate finite canonical definitions and their static implementation edges.""" + + if ( + semantic_definition_bundle.bootstrap_schema_sha256 + != BOOTSTRAP_SCHEMA_SHA256 + or solve_policy_definition_bundle.bootstrap_schema_sha256 + != BOOTSTRAP_SCHEMA_SHA256 + ): + raise DefinitionClosureError("bootstrap schema") + self._validate_definition_hashes(semantic_definition_bundle) + self._validate_definition_hashes(solve_policy_definition_bundle) + semantic_definitions, solve_definitions, definitions = _definition_root_maps( + semantic_definition_bundle, + solve_policy_definition_bundle, + ) + if any( + not _references(definition, "definition:") <= semantic_definitions.keys() + for definition in semantic_definitions.values() + ): + raise DefinitionClosureError("semantic definition root") + self._validate_definition_cycles(semantic_definitions, solve_definitions) + + schemas: dict[str, ValueSchemaDefinition] = {} + for schema in value_schema_definitions: + if not _self_digest_matches(schema): + raise DefinitionClosureError("value schema hash") + previous = schemas.get(schema.value_schema_ref) + if previous is not None: + if canonical_json_bytes(previous) != canonical_json_bytes(schema): + raise DefinitionClosureError( + "same value schema identifier has different bytes" + ) + raise DefinitionClosureError("duplicate value schema identifier") + schemas[schema.value_schema_ref] = schema + for schema in schemas.values(): + for reference in _schema_dependency_refs(schema): + if reference not in schemas: + raise DefinitionClosureError("schema reference") + + specialized_records = ( + *((record, record.predicate_ref) for record in predicate_definitions), + *( + (record, record.state_variable_ref) + for record in state_variable_definitions + ), + *( + (record, record.derived_fact_rule_ref) + for record in derived_fact_rule_definitions + ), + *((record, record.operator_ref) for record in operator_definitions), + ) + specialized_by_ref: dict[str, HashBoundCanonicalModel] = {} + for record, reference in specialized_records: + if not _self_digest_matches(record): + raise DefinitionClosureError("specialized definition hash") + previous = specialized_by_ref.get(reference) + if previous is not None: + if canonical_json_bytes(previous) != canonical_json_bytes(record): + raise DefinitionClosureError( + "same specialized definition identifier has different bytes" + ) + raise DefinitionClosureError("duplicate specialized definition") + specialized_by_ref[reference] = record + + records: tuple[object, ...] = ( + semantic_definition_bundle, + solve_policy_definition_bundle, + *predicate_definitions, + *state_variable_definitions, + *derived_fact_rule_definitions, + *operator_definitions, + ) + for record in records: + for value in _walk_values(record): + if isinstance(value, TypedValue): + _validate_typed_value(value, schemas) + if ( + isinstance(value, str) + and value.startswith("schema:") + and value not in schemas + ): + raise DefinitionClosureError("typed value schema") + + all_definition_refs = set() + required_capabilities = set() + for record in records: + all_definition_refs.update(_references(record, "definition:")) + required_capabilities.update(_references(record, "capability:")) + dangling = all_definition_refs - definitions.keys() + if dangling: + raise DefinitionClosureError("dangling definition reference") + roles = _definition_roles(definitions) + semantic_roles = _definition_roles(semantic_definitions) + solve_roles = _definition_roles(solve_definitions) + if any(role == _ROLE_RECORD_BINDING for role in solve_roles.values()): + raise DefinitionClosureError("definition record binding") + record_bindings = _definition_record_bindings( + semantic_definitions, + semantic_roles, + ) + for reference, record in ( + *schemas.items(), + *specialized_by_ref.items(), + ): + if record_bindings.get(reference) != getattr( + record, + record.SELF_DIGEST_FIELD, + ): + raise DefinitionClosureError("definition record binding") + for reference, role in roles.items(): + definition = definitions[reference] + if role == _ROLE_PROOF_MATERIAL: + payload_schema_ref = _definition_record_reference( + definition, + _PROOF_PAYLOAD_SCHEMA_FIELD, + ) + if payload_schema_ref not in schemas: + raise DefinitionClosureError("proof material schema") + _definition_record_reference( + definition, + _PROOF_CHECKER_CAPABILITY_FIELD, + ) + elif role in {_ROLE_CERTIFIED_SOLUTION, _ROLE_PROVEN_UNSAT}: + proof_definition_ref = _definition_record_reference( + definition, + _CLAIM_PROOF_MATERIAL_FIELD, + ) + if ( + reference not in semantic_definitions + or semantic_roles.get(proof_definition_ref) != _ROLE_PROOF_MATERIAL + ): + raise DefinitionClosureError("claim proof material") + _definition_record_reference( + definition, + _CLAIM_CHECKER_CAPABILITY_FIELD, + ) + elif role in {_ROLE_COMPLETE_DOMAIN, _ROLE_SOUND_COMPLETE_DOMAIN}: + claim_ref = _definition_record_reference( + definition, + _COMPLETE_DOMAIN_CLAIM_FIELD, + ) + if ( + reference not in semantic_definitions + or semantic_roles.get(claim_ref) != _ROLE_PROVEN_UNSAT + ): + raise DefinitionClosureError("complete-domain claim") + # The typed envelope is the semantic source of truth for specialized + # records. Matching by a textual reference suffix would make a hostile + # wire indistinguishable from a legitimate extension. + for definition in predicate_definitions: + _require_definition_role( + semantic_roles, + definition.predicate_ref, + "definition-kind:predicate", + ) + for definition in state_variable_definitions: + _require_definition_role( + semantic_roles, + definition.state_variable_ref, + "definition-kind:state-variable", + ) + for definition in derived_fact_rule_definitions: + _require_definition_role( + semantic_roles, + definition.derived_fact_rule_ref, + "definition-kind:derived-rule", + ) + for definition in operator_definitions: + _require_definition_role( + semantic_roles, + definition.operator_ref, + "definition-kind:operator", + ) + self._validate_snapshot( + implementation_registry_snapshot, + required_capabilities, + ( + *predicate_definitions, + *state_variable_definitions, + *derived_fact_rule_definitions, + *operator_definitions, + ), + ) + return semantic_definition_bundle + + def validate_semantic_problem( + self, + semantic_definition_bundle: DefinitionBundle, + solve_policy_definition_bundle: DefinitionBundle, + value_schema_definitions: tuple[ValueSchemaDefinition, ...], + predicate_definitions: tuple[PredicateDefinition, ...], + state_variable_definitions: tuple[StateVariableDefinition, ...], + derived_fact_rule_definitions: tuple[DerivedFactRuleDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], + implementation_registry_snapshot: ImplementationRegistrySnapshot, + problem: CounterfactualProblemIR, + semantics_profile: SemanticsProfile, + action_space_profile: ActionSpaceProfile, + scene_state: SceneStateEnvelope, + ) -> CounterfactualProblemIR: + """Validate problem/profile/scene/action closure on explicit input records.""" + + # Specialized records are not roots merely because a caller supplied + # them alongside a problem. The profiles and request authorization + # choose the finite semantic universe; accepting an extra record here + # would let an otherwise unreachable envelope and binding make itself + # reachable in the semantic definition bundle below. + try: + supplied_predicate_refs = tuple( + definition.predicate_ref for definition in predicate_definitions + ) + supplied_operator_refs = tuple( + definition.operator_ref for definition in operator_definitions + ) + supplied_state_refs = tuple( + definition.state_variable_ref + for definition in state_variable_definitions + ) + supplied_derived_rule_refs = tuple( + definition.derived_fact_rule_ref + for definition in derived_fact_rule_definitions + ) + except AttributeError as error: + raise SemanticContractError("profile definition closure") from error + + expected_predicate_refs = set(semantics_profile.predicate_definition_refs) + expected_operator_refs = set(action_space_profile.allowed_operator_refs) + expected_state_refs = set(action_space_profile.state_variable_definition_refs) + if ( + len(set(supplied_predicate_refs)) != len(supplied_predicate_refs) + or len(set(supplied_operator_refs)) != len(supplied_operator_refs) + or len(set(supplied_state_refs)) != len(supplied_state_refs) + or len(set(supplied_derived_rule_refs)) != len(supplied_derived_rule_refs) + ): + raise SemanticContractError("profile definition closure") + + # Preserve the semantic source of a malformed cross-record edge before + # enforcing exact supplied specialized tuples. A profile omission is + # not the same violation as a caller-supplied unreferenced record: the + # former must identify authorization, operator, or derived-output + # authority, while the latter remains a closed-root failure below. + authorization = problem.intervention_authorization + for leaf in authorization.authorized_primary_write_set: + matching_definitions = tuple( + definition + for definition in state_variable_definitions + if definition.state_variable_schema_ref + == leaf.state_variable_schema_ref + ) + if ( + len(matching_definitions) == 1 + and matching_definitions[0].state_variable_ref + not in expected_state_refs + ): + raise SemanticContractError("authorization profile state") + + supplied_derived_rule_ref_set = set(supplied_derived_rule_refs) + semantic_derived_rule_refs = set(semantics_profile.derived_fact_rule_refs) + required_derived_rule_refs = set(authorization.required_derived_rule_refs) + if ( + not required_derived_rule_refs <= semantic_derived_rule_refs + or not required_derived_rule_refs <= supplied_derived_rule_ref_set + ): + raise SemanticContractError("authorization derived rule") + operator_derived_rule_refs = { + rule_ref + for definition in operator_definitions + for rule_ref in definition.derived_write_rule_refs + } + if not required_derived_rule_refs <= operator_derived_rule_refs: + raise SemanticContractError("authorization derived rule") + for definition in operator_definitions: + if not set(definition.derived_write_rule_refs) <= ( + semantic_derived_rule_refs & supplied_derived_rule_ref_set + ): + raise SemanticContractError("operator derived rule") + + for rule in derived_fact_rule_definitions: + for output in rule.fixed_output_set: + matching_definitions = tuple( + definition + for definition in state_variable_definitions + if definition.state_variable_schema_ref + == output.state_variable_schema_ref + ) + if len(matching_definitions) != 1: + continue + output_definition = matching_definitions[0] + if output_definition.write_authority is not WriteAuthority.DERIVED_ONLY: + raise SemanticContractError("derived output authority") + if ( + output_definition.derived_fact_rule_ref + != rule.derived_fact_rule_ref + ): + raise SemanticContractError("derived output owner") + for definition in state_variable_definitions: + if ( + definition.derived_fact_rule_ref is not None + and definition.derived_fact_rule_ref + not in semantic_derived_rule_refs & supplied_derived_rule_ref_set + ): + raise SemanticContractError("derived output owner") + + if ( + set(supplied_predicate_refs) != expected_predicate_refs + or set(supplied_operator_refs) != expected_operator_refs + or set(supplied_state_refs) != expected_state_refs + ): + raise SemanticContractError("profile definition closure") + + supplied_states_by_ref = { + definition.state_variable_ref: definition + for definition in state_variable_definitions + } + selected_state_definitions = tuple( + supplied_states_by_ref[reference] for reference in expected_state_refs + ) + expected_derived_rule_refs = required_derived_rule_refs | { + definition.derived_fact_rule_ref + for definition in selected_state_definitions + if definition.derived_fact_rule_ref is not None + } + if ( + set(supplied_derived_rule_refs) != expected_derived_rule_refs + or not expected_derived_rule_refs <= semantic_derived_rule_refs + ): + raise SemanticContractError("profile definition closure") + + self.validate_definition_closure( + semantic_definition_bundle, + solve_policy_definition_bundle, + value_schema_definitions, + predicate_definitions, + state_variable_definitions, + derived_fact_rule_definitions, + operator_definitions, + implementation_registry_snapshot, + ) + if problem.definition_bundle != semantic_definition_bundle: + raise SemanticContractError("semantic definition bundle") + if problem.scene_state != scene_state: + raise SemanticContractError("scene state") + if ( + problem.semantics_profile_ref != semantics_profile.semantics_profile_ref + or problem.action_space_profile_ref + != action_space_profile.action_space_profile_ref + ): + raise SemanticContractError("semantic/action profile") + profile_definitions, solve_definitions, _definitions = _definition_root_maps( + semantic_definition_bundle, + solve_policy_definition_bundle, + ) + profile_bindings = _definition_record_bindings( + profile_definitions, + _definition_roles(profile_definitions), + ) + for reference, digest in ( + ( + semantics_profile.semantics_profile_ref, + semantics_profile.semantics_profile_sha256, + ), + ( + action_space_profile.action_space_profile_ref, + action_space_profile.action_space_profile_sha256, + ), + ): + if profile_bindings.get(reference) != digest: + raise DefinitionClosureError("definition record binding") + if ( + not _references(semantics_profile, "definition:") + <= profile_definitions.keys() + ): + raise DefinitionClosureError("semantic definition root") + action_profile_refs = _references(action_space_profile, "definition:") + permitted_operational_profile_ref = { + action_space_profile.publication_proof_policy_ref + } + if ( + not action_profile_refs - permitted_operational_profile_ref + <= profile_definitions.keys() + or action_space_profile.publication_proof_policy_ref + not in solve_definitions + ): + raise DefinitionClosureError("semantic definition root") + + # Do not let the caller's schema tuple or the problem's embedded + # definition bundle establish semantic meaning. The finite schema + # universe starts at real problem/profile records and the exact + # profile-selected specialized records, then closes through semantic + # definition payloads and declared schema dependencies. + semantic_root_records: tuple[object, ...] = ( + scene_state, + problem.intervention_authorization, + problem.before_preconditions, + problem.after_goal, + problem.preservation_invariants, + problem.explicit_observation_obligations, + problem.objective_expression, + problem.numeric_semantics_ref, + semantics_profile, + action_space_profile, + *predicate_definitions, + *state_variable_definitions, + *derived_fact_rule_definitions, + *operator_definitions, + ) + schemas = { + schema.value_schema_ref: schema for schema in value_schema_definitions + } + expected_schema_refs = _semantic_schema_definition_closure( + profile_definitions, + schemas, + semantic_root_records, + ) + if set(schemas) != expected_schema_refs: + raise DefinitionClosureError("semantic schema closure") + _validate_exact_root_definition_closure( + profile_definitions, + root_records=semantic_root_records, + record_binding_targets={ + problem.numeric_semantics_ref, + semantics_profile.semantics_profile_ref, + action_space_profile.action_space_profile_ref, + *expected_schema_refs, + }, + root_label="semantic", + include_complete_domain_dependents=True, + ) + if ( + problem.numeric_semantics_ref != semantics_profile.numeric_semantics_ref + or action_space_profile.numeric_semantics_ref + != semantics_profile.numeric_semantics_ref + ): + raise SemanticContractError("profile numeric semantics") + if ( + scene_state.base_scene_schema_ref + not in semantics_profile.accepted_scene_and_fact_schema_refs + or scene_state.base_scene_schema_ref + not in action_space_profile.accepted_scene_schema_refs + ): + raise SemanticContractError("scene schema") + + _, leaf_values, base_scene = _validate_scene_state_envelope( + scene_state, + state_variable_definitions, + value_schema_definitions, + profile_definitions, + after_state=False, + ) + + expected_entities = { + identifier for _family, identifier, _value in _base_fact_rows(base_scene) + } | { + fact.subject_entity_id + for bundle in scene_state.extension_fact_bundles + for fact in bundle.facts + } + if set(scene_state.closed_entity_index) != expected_entities: + raise SemanticContractError("complete scene entity index") + leaves = scene_state.canonical_state_leaf_index.leaves + leaf_keys = {_state_key(leaf) for leaf in leaves} + base_owners = { + (family, identifier) + for family, identifier, _fact in _base_fact_rows(base_scene) + } + extension_facts = _extension_facts_by_address(scene_state) + base_addresses = { + (leaf.fact_family_ref, leaf.entity_or_fact_key, leaf.field_path_ref) + for leaf in leaves + if (leaf.fact_family_ref, leaf.entity_or_fact_key) in base_owners + } + if base_addresses != _expected_base_leaf_addresses(base_scene): + raise SemanticContractError("exact state leaf index") + by_family_identifier = _state_leaf_owners(leaves) + for family, identifier, _value in _base_fact_rows(base_scene): + owned = by_family_identifier.get((family, identifier), ()) + if not any( + leaf.field_path_ref.startswith("field-path:presence-") for leaf in owned + ): + raise SemanticContractError("complete state leaf presence") + if not any( + not leaf.field_path_ref.startswith("field-path:presence-") + for leaf in owned + ): + raise SemanticContractError("complete state leaf value") + + state_by_schema = { + definition.state_variable_schema_ref: definition + for definition in state_variable_definitions + } + state_by_ref = { + definition.state_variable_ref: definition + for definition in state_variable_definitions + } + if len(state_by_schema) != len(state_variable_definitions) or len( + state_by_ref + ) != len(state_variable_definitions): + raise SemanticContractError("state leaf definition") + if any( + leaf.state_variable_schema_ref not in state_by_schema for leaf in leaves + ): + raise SemanticContractError("state leaf definition") + if not leaf_keys: + raise SemanticContractError("complete state leaf index") + + # A submitted leaf is not owned merely because its schema happens to + # occur in a state definition. Its complete address and value schema + # must come from the explicit typed definition record. This makes the + # frozen scene index a closed semantic partition, not an opaque list of + # presence/value placeholders. + definitions, _solve_definitions, _all_definitions = _definition_root_maps( + semantic_definition_bundle, + solve_policy_definition_bundle, + ) + metadata_by_ref = _state_definition_metadata(definitions) + if set(metadata_by_ref) != set(state_by_ref): + raise SemanticContractError("schema-owned field path") + metadata_by_address: dict[ + tuple[str, str, str, str, str], StateVariableDefinition + ] = {} + for definition_ref, state_definition in state_by_ref.items(): + ( + state_variable_schema_ref, + state_schema_ref, + fact_family_ref, + entity_or_fact_key, + field_path_ref, + value_schema_ref, + ) = metadata_by_ref[definition_ref] + if ( + state_variable_schema_ref != state_definition.state_variable_schema_ref + or value_schema_ref != state_definition.value_schema_ref + ): + raise SemanticContractError("schema-owned field path") + address = ( + state_variable_schema_ref, + state_schema_ref, + fact_family_ref, + entity_or_fact_key, + field_path_ref, + ) + if address in metadata_by_address: + raise SemanticContractError("schema-owned field path") + metadata_by_address[address] = state_definition + leaf_by_address = { + ( + leaf.state_variable_schema_ref, + leaf.state_schema_ref, + leaf.fact_family_ref, + leaf.entity_or_fact_key, + leaf.field_path_ref, + ): leaf + for leaf in leaves + } + if set(leaf_by_address) != set(metadata_by_address): + raise SemanticContractError("schema-owned field path") + extension_leaf_owners = _declared_extension_leaf_owners( + leaves, + base_owners, + ) + if not set(extension_facts) <= set(extension_leaf_owners): + raise SemanticContractError("extension fact address") + for owned in extension_leaf_owners.values(): + if ( + len(owned) != 2 + or sum( + leaf.field_path_ref.startswith("field-path:presence-") + for leaf in owned + ) + != 1 + ): + raise SemanticContractError("complete extension state leaf") + absent_extension_addresses = set(extension_leaf_owners) - set(extension_facts) + semantics_by_ref = _state_definition_semantics(definitions) + if set(semantics_by_ref) != set(state_by_ref): + raise SemanticContractError("state leaf semantics") + for definition_ref, state_definition in state_by_ref.items(): + if semantics_by_ref[definition_ref] != ( + state_definition.frame_ref, + state_definition.unit_ref, + state_definition.topology_ref, + ): + raise SemanticContractError("state leaf semantics") + semantic_definition_refs = { + reference + for record in semantic_root_records + for reference in _references(record, "definition:") + } - permitted_operational_profile_ref + if not semantic_definition_refs <= profile_definitions.keys(): + raise SemanticContractError("semantic definition closure") + profile_capabilities = _references(action_space_profile, "capability:") + self._validate_snapshot( + implementation_registry_snapshot, + profile_capabilities, + ( + *predicate_definitions, + *state_variable_definitions, + *derived_fact_rule_definitions, + *operator_definitions, + ), + ) + try: + _validate_state_leaf_value_wires( + leaves, + leaf_values, + { + _state_key(leaf): metadata_by_address[address] + for address, leaf in leaf_by_address.items() + }, + schemas, + set(extension_facts), + absent_extension_addresses, + ) + except DefinitionClosureError as error: + raise SemanticContractError("state leaf value schema") from error + + predicate_by_ref = { + definition.predicate_ref: definition for definition in predicate_definitions + } + derived_rules = { + definition.derived_fact_rule_ref: definition + for definition in derived_fact_rule_definitions + } + if ( + set(predicate_by_ref) != expected_predicate_refs + or set(derived_rules) != expected_derived_rule_refs + or set(state_by_ref) != expected_state_refs + ): + raise SemanticContractError("profile definition closure") + predicate_refs = _formula_predicate_refs( + ( + problem.before_preconditions, + problem.after_goal, + problem.preservation_invariants, + problem.explicit_observation_obligations, + ) + ) + if not predicate_refs <= predicate_by_ref.keys(): + raise SemanticContractError("formula predicate closure") + if not predicate_refs <= set(semantics_profile.predicate_definition_refs): + raise SemanticContractError("profile predicate closure") + formula_contexts = ( + *(item.formula for item in problem.before_preconditions), + problem.after_goal.formula, + *( + formula + for invariant in problem.preservation_invariants + for formula in (invariant.before_formula, invariant.after_formula) + ), + *(item.formula for item in problem.explicit_observation_obligations), + ) + if not all(_formula_is_fully_grounded(formula) for formula in formula_contexts): + raise SemanticContractError("formula grounding") + for atom in _formula_atoms(formula_contexts): + predicate = predicate_by_ref.get(atom.predicate_ref) + if ( + predicate is None + or tuple(operand.value_schema_ref for operand in atom.operands) + != predicate.operand_schema_refs + ): + raise SemanticContractError("formula predicate closure") + try: + for operand in atom.operands: + _validate_typed_value(operand, schemas) + except DefinitionClosureError as error: + raise SemanticContractError("formula predicate closure") from error + actual_fact_families = { + family for family, _identifier, _fact in _base_fact_rows(base_scene) + } | { + fact.fact_family_ref + for bundle in scene_state.extension_fact_bundles + for fact in bundle.facts + } + for predicate_ref in predicate_refs: + predicate = predicate_by_ref[predicate_ref] + for prerequisite_ref in predicate.observation_prerequisite_template_refs: + prerequisite = definitions.get(prerequisite_ref) + if prerequisite is None: + raise SemanticContractError("prerequisite closure") + try: + required_fact_family = _definition_record_reference( + prerequisite, + _PREREQUISITE_FACT_FAMILY_FIELD, + ) + except DefinitionClosureError as error: + raise SemanticContractError("prerequisite closure") from error + if required_fact_family not in actual_fact_families: + raise SemanticContractError("required fact completeness") + + operators = { + definition.operator_ref: definition for definition in operator_definitions + } + if set(operators) != expected_operator_refs: + raise SemanticContractError("profile definition closure") + authorization = problem.intervention_authorization + if ( + not authorization.allowed_operator_refs + or not set(authorization.allowed_operator_refs) + <= set(action_space_profile.allowed_operator_refs) + or not set(authorization.allowed_operator_refs) <= operators.keys() + ): + raise SemanticContractError("authorization") + if not set(authorization.editable_entity_ids) <= set( + scene_state.closed_entity_index + ): + raise SemanticContractError("authorization") + authorization_keys = { + _state_key(leaf) for leaf in authorization.authorized_primary_write_set + } + if not authorization_keys <= leaf_keys: + raise SemanticContractError("authorization") + leaf_by_key = {_state_key(leaf): leaf for leaf in leaves} + extension_subjects = { + address: fact.subject_entity_id + for address, fact in _extension_facts_by_address(scene_state).items() + } + for leaf in authorization.authorized_primary_write_set: + definition = state_by_schema.get(leaf.state_variable_schema_ref) + if ( + definition is None + or definition.write_authority is not WriteAuthority.PRIMARY_WRITABLE + or extension_subjects.get( + (leaf.fact_family_ref, leaf.entity_or_fact_key), + leaf.entity_or_fact_key, + ) + not in authorization.editable_entity_ids + ): + raise SemanticContractError("authorization") + authorized_primary_definition_refs = { + state_by_schema[leaf.state_variable_schema_ref].state_variable_ref + for leaf in authorization.authorized_primary_write_set + } + profile_state_definition_refs = set( + action_space_profile.state_variable_definition_refs + ) + if not authorized_primary_definition_refs <= profile_state_definition_refs: + raise SemanticContractError("authorization profile state") + for bound in authorization.variable_bounds: + bound_leaf = leaf_by_key.get(_state_key(bound.state_variable_ref)) + bound_definition = state_by_schema.get( + bound.state_variable_ref.state_variable_schema_ref + ) + if ( + _state_key(bound.state_variable_ref) not in authorization_keys + or bound_definition is None + or bound_definition.write_authority + is not WriteAuthority.PRIMARY_WRITABLE + ): + raise SemanticContractError("variable bound authorization") + if bound_leaf != bound.state_variable_ref or ( + bound.value_schema_ref, + bound.frame_ref, + bound.unit_ref, + bound.topology_ref, + ) != ( + bound_definition.value_schema_ref, + bound_definition.frame_ref, + bound_definition.unit_ref, + bound_definition.topology_ref, + ): + raise SemanticContractError("variable bound semantics") + try: + _validate_typed_value(bound.typed_domain, schemas) + except DefinitionClosureError as error: + raise SemanticContractError("variable bound semantics") from error + mandatory_invariant_template_refs = set( + action_space_profile.mandatory_invariant_template_refs + ) + if not mandatory_invariant_template_refs <= { + invariant.transition_comparator_ref + for invariant in problem.preservation_invariants + }: + raise SemanticContractError("mandatory invariant closure") + required_derived_rule_refs = set(authorization.required_derived_rule_refs) + if not required_derived_rule_refs <= set( + semantics_profile.derived_fact_rule_refs + ) or not required_derived_rule_refs <= { + rule_ref + for operator_ref in authorization.allowed_operator_refs + for rule_ref in operators[operator_ref].derived_write_rule_refs + }: + raise SemanticContractError("authorization derived rule") + for operator_ref in action_space_profile.allowed_operator_refs: + operator = operators[operator_ref] + if ( + operator.transition_semantics_ref + not in semantics_profile.transition_semantics_refs + ): + raise SemanticContractError("operator transition semantics") + for pattern in ( + *operator.read_footprint, + *operator.primary_write_footprint, + ): + state_definition = state_by_ref.get( + pattern.state_variable_definition_ref + ) + if state_definition is None: + raise SemanticContractError("operator state footprint") + if ( + pattern.state_variable_definition_ref + not in profile_state_definition_refs + ): + raise SemanticContractError("operator profile state") + if any( + binding.parameter_schema_ref not in operator.parameter_schema_refs + for binding in pattern.parameter_bindings + ): + raise SemanticContractError("operator parameter binding") + if not set( + operator.derived_write_rule_refs + ) <= derived_rules.keys() or not set( + operator.derived_write_rule_refs + ) <= set(semantics_profile.derived_fact_rule_refs): + raise SemanticContractError("operator derived rule") + allowed_primary_footprints = { + pattern.state_variable_definition_ref + for operator_ref in authorization.allowed_operator_refs + for pattern in operators[operator_ref].primary_write_footprint + } + if not authorized_primary_definition_refs <= allowed_primary_footprints: + raise SemanticContractError("authorization operator footprint") + output_owners: dict[bytes, str] = {} + for rule in derived_fact_rule_definitions: + for read in rule.fixed_read_set: + read_leaf = leaf_by_key.get(_state_key(read)) + read_definition = state_by_schema.get(read.state_variable_schema_ref) + if read_leaf != read or read_definition is None: + raise SemanticContractError("derived read closure") + for output in rule.fixed_output_set: + output_leaf = leaf_by_key.get(_state_key(output)) + output_definition = state_by_schema.get( + output.state_variable_schema_ref + ) + if ( + output_leaf != output + or output_definition is None + or output_definition.write_authority + is not WriteAuthority.DERIVED_ONLY + ): + raise SemanticContractError("derived output authority") + if ( + output_definition.derived_fact_rule_ref + != rule.derived_fact_rule_ref + ): + raise SemanticContractError("derived output owner") + output_key = _state_key(output) + if output_key in output_owners: + raise SemanticContractError("derived output owner") + output_owners[output_key] = rule.derived_fact_rule_ref + derived_output_definition_refs = { + state_by_schema[output.state_variable_schema_ref].state_variable_ref + for rule in derived_fact_rule_definitions + for output in rule.fixed_output_set + } + derived_only_definition_refs = { + definition.state_variable_ref + for definition in state_variable_definitions + if definition.write_authority is WriteAuthority.DERIVED_ONLY + } + profile_primary_footprints = { + pattern.state_variable_definition_ref + for operator_ref in action_space_profile.allowed_operator_refs + for pattern in operators[operator_ref].primary_write_footprint + } + if profile_primary_footprints & ( + derived_output_definition_refs | derived_only_definition_refs + ): + raise SemanticContractError("primary/derived footprint") + if not required_derived_rule_refs <= { + rule.derived_fact_rule_ref for rule in derived_fact_rule_definitions + }: + raise SemanticContractError("authorization derived rule") + objective_refs = { + term.objective_definition_ref for term in problem.objective_expression.terms + } + if not objective_refs <= set(semantics_profile.objective_definition_refs): + raise SemanticContractError("objective closure") + for term in problem.objective_expression.terms: + objective_definition = definitions.get(term.objective_definition_ref) + if objective_definition is None: + raise SemanticContractError("objective closure") + try: + expected_objective_semantics = ( + _definition_record_reference( + objective_definition, + _OBJECTIVE_INPUT_SELECTOR_FIELD, + ), + _definition_record_reference( + objective_definition, + _OBJECTIVE_UNIT_FIELD, + ), + _definition_record_reference( + objective_definition, + _OBJECTIVE_NORMALIZATION_FIELD, + ), + ) + except DefinitionClosureError as error: + raise SemanticContractError("objective unit/normalization") from error + if expected_objective_semantics != ( + term.input_selector_definition_ref, + term.unit_ref, + term.normalization_definition_ref, + ): + raise SemanticContractError("objective unit/normalization") + # Hash identity is checked after the explanatory semantic boundary so a + # malformed authorization/leaf/profile reports that direct violation + # rather than a stale enclosing root caused by a test-only model copy. + for record, reason in ( + (problem, "semantic problem hash"), + (semantics_profile, "semantics profile hash"), + (action_space_profile, "action profile hash"), + (scene_state, "scene state hash"), + ): + if not _self_digest_matches(record): + raise SemanticContractError(reason) + return problem + + def validate_solve_request( + self, + semantic_definition_bundle: DefinitionBundle, + solve_policy_definition_bundle: DefinitionBundle, + value_schema_definitions: tuple[ValueSchemaDefinition, ...], + predicate_definitions: tuple[PredicateDefinition, ...], + state_variable_definitions: tuple[StateVariableDefinition, ...], + derived_fact_rule_definitions: tuple[DerivedFactRuleDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], + implementation_registry_snapshot: ImplementationRegistrySnapshot, + problem: CounterfactualProblemIR, + semantics_profile: SemanticsProfile, + action_space_profile: ActionSpaceProfile, + scene_state: SceneStateEnvelope, + request: CounterfactualSolveRequest, + backend_descriptor_bundle: BackendDescriptorBundle, + solver_config: CounterfactualSolverConfig, + proof_policy: ProofPolicy, + resource_policy: ResourcePolicy, + backend_routing_policy: BackendRoutingPolicy, + ) -> CounterfactualSolveRequest: + """Validate operational policy and static backend snapshot closure.""" + + if ( + not isinstance( + getattr(action_space_profile, "backend_capability_requirements", None), + tuple, + ) + or not action_space_profile.backend_capability_requirements + ): + raise SemanticContractError("backend capability requirements") + if ( + not isinstance( + getattr(backend_descriptor_bundle, "backend_descriptors", None), tuple + ) + or not backend_descriptor_bundle.backend_descriptors + ): + raise SemanticContractError("available backend descriptors") + if request.implementation_registry_snapshot != implementation_registry_snapshot: + raise ImplementationResolutionError("registry snapshot") + self.validate_semantic_problem( + semantic_definition_bundle, + solve_policy_definition_bundle, + value_schema_definitions, + predicate_definitions, + state_variable_definitions, + derived_fact_rule_definitions, + operator_definitions, + implementation_registry_snapshot, + problem, + semantics_profile, + action_space_profile, + scene_state, + ) + if request.semantic_problem != problem or ( + request.semantic_problem_sha256 != problem.semantic_problem_sha256 + ): + raise SemanticContractError("solve request semantic problem") + if request.solve_policy_definition_bundle != solve_policy_definition_bundle: + raise DefinitionClosureError("solve policy definition bundle") + if request.backend_descriptor_bundle != backend_descriptor_bundle: + raise SemanticContractError("backend descriptor bundle") + if request.solver_config != solver_config: + raise SemanticContractError("solver config") + if request.proof_policy != proof_policy: + raise SemanticContractError("proof policy") + if request.resource_policy != resource_policy: + raise SemanticContractError("resource policy") + if request.backend_routing_policy != backend_routing_policy: + raise SemanticContractError("backend routing policy") + for record, reason in ( + (request, "solve request hash"), + (backend_descriptor_bundle, "backend descriptor bundle hash"), + (solver_config, "solver config hash"), + (proof_policy, "proof policy hash"), + (resource_policy, "resource policy hash"), + (backend_routing_policy, "backend routing policy hash"), + (semantics_profile, "semantics profile hash"), + (action_space_profile, "action profile hash"), + ): + if not _self_digest_matches(record): + raise SemanticContractError(reason) + _semantic_definitions, _solve_definitions, definitions = _definition_root_maps( + semantic_definition_bundle, + solve_policy_definition_bundle, + ) + policy_records = ( + solver_config, + proof_policy, + resource_policy, + backend_routing_policy, + ) + if ( + not { + reference + for record in policy_records + for reference in _references(record, "definition:") + } + <= definitions.keys() + ): + raise DefinitionClosureError("solve policy definition closure") + operational_policy_refs = ( + _references(solver_config, "definition:") + | _references(resource_policy, "definition:") + | _references(backend_routing_policy, "definition:") + | {proof_policy.proof_policy_ref} + ) + if not operational_policy_refs <= _solve_definitions.keys(): + raise DefinitionClosureError("solve policy definition root") + if ( + not { + *proof_policy.accepted_claim_definition_refs, + proof_policy.publication_minimum_claim_ref, + } + <= _semantic_definitions.keys() + ): + raise DefinitionClosureError("semantic claim definition root") + policy_roles = _definition_roles(definitions) + solve_roles = _definition_roles(_solve_definitions) + _validate_exact_root_definition_closure( + _solve_definitions, + root_records=( + solver_config, + proof_policy, + resource_policy, + backend_routing_policy, + backend_descriptor_bundle, + ), + record_binding_targets={ + reference + for reference, role in solve_roles.items() + if role + in { + _ROLE_ROUTING_SELECTION_DISPOSITION, + _ROLE_ROUTING_SELECTION_REASON, + } + }, + root_label="solve policy", + ) + try: + resource_accounting_ref = _definition_record_reference( + _solve_definitions[resource_policy.resource_policy_ref], + _RESOURCE_ACCOUNTING_CLAIM_FIELD, + ) + except (DefinitionClosureError, KeyError) as error: + raise DefinitionClosureError("resource policy accounting") from error + if ( + solve_roles.get(resource_policy.resource_policy_ref) + != _ROLE_RESOURCE_POLICY + or solve_roles.get(resource_accounting_ref) != _ROLE_RESOURCE_ACCOUNTING + ): + raise DefinitionClosureError("resource policy accounting") + try: + routing_definition = _solve_definitions[ + backend_routing_policy.routing_policy_ref + ] + routing_match_ref = _definition_record_reference( + routing_definition, + "field:routing-match-claim", + ) + routing_mismatch_ref = _definition_record_reference( + routing_definition, + "field:routing-mismatch-claim", + ) + except (DefinitionClosureError, KeyError) as error: + raise DefinitionClosureError("routing policy semantics") from error + if ( + solve_roles.get(backend_routing_policy.routing_policy_ref) + != _ROLE_ROUTING_POLICY + or solve_roles.get(routing_match_ref) != _ROLE_ROUTING_MATCH + or solve_roles.get(routing_mismatch_ref) != _ROLE_ROUTING_MISMATCH + ): + raise DefinitionClosureError("routing policy semantics") + accepted_claim_definition_refs = set( + proof_policy.accepted_claim_definition_refs + ) + if ( + proof_policy.publication_minimum_claim_ref + not in accepted_claim_definition_refs + ): + raise SemanticContractError("proof policy publication minimum") + checker_capabilities = set(proof_policy.required_checker_capability_refs) + for claim_ref in proof_policy.accepted_claim_definition_refs: + try: + claim_definition = _semantic_definitions[claim_ref] + proof_material_ref = _definition_record_reference( + claim_definition, + _CLAIM_PROOF_MATERIAL_FIELD, + ) + claim_checker_capability = _definition_record_reference( + claim_definition, + _CLAIM_CHECKER_CAPABILITY_FIELD, + ) + proof_material_definition = _semantic_definitions[proof_material_ref] + proof_material_checker_capability = _definition_record_reference( + proof_material_definition, + _PROOF_CHECKER_CAPABILITY_FIELD, + ) + except (DefinitionClosureError, KeyError) as error: + raise DefinitionClosureError("proof policy claim metadata") from error + if ( + policy_roles.get(proof_material_ref) != _ROLE_PROOF_MATERIAL + or claim_checker_capability != proof_material_checker_capability + or claim_checker_capability not in checker_capabilities + or proof_material_checker_capability not in checker_capabilities + ): + raise SemanticContractError("proof policy checker") + if ( + proof_policy.proof_policy_ref + != action_space_profile.publication_proof_policy_ref + or not set(proof_policy.accepted_claim_definition_refs) + <= set(action_space_profile.allowed_claim_definition_refs) + or proof_policy.publication_minimum_claim_ref + not in action_space_profile.allowed_claim_definition_refs + or any( + policy_roles.get(reference) + not in {_ROLE_CERTIFIED_SOLUTION, _ROLE_PROVEN_UNSAT} + for reference in proof_policy.accepted_claim_definition_refs + ) + or policy_roles.get(proof_policy.publication_minimum_claim_ref) + not in {_ROLE_CERTIFIED_SOLUTION, _ROLE_PROVEN_UNSAT} + ): + raise SemanticContractError("proof policy action profile") + capability_owners = self._owners_by_capability() + backend_capabilities = set(action_space_profile.backend_capability_requirements) + for capability in backend_capabilities | checker_capabilities: + if capability not in capability_owners: + raise ImplementationResolutionError("capability owner") + self._validate_snapshot( + implementation_registry_snapshot, + backend_capabilities | checker_capabilities, + ( + *predicate_definitions, + *state_variable_definitions, + *derived_fact_rule_definitions, + *operator_definitions, + ), + ) + backend_owner_by_capability = { + capability: capability_owners[capability] + for capability in backend_capabilities + } + available_backend_refs = { + descriptor.backend_ref + for descriptor in backend_descriptor_bundle.backend_descriptors + } + unavailable_backend_refs = { + unavailable.backend_ref + for unavailable in backend_descriptor_bundle.unavailable_optional_backends + } + # The domain model normally enforces this too. Keep the registry + # boundary defensive because tests and callers can construct frozen + # models without normal validation. + if available_backend_refs & unavailable_backend_refs: + raise DefinitionClosureError("unavailable backend universe") + descriptor_owner_refs: set[str] = set() + for descriptor in backend_descriptor_bundle.backend_descriptors: + if not _self_digest_matches(descriptor): + raise SemanticContractError("backend descriptor hash") + if not _references(descriptor, "definition:") <= definitions.keys(): + raise DefinitionClosureError("backend descriptor definition closure") + descriptor_capabilities = _references(descriptor, "capability:") + if not descriptor_capabilities <= capability_owners.keys(): + raise ImplementationResolutionError("backend descriptor capability") + descriptor_owners = tuple( + sorted( + ( + owner + for owner in set(backend_owner_by_capability.values()) + if owner.implementation_build_sha256 + == descriptor.implementation_build_sha256 + ), + key=lambda owner: _ref_key(owner.owner_ref), + ) + ) + # The wire exposes a descriptor build but no owner ref. Refuse an + # ambiguous build rather than selecting an arbitrary set member; + # separate descriptor rows are the explicit portfolio mechanism. + if len(descriptor_owners) != 1: + raise ImplementationResolutionError("backend descriptor build") + descriptor_owner_refs.add(descriptor_owners[0].owner_ref) + for unavailable in backend_descriptor_bundle.unavailable_optional_backends: + if policy_roles.get(unavailable.reason_claim_definition_ref) not in { + _ROLE_UNKNOWN, + _ROLE_ROUTING_MISMATCH, + }: + raise DefinitionClosureError("unavailable backend reason") + if ( + available_backend_refs + and not {owner.owner_ref for owner in backend_owner_by_capability.values()} + <= descriptor_owner_refs + ): + raise ImplementationResolutionError("backend descriptor build") + return request + + def validate_edit_program( + self, + semantic_definition_bundle: DefinitionBundle, + solve_policy_definition_bundle: DefinitionBundle, + value_schema_definitions: tuple[ValueSchemaDefinition, ...], + predicate_definitions: tuple[PredicateDefinition, ...], + state_variable_definitions: tuple[StateVariableDefinition, ...], + derived_fact_rule_definitions: tuple[DerivedFactRuleDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], + implementation_registry_snapshot: ImplementationRegistrySnapshot, + problem: CounterfactualProblemIR, + semantics_profile: SemanticsProfile, + action_space_profile: ActionSpaceProfile, + scene_state: SceneStateEnvelope, + program: EditProgram, + before_state: SceneStateEnvelope, + after_state: SceneStateEnvelope, + grounded_obligations: GroundedObligationSet, + intervention_authorization: InterventionAuthorization, + ) -> EditProgram: + """Reconstruct the complete state partition for one explicit edit program.""" + + self.validate_semantic_problem( + semantic_definition_bundle, + solve_policy_definition_bundle, + value_schema_definitions, + predicate_definitions, + state_variable_definitions, + derived_fact_rule_definitions, + operator_definitions, + implementation_registry_snapshot, + problem, + semantics_profile, + action_space_profile, + scene_state, + ) + if intervention_authorization != problem.intervention_authorization: + raise SemanticContractError("intervention authorization") + if before_state != problem.scene_state: + raise SemanticContractError("program before scene") + try: + before_base_scene = _validated_base_scene_payload( + before_state.base_scene_payload + ) + except (TypeError, ValidationError, ValueError) as error: + raise SemanticContractError("program before scene") from error + if ( + program.semantic_problem_sha256 != problem.semantic_problem_sha256 + or program.action_space_profile_sha256 + != action_space_profile.action_space_profile_sha256 + ): + raise SemanticContractError("program roots") + if ( + program.before_state_sha256 != before_state.scene_state_sha256 + or program.after_scene_state != after_state + or program.after_scene_state_sha256 != after_state.scene_state_sha256 + ): + raise SemanticContractError("program state") + if after_state.base_scene_schema_ref != scene_state.base_scene_schema_ref: + raise SemanticContractError("complete after state") + if ( + program.grounded_obligation_set_sha256 + != grounded_obligations.grounded_obligation_set_sha256 + ): + raise SemanticContractError("program obligations") + + definitions, _solve_definitions, _all_definitions = _definition_root_maps( + semantic_definition_bundle, + solve_policy_definition_bundle, + ) + _, after_values, after_base_scene = _validate_scene_state_envelope( + after_state, + state_variable_definitions, + value_schema_definitions, + definitions, + after_state=True, + ) + + manifest = program.state_delta_manifest + primary_keys = {_state_key(leaf) for leaf in manifest.authorized_primary_writes} + derived_keys = {_state_key(leaf) for leaf in manifest.recomputed_derived_writes} + if primary_keys & derived_keys: + raise SemanticContractError("primary/derived") + before_leaves = { + _state_key(leaf): leaf + for leaf in before_state.canonical_state_leaf_index.leaves + } + after_leaves = { + _state_key(leaf): leaf + for leaf in after_state.canonical_state_leaf_index.leaves + } + complete_keys = set(before_leaves) | set(after_leaves) + state_by_schema = { + definition.state_variable_schema_ref: definition + for definition in state_variable_definitions + } + metadata_by_ref = _state_definition_metadata(definitions) + expected_after_addresses = { + ( + metadata[0], + metadata[1], + metadata[2], + metadata[3], + metadata[4], + ) + for metadata in metadata_by_ref.values() + } + actual_after_addresses = { + ( + leaf.state_variable_schema_ref, + leaf.state_schema_ref, + leaf.fact_family_ref, + leaf.entity_or_fact_key, + leaf.field_path_ref, + ) + for leaf in after_leaves.values() + } + if actual_after_addresses != expected_after_addresses: + raise SemanticContractError("complete after state") + if { + (leaf.fact_family_ref, leaf.entity_or_fact_key, leaf.field_path_ref) + for leaf in after_leaves.values() + if ( + leaf.fact_family_ref, + leaf.entity_or_fact_key, + ) + in { + (family, identifier) + for family, identifier, _fact in _base_fact_rows(after_base_scene) + } + } != _expected_base_leaf_addresses(after_base_scene): + raise SemanticContractError("complete after state") + after_base_owners = { + (family, identifier) + for family, identifier, _fact in _base_fact_rows(after_base_scene) + } + after_extension_facts = _extension_facts_by_address(after_state) + absent_after_extension_addresses = set( + _declared_extension_leaf_owners( + tuple(after_leaves.values()), + after_base_owners, + ) + ) - set(after_extension_facts) + schemas = { + schema.value_schema_ref: schema for schema in value_schema_definitions + } + after_definitions_by_leaf: dict[bytes, StateVariableDefinition] = {} + for leaf in after_leaves.values(): + state_definition = state_by_schema.get(leaf.state_variable_schema_ref) + if state_definition is None: + raise SemanticContractError("complete after state") + after_definitions_by_leaf[_state_key(leaf)] = state_definition + try: + _validate_state_leaf_value_wires( + tuple(after_leaves.values()), + after_values, + after_definitions_by_leaf, + schemas, + set(after_extension_facts), + absent_after_extension_addresses, + ) + except DefinitionClosureError as error: + raise SemanticContractError("complete after state") from error + if not (primary_keys | derived_keys) <= complete_keys: + raise SemanticContractError("complete delta partition") + authorized_keys = { + _state_key(leaf) + for leaf in intervention_authorization.authorized_primary_write_set + } + if not primary_keys <= authorized_keys: + raise SemanticContractError("authorization") + output_owners: dict[bytes, str] = {} + for rule in derived_fact_rule_definitions: + if ( + rule.derived_fact_rule_ref + not in intervention_authorization.required_derived_rule_refs + ): + continue + for leaf in rule.fixed_output_set: + key = _state_key(leaf) + if key in output_owners: + raise SemanticContractError("derived output owner") + output_owners[key] = rule.derived_fact_rule_ref + rule_outputs = set(output_owners) + if derived_keys != rule_outputs: + raise SemanticContractError("derived footprint") + before_values = _leaf_values(before_state, before_base_scene) + changed = { + key + for key in complete_keys + if canonical_json_bytes(before_values.get(key)) + != canonical_json_bytes(after_values.get(key)) + } + if changed != primary_keys | derived_keys: + raise SemanticContractError("complete delta partition") + ordered_union_keys = tuple( + _state_key(leaf) for leaf in before_state.canonical_state_leaf_index.leaves + ) + tuple( + key for key in sorted(set(after_leaves) - set(before_leaves), key=_ref_key) + ) + unchanged_rows = tuple( + ( + (before_leaves[key] if key in before_leaves else after_leaves[key]), + before_values.get(key), + ) + for key in ordered_union_keys + if key not in changed + and canonical_json_bytes(before_values.get(key)) + == canonical_json_bytes(after_values.get(key)) + ) + if manifest.unchanged_leaves_digest != canonical_sha256( + unchanged_rows, + domain=_UNCHANGED_LEAF_DOMAIN, + ): + raise SemanticContractError("unchanged-leaf digest") + if ( + manifest.complete_before_leaf_index_sha256 + != before_state.canonical_state_leaf_index.state_leaf_index_sha256 + or manifest.complete_after_leaf_index_sha256 + != after_state.canonical_state_leaf_index.state_leaf_index_sha256 + ): + raise SemanticContractError("complete leaf index") + operators = { + definition.operator_ref: definition for definition in operator_definitions + } + if len(program.steps) > intervention_authorization.maximum_program_steps: + raise SemanticContractError("program steps") + problem_precondition_bytes = { + canonical_json_bytes(precondition) + for precondition in problem.before_preconditions + } + primary_footprint_definition_refs: set[str] = set() + derived_rule_refs: set[str] = set() + for step in program.steps: + definition = operators.get(step.operator_ref) + if ( + definition is None + or step.operator_ref + not in intervention_authorization.allowed_operator_refs + ): + raise SemanticContractError("authorization") + if ( + not { + canonical_json_bytes(precondition) + for precondition in definition.required_preconditions + } + <= problem_precondition_bytes + ): + raise SemanticContractError("operator required precondition") + if len(step.arguments) != len(definition.parameter_schema_refs): + raise SemanticContractError("operator parameters") + if ( + tuple(argument.value.value_schema_ref for argument in step.arguments) + != definition.parameter_schema_refs + ): + raise SemanticContractError("operator parameters") + for argument in step.arguments: + try: + _validate_typed_value(argument.value, schemas) + except DefinitionClosureError as error: + raise SemanticContractError("operator parameters") from error + arguments_by_name = { + argument.argument_name: argument for argument in step.arguments + } + for pattern in ( + *definition.read_footprint, + *definition.primary_write_footprint, + ): + for binding in pattern.parameter_bindings: + argument = arguments_by_name.get(binding.parameter_ref) + if ( + argument is None + or argument.value.value_schema_ref + != binding.parameter_schema_ref + ): + raise SemanticContractError("operator parameter binding") + primary_footprint_definition_refs.update( + pattern.state_variable_definition_ref + for pattern in definition.primary_write_footprint + ) + derived_rule_refs.update(definition.derived_write_rule_refs) + if not { + pattern.state_variable_definition_ref + for pattern in definition.read_footprint + } <= { + state_definition.state_variable_ref + for state_definition in state_by_schema.values() + }: + raise SemanticContractError("operator footprint") + if ( + not set(intervention_authorization.required_derived_rule_refs) + <= derived_rule_refs + ): + raise SemanticContractError("derived footprint") + if not derived_rule_refs <= set( + intervention_authorization.required_derived_rule_refs + ): + raise SemanticContractError("authorization derived footprint") + actual_primary_footprint = { + key + for key, leaf in ({**before_leaves, **after_leaves}).items() + if state_by_schema[leaf.state_variable_schema_ref].state_variable_ref + in primary_footprint_definition_refs + } + if not actual_primary_footprint <= authorized_keys: + raise SemanticContractError("authorization operator footprint") + if not primary_keys <= actual_primary_footprint: + raise SemanticContractError("operator footprint") + extension_subjects = { + address: fact.subject_entity_id + for state in (before_state, after_state) + for address, fact in _extension_facts_by_address(state).items() + } + edited_entities = { + extension_subjects.get( + ( + (before_leaves.get(key) or after_leaves[key]).fact_family_ref, + (before_leaves.get(key) or after_leaves[key]).entity_or_fact_key, + ), + (before_leaves.get(key) or after_leaves[key]).entity_or_fact_key, + ) + for key in primary_keys + } + if len(edited_entities) > intervention_authorization.maximum_edited_entities: + raise SemanticContractError("authorization") + if not _self_digest_matches(grounded_obligations): + raise SemanticContractError("grounded obligations") + if not set(grounded_obligations.source_definition_refs) <= definitions.keys(): + raise SemanticContractError("grounded obligations") + partitions = ( + (grounded_obligations.before_preconditions, problem.before_preconditions), + (grounded_obligations.after_goals, (problem.after_goal,)), + ( + grounded_obligations.preservation_invariants, + problem.preservation_invariants, + ), + ( + grounded_obligations.observation_obligations, + problem.explicit_observation_obligations, + ), + ) + if any( + {canonical_json_bytes(item.context) for item in grounded_partition} + != {canonical_json_bytes(item) for item in semantic_partition} + for grounded_partition, semantic_partition in partitions + ): + raise SemanticContractError("grounded obligations") + if any( + canonical_json_bytes(obligation.context) + not in { + canonical_json_bytes(item.context) + for item in grounded_obligations.after_goals + } + for definition in (operators[step.operator_ref] for step in program.steps) + for obligation in definition.generated_obligations + ): + raise SemanticContractError("grounded obligations") + if not _self_digest_matches(manifest) or not _self_digest_matches(program): + raise SemanticContractError("program hash") + return program + + def validate_outcome_contract( + self, + semantic_definition_bundle: DefinitionBundle, + solve_policy_definition_bundle: DefinitionBundle, + value_schema_definitions: tuple[ValueSchemaDefinition, ...], + predicate_definitions: tuple[PredicateDefinition, ...], + state_variable_definitions: tuple[StateVariableDefinition, ...], + derived_fact_rule_definitions: tuple[DerivedFactRuleDefinition, ...], + operator_definitions: tuple[OperatorDefinition, ...], + implementation_registry_snapshot: ImplementationRegistrySnapshot, + problem: CounterfactualProblemIR, + semantics_profile: SemanticsProfile, + action_space_profile: ActionSpaceProfile, + scene_state: SceneStateEnvelope, + request: CounterfactualSolveRequest, + backend_descriptor_bundle: BackendDescriptorBundle, + solver_config: CounterfactualSolverConfig, + proof_policy: ProofPolicy, + resource_policy: ResourcePolicy, + backend_routing_policy: BackendRoutingPolicy, + selection: BackendSelectionRecord, + proposal: BackendProposal | None, + proof_material: ProofMaterialEnvelope | None, + checked_proof_outcome: CheckedProofOutcome | None, + verifier_dispatch_record: VerifierDispatchRecord | None, + certificate: CertifiedSolutionCertificate | ProvenUnsatCertificate | None, + result: ( + CertifiedSolutionResult + | ProvenUnsatResult + | NoncertifiedWitnessResult + | UnknownResult + ), + program: EditProgram | None, + grounded_obligations: GroundedObligationSet | None, + ) -> ( + CertifiedSolutionResult + | ProvenUnsatResult + | NoncertifiedWitnessResult + | UnknownResult + ): + """Validate the submitted, branch-specific hash DAG without execution. + + The method accepts all four structural terminal envelopes. A weak + branch is admissible as a weak branch when policy permits it; only a + certificate or complete-domain UNSAT branch may claim trusted strength. + """ + + self.validate_solve_request( + semantic_definition_bundle, + solve_policy_definition_bundle, + value_schema_definitions, + predicate_definitions, + state_variable_definitions, + derived_fact_rule_definitions, + operator_definitions, + implementation_registry_snapshot, + problem, + semantics_profile, + action_space_profile, + scene_state, + request, + backend_descriptor_bundle, + solver_config, + proof_policy, + resource_policy, + backend_routing_policy, + ) + for record in ( + selection, + proposal, + proof_material, + checked_proof_outcome, + verifier_dispatch_record, + result, + ): + if record is not None and not _self_digest_matches(record): + raise SemanticContractError("outcome record hash") + if certificate is not None and not _self_digest_matches(certificate): + raise SemanticContractError("certificate hash") + if ( + result.semantic_problem_sha256 != problem.semantic_problem_sha256 + or result.solve_request_sha256 != request.solve_request_sha256 + ): + raise SemanticContractError("result roots") + if ( + selection.semantic_problem_sha256 != problem.semantic_problem_sha256 + or selection.solve_request_sha256 != request.solve_request_sha256 + or selection.implementation_registry_snapshot_sha256 + != implementation_registry_snapshot.implementation_registry_snapshot_sha256 + or selection.backend_descriptor_bundle_sha256 + != backend_descriptor_bundle.backend_descriptor_bundle_sha256 + or selection.backend_routing_policy_sha256 + != backend_routing_policy.backend_routing_policy_sha256 + ): + raise SemanticContractError("selection roots") + + _semantic_definitions, _solve_definitions, definitions = _definition_root_maps( + semantic_definition_bundle, + solve_policy_definition_bundle, + ) + roles = _definition_roles(definitions) + available_backend_refs = { + descriptor.backend_ref + for descriptor in backend_descriptor_bundle.backend_descriptors + } + unavailable_backend_refs = { + unavailable.backend_ref + for unavailable in backend_descriptor_bundle.unavailable_optional_backends + } + if not available_backend_refs or ( + available_backend_refs & unavailable_backend_refs + ): + # Task 7 has no descriptor digest field for an unavailable row, so + # a nonempty BackendSelectionRecord cannot safely represent an + # unavailable-only universe. It must terminate fail-closed rather + # than fabricate a CapabilityMismatch. + raise SemanticContractError("unavailable backend selection") + if ( + set(selection.ordered_candidate_backend_refs) & unavailable_backend_refs + or selection.selected_backend_ref in unavailable_backend_refs + ): + raise SemanticContractError("unavailable backend selection") + expected_rows = _reconstructed_backend_rows( + request, + action_space_profile, + semantics_profile, + predicate_definitions, + operator_definitions, + definitions, + roles, + ) + if ( + set(selection.ordered_candidate_backend_refs) != available_backend_refs + or selection.ordered_candidate_backend_refs + != tuple(row.backend_ref for row in expected_rows) + or canonical_json_bytes(selection.capability_rows) + != canonical_json_bytes(expected_rows) + ): + raise SemanticContractError("ordered backend candidates") + if ( + result.backend_selection_record_sha256 + != selection.backend_selection_record_sha256 + ): + raise SemanticContractError("result roots") + if ( + roles.get(selection.selection_disposition_claim_ref) + != _ROLE_ROUTING_SELECTION_DISPOSITION + or roles.get(selection.deterministic_selection_reason_ref) + != _ROLE_ROUTING_SELECTION_REASON + ): + raise SemanticContractError("selection definition closure") + descriptor_by_ref = { + descriptor.backend_ref: descriptor + for descriptor in backend_descriptor_bundle.backend_descriptors + } + matching_rows = tuple( + row for row in expected_rows if isinstance(row, CapabilityMatch) + ) + if selection.selection_disposition == "NO_SELECTION": + if matching_rows: + raise SemanticContractError("deterministic selected backend") + if any( + item is not None + for item in ( + proposal, + proof_material, + checked_proof_outcome, + verifier_dispatch_record, + certificate, + program, + grounded_obligations, + ) + ) or not isinstance(result, UnknownResult): + raise SemanticContractError("no-selection outcome") + if ( + result.checked_proof_outcome_sha256 is not None + or result.verifier_dispatch_record_sha256 is not None + or result.checker_disposition is not None + ): + raise SemanticContractError("no-selection checker") + _require_outcome_definition_role( + roles, + result.claim_definition_ref, + (_ROLE_UNKNOWN,), + "claim admissibility", + ) + _require_outcome_definition_role( + roles, + result.reason_claim_definition_ref, + (_ROLE_UNKNOWN,), + "unknown reason admissibility", + ) + if ( + result.claim_definition_ref + not in action_space_profile.allowed_claim_definition_refs + or result.reason_claim_definition_ref + not in action_space_profile.allowed_claim_definition_refs + ): + raise SemanticContractError("unknown claim admissibility") + _validate_resource_usage( + result.resource_usage, resource_policy, definitions + ) + return result + if selection.selection_disposition != "SELECTED": + raise SemanticContractError("selection disposition") + if ( + selection.selected_backend_ref is None + or selection.selected_backend_descriptor_sha256 is None + or selection.selected_backend_ref not in descriptor_by_ref + or descriptor_by_ref[ + selection.selected_backend_ref + ].backend_descriptor_sha256 + != selection.selected_backend_descriptor_sha256 + ): + raise SemanticContractError("selected backend descriptor") + selected_row = next( + ( + row + for row in expected_rows + if row.backend_ref == selection.selected_backend_ref + ), + None, + ) + if not isinstance(selected_row, CapabilityMatch): + raise SemanticContractError("selected backend capability") + if not matching_rows or selected_row != matching_rows[0]: + raise SemanticContractError("deterministic selected backend") + descriptor = descriptor_by_ref[selection.selected_backend_ref] + + if proposal is None or proof_material is None: + raise SemanticContractError("selected proposal presence") + + if ( + proposal.semantic_problem_sha256 != problem.semantic_problem_sha256 + or proposal.solve_request_sha256 != request.solve_request_sha256 + or proposal.backend_selection_record_sha256 + != selection.backend_selection_record_sha256 + or proposal.proposal_backend_ref != selection.selected_backend_ref + or proposal.proof_material_sha256 != proof_material.proof_material_sha256 + ): + raise SemanticContractError("proposal roots") + if ( + proof_material.semantic_problem_sha256 != problem.semantic_problem_sha256 + or proof_material.solve_request_sha256 != request.solve_request_sha256 + or proof_material.backend_selection_record_sha256 + != selection.backend_selection_record_sha256 + or proof_material.proposal_backend_ref != selection.selected_backend_ref + or proof_material.proof_material_definition_ref + not in descriptor.emitted_proof_material_definition_refs + ): + raise SemanticContractError("proof material roots") + schemas = { + schema.value_schema_ref: schema for schema in value_schema_definitions + } + if any( + value.value_schema_ref != proof_material.payload_schema_ref + for value in proof_material.typed_payload + ): + raise SemanticContractError("proof material schema") + try: + for value in proof_material.typed_payload: + _validate_typed_value(value, schemas) + except DefinitionClosureError as error: + raise SemanticContractError("proof material schema") from error + if proposal.proposal_claim_definition_ref != result.claim_definition_ref: + raise SemanticContractError("proposal claim") + if isinstance(result, CertifiedSolutionResult) and ( + program is None + or proposal.program_sha256 != program.program_sha256 + or proposal.after_scene_state_sha256 != program.after_scene_state_sha256 + ): + raise SemanticContractError("proposal program") + capability_owners = self._owners_by_capability() + proposal_owner = capability_owners.get(proposal.proposal_backend_capability_ref) + if ( + proposal_owner is None + or proposal_owner.owner_ref != proposal.proposal_backend_owner_ref + or proposal_owner.implementation_build_sha256 + != proposal.proposal_backend_build_sha256 + or descriptor.implementation_build_sha256 + != proposal.proposal_backend_build_sha256 + or proposal.proposal_backend_capability_ref + not in action_space_profile.backend_capability_requirements + ): + raise ImplementationResolutionError("proposal backend owner/build") + result_has_checker = result.checked_proof_outcome_sha256 is not None + if (checked_proof_outcome is None) != ( + verifier_dispatch_record is None + ) or result_has_checker != (checked_proof_outcome is not None): + raise SemanticContractError("checker pair") + checker_owner: StaticOwner | None = None + if checked_proof_outcome is not None: + assert verifier_dispatch_record is not None + checker_owner = capability_owners.get( + checked_proof_outcome.checker_capability_ref + ) + if ( + checker_owner is None + or checker_owner.implementation_build_sha256 + != checked_proof_outcome.checker_build_sha256 + or checker_owner.owner_ref == proposal_owner.owner_ref + or checked_proof_outcome.checker_capability_ref + not in descriptor.compatible_checker_capability_refs + or checked_proof_outcome.checker_capability_ref + not in proof_policy.required_checker_capability_refs + ): + raise ImplementationResolutionError("checker owner/build") + if ( + checked_proof_outcome.semantic_problem_sha256 + != problem.semantic_problem_sha256 + or checked_proof_outcome.solve_request_sha256 + != request.solve_request_sha256 + or checked_proof_outcome.backend_selection_record_sha256 + != selection.backend_selection_record_sha256 + or checked_proof_outcome.proof_material_sha256 + != proof_material.proof_material_sha256 + or checked_proof_outcome.checked_claim_definition_ref + != proposal.proposal_claim_definition_ref + or result.checked_proof_outcome_sha256 + != checked_proof_outcome.checked_proof_outcome_sha256 + or result.verifier_dispatch_record_sha256 + != verifier_dispatch_record.verifier_dispatch_record_sha256 + or result.checker_disposition + != checked_proof_outcome.checker_disposition + ): + raise SemanticContractError("checked proof roots") + if ( + verifier_dispatch_record.semantic_problem_sha256 + != problem.semantic_problem_sha256 + or verifier_dispatch_record.solve_request_sha256 + != request.solve_request_sha256 + or verifier_dispatch_record.semantic_definition_bundle_sha256 + != semantic_definition_bundle.definition_bundle_sha256 + or verifier_dispatch_record.solve_policy_definition_bundle_sha256 + != solve_policy_definition_bundle.definition_bundle_sha256 + or verifier_dispatch_record.backend_selection_record_sha256 + != selection.backend_selection_record_sha256 + or verifier_dispatch_record.checked_proof_outcome_sha256 + != checked_proof_outcome.checked_proof_outcome_sha256 + or verifier_dispatch_record.proof_policy_sha256 + != proof_policy.proof_policy_sha256 + or verifier_dispatch_record.proposal_backend_owner_ref + != proposal.proposal_backend_owner_ref + or verifier_dispatch_record.proposal_backend_capability_ref + != proposal.proposal_backend_capability_ref + or verifier_dispatch_record.proposal_backend_build_sha256 + != proposal.proposal_backend_build_sha256 + or verifier_dispatch_record.proof_material_definition_ref + != proof_material.proof_material_definition_ref + or verifier_dispatch_record.checker_owner_ref != checker_owner.owner_ref + or verifier_dispatch_record.checker_capability_ref + != checked_proof_outcome.checker_capability_ref + or verifier_dispatch_record.checker_build_sha256 + != checked_proof_outcome.checker_build_sha256 + ): + raise SemanticContractError("verifier dispatch roots") + + for usage in ( + selection.resource_allocation, + proposal.resource_usage, + result.resource_usage, + certificate.resource_usage if certificate is not None else None, + ): + if usage is not None: + _validate_resource_usage(usage, resource_policy, definitions) + _require_outcome_definition_role( + roles, + proof_material.proof_material_definition_ref, + (_ROLE_PROOF_MATERIAL,), + "proof material admissibility", + ) + proof_definition = definitions[proof_material.proof_material_definition_ref] + if ( + _definition_record_reference( + proof_definition, + _PROOF_PAYLOAD_SCHEMA_FIELD, + ) + != proof_material.payload_schema_ref + ): + raise SemanticContractError("proof material schema") + if ( + checked_proof_outcome is not None + and _definition_record_reference( + proof_definition, + _PROOF_CHECKER_CAPABILITY_FIELD, + ) + != checked_proof_outcome.checker_capability_ref + ): + raise SemanticContractError("proof material checker") + + if isinstance(result, CertifiedSolutionResult): + if not isinstance(certificate, CertifiedSolutionCertificate): + raise SemanticContractError("certificate branch") + if program is None or grounded_obligations is None: + raise SemanticContractError("certificate program") + if checked_proof_outcome is None or verifier_dispatch_record is None: + raise SemanticContractError("certificate checker") + self.validate_edit_program( + semantic_definition_bundle, + solve_policy_definition_bundle, + value_schema_definitions, + predicate_definitions, + state_variable_definitions, + derived_fact_rule_definitions, + operator_definitions, + implementation_registry_snapshot, + problem, + semantics_profile, + action_space_profile, + scene_state, + program, + scene_state, + program.after_scene_state, + grounded_obligations, + problem.intervention_authorization, + ) + _require_outcome_definition_role( + roles, + certificate.claim_definition_ref, + (_ROLE_CERTIFIED_SOLUTION,), + "claim admissibility", + ) + claim_definition = definitions[certificate.claim_definition_ref] + if ( + _definition_record_reference( + claim_definition, + _CLAIM_PROOF_MATERIAL_FIELD, + ) + != proof_material.proof_material_definition_ref + or _definition_record_reference( + claim_definition, + _CLAIM_CHECKER_CAPABILITY_FIELD, + ) + != checked_proof_outcome.checker_capability_ref + ): + raise SemanticContractError("claim admissibility") + if ( + certificate.proof_material_definition_ref + != proof_material.proof_material_definition_ref + or certificate.proof_material_definition_ref + != _definition_record_reference( + claim_definition, + _CLAIM_PROOF_MATERIAL_FIELD, + ) + ): + raise SemanticContractError("certificate proof material") + if ( + certificate != result.accepted_certificate + or certificate.claim_definition_ref + != proposal.proposal_claim_definition_ref + or certificate.claim_definition_ref + != checked_proof_outcome.checked_claim_definition_ref + or certificate.claim_definition_ref != result.claim_definition_ref + or certificate.claim_definition_ref + not in proof_policy.accepted_claim_definition_refs + or certificate.claim_definition_ref + not in action_space_profile.allowed_claim_definition_refs + or certificate.checker_disposition is not CheckerDisposition.ACCEPTED + or checked_proof_outcome.checker_disposition + is not CheckerDisposition.ACCEPTED + or certificate.program_sha256 != program.program_sha256 + or certificate.after_scene_state_sha256 + != program.after_scene_state_sha256 + or certificate.state_delta_manifest_sha256 + != program.state_delta_manifest.state_delta_manifest_sha256 + or certificate.grounded_obligation_set_sha256 + != grounded_obligations.grounded_obligation_set_sha256 + or result.certificate_sha256 != certificate.certificate_sha256 + or result.program_sha256 != program.program_sha256 + or result.after_scene_state_sha256 != program.after_scene_state_sha256 + ): + raise SemanticContractError("certificate admissibility") + elif isinstance(result, ProvenUnsatResult): + if not isinstance(certificate, ProvenUnsatCertificate): + raise SemanticContractError("complete-domain certificate") + if program is not None or grounded_obligations is not None: + raise SemanticContractError("unsat program presence") + if checked_proof_outcome is None or verifier_dispatch_record is None: + raise SemanticContractError("complete-domain checker") + _require_outcome_definition_role( + roles, + certificate.claim_definition_ref, + (_ROLE_PROVEN_UNSAT,), + "claim admissibility", + ) + _require_outcome_definition_role( + roles, + certificate.complete_domain_claim_definition_ref, + (_ROLE_COMPLETE_DOMAIN,), + "complete-domain coverage", + ) + _require_outcome_definition_role( + roles, + certificate.sound_complete_domain_claim_definition_ref, + (_ROLE_SOUND_COMPLETE_DOMAIN,), + "complete-domain coverage", + ) + claim_definition = definitions[certificate.claim_definition_ref] + complete_domain_definition = definitions[ + certificate.complete_domain_claim_definition_ref + ] + sound_domain_definition = definitions[ + certificate.sound_complete_domain_claim_definition_ref + ] + if ( + _definition_record_reference( + claim_definition, + _CLAIM_PROOF_MATERIAL_FIELD, + ) + != proof_material.proof_material_definition_ref + or _definition_record_reference( + claim_definition, + _CLAIM_CHECKER_CAPABILITY_FIELD, + ) + != checked_proof_outcome.checker_capability_ref + ): + raise SemanticContractError("claim admissibility") + if ( + certificate.proof_material_definition_ref + != proof_material.proof_material_definition_ref + or certificate.proof_material_definition_ref + != _definition_record_reference( + claim_definition, + _CLAIM_PROOF_MATERIAL_FIELD, + ) + ): + raise SemanticContractError("certificate proof material") + if ( + _definition_record_reference( + complete_domain_definition, + _COMPLETE_DOMAIN_CLAIM_FIELD, + ) + != certificate.claim_definition_ref + or _definition_record_reference( + sound_domain_definition, + _COMPLETE_DOMAIN_CLAIM_FIELD, + ) + != certificate.claim_definition_ref + ): + raise SemanticContractError("complete-domain coverage") + if ( + certificate != result.accepted_certificate + or certificate.claim_definition_ref + != proposal.proposal_claim_definition_ref + or certificate.claim_definition_ref + != checked_proof_outcome.checked_claim_definition_ref + or certificate.claim_definition_ref != result.claim_definition_ref + or certificate.claim_definition_ref + not in proof_policy.accepted_claim_definition_refs + or certificate.claim_definition_ref + not in action_space_profile.allowed_claim_definition_refs + or certificate.checker_disposition is not CheckerDisposition.ACCEPTED + or checked_proof_outcome.checker_disposition + is not CheckerDisposition.ACCEPTED + or result.certificate_sha256 != certificate.certificate_sha256 + or result.complete_domain_coverage_artifact_sha256 + != certificate.complete_domain_coverage_artifact_sha256 + ): + raise SemanticContractError("complete-domain coverage") + elif isinstance(result, NoncertifiedWitnessResult): + if certificate is not None: + raise SemanticContractError("witness certificate presence") + if not proof_policy.permit_noncertified_terminal_records: + raise SemanticContractError("noncertified policy") + _require_outcome_definition_role( + roles, + result.claim_definition_ref, + (_ROLE_NONCERTIFIED_WITNESS,), + "claim admissibility", + ) + if ( + result.claim_definition_ref + not in action_space_profile.allowed_claim_definition_refs + ): + raise SemanticContractError("claim admissibility") + if result.evidence_claim_definition_ref not in definitions: + raise SemanticContractError("witness evidence admissibility") + if result.program_sha256 is None: + if ( + program is not None + or grounded_obligations is not None + or proposal.program_sha256 is not None + or proposal.after_scene_state_sha256 is not None + ): + raise SemanticContractError("witness program presence") + else: + if program is None or grounded_obligations is None: + raise SemanticContractError("witness program presence") + self.validate_edit_program( + semantic_definition_bundle, + solve_policy_definition_bundle, + value_schema_definitions, + predicate_definitions, + state_variable_definitions, + derived_fact_rule_definitions, + operator_definitions, + implementation_registry_snapshot, + problem, + semantics_profile, + action_space_profile, + scene_state, + program, + scene_state, + program.after_scene_state, + grounded_obligations, + problem.intervention_authorization, + ) + if ( + result.program_sha256 != program.program_sha256 + or result.after_scene_state_sha256 + != program.after_scene_state_sha256 + or proposal.program_sha256 != program.program_sha256 + or proposal.after_scene_state_sha256 + != program.after_scene_state_sha256 + ): + raise SemanticContractError("witness program") + if result.checker_disposition is CheckerDisposition.ACCEPTED: + raise SemanticContractError("weak claim promotion") + if ( + checked_proof_outcome is not None + and checked_proof_outcome.checker_disposition + is CheckerDisposition.ACCEPTED + ): + raise SemanticContractError("weak claim promotion") + elif isinstance(result, UnknownResult): + if ( + certificate is not None + or program is not None + or grounded_obligations is not None + ): + raise SemanticContractError("unknown certificate presence") + if ( + proposal.program_sha256 is not None + or proposal.after_scene_state_sha256 is not None + ): + raise SemanticContractError("unknown proposal program") + _require_outcome_definition_role( + roles, + result.claim_definition_ref, + (_ROLE_UNKNOWN,), + "claim admissibility", + ) + _require_outcome_definition_role( + roles, + result.reason_claim_definition_ref, + (_ROLE_UNKNOWN,), + "unknown reason admissibility", + ) + if ( + result.claim_definition_ref + not in action_space_profile.allowed_claim_definition_refs + or result.reason_claim_definition_ref + not in action_space_profile.allowed_claim_definition_refs + ): + raise SemanticContractError("unknown claim admissibility") + if result.checker_disposition is CheckerDisposition.ACCEPTED: + raise SemanticContractError("unknown claim promotion") + if ( + checked_proof_outcome is not None + and checked_proof_outcome.checker_disposition + is CheckerDisposition.ACCEPTED + ): + raise SemanticContractError("unknown claim promotion") + else: # pragma: no cover - discriminated domain union is exhaustive. + raise SemanticContractError("result branch") + + # A direct result/certificate root must carry every static dependency; + # this rejects forward, reverse, self, and mixed-branch digest swaps. + if certificate is not None: + certificate_fields = ( + ("semantic_problem_sha256", problem.semantic_problem_sha256), + ("solve_request_sha256", request.solve_request_sha256), + ("scene_state_sha256", scene_state.scene_state_sha256), + ( + "backend_selection_record_sha256", + selection.backend_selection_record_sha256, + ), + ( + "checked_proof_outcome_sha256", + checked_proof_outcome.checked_proof_outcome_sha256, + ), + ( + "verifier_dispatch_record_sha256", + verifier_dispatch_record.verifier_dispatch_record_sha256, + ), + ( + "semantic_definition_bundle_sha256", + semantic_definition_bundle.definition_bundle_sha256, + ), + ( + "solve_policy_definition_bundle_sha256", + solve_policy_definition_bundle.definition_bundle_sha256, + ), + ( + "semantics_profile_sha256", + semantics_profile.semantics_profile_sha256, + ), + ( + "action_space_profile_sha256", + action_space_profile.action_space_profile_sha256, + ), + ( + "intervention_authorization_sha256", + problem.intervention_authorization.intervention_authorization_sha256, + ), + ( + "objective_expression_sha256", + problem.objective_expression.objective_expression_sha256, + ), + ("proof_policy_sha256", proof_policy.proof_policy_sha256), + ("resource_policy_sha256", resource_policy.resource_policy_sha256), + ( + "backend_routing_policy_sha256", + backend_routing_policy.backend_routing_policy_sha256, + ), + ("solver_config_sha256", solver_config.solver_config_sha256), + ( + "implementation_registry_snapshot_sha256", + implementation_registry_snapshot.implementation_registry_snapshot_sha256, + ), + ( + "backend_descriptor_bundle_sha256", + backend_descriptor_bundle.backend_descriptor_bundle_sha256, + ), + ( + "proposal_backend_build_sha256", + proposal.proposal_backend_build_sha256, + ), + ("checker_build_sha256", checked_proof_outcome.checker_build_sha256), + ("proof_material_sha256", proof_material.proof_material_sha256), + ) + if any( + getattr(certificate, name) != expected + for name, expected in certificate_fields + ): + raise SemanticContractError("certificate roots") + return result diff --git a/src/spatialcf/domain/counterfactual.py b/src/spatialcf/domain/counterfactual.py new file mode 100644 index 0000000..c170c90 --- /dev/null +++ b/src/spatialcf/domain/counterfactual.py @@ -0,0 +1,368 @@ +"""Composed semantic counterfactual problems and operational solve requests. + +This additive M1 module composes the frozen current :class:`CanonicalScene` +with typed extension facts. It intentionally owns only local structural and +self-hash validation: definition/profile resolution, leaf-index completeness, +transition replay, authorization subset checks, and backend compatibility are +static-registry concerns for Task 8. +""" + +from __future__ import annotations + +from typing import ClassVar, Literal, Self, TypeVar + +from pydantic import Field, model_validator + +from spatialcf.domain.base import CanonicalId, CanonicalModel, FactSetV2, Sha256Digest +from spatialcf.domain.definitions import ( + DefinitionBundle, + DefinitionRef, + HashBoundCanonicalModel, + SchemaRef, + TypedValue, +) +from spatialcf.domain.operators import ( + OperationInvocation, + StateDeltaManifest, + StateLeafIndex, +) +from spatialcf.domain.predicates import ( + AfterGoal, + BeforePrecondition, + ObservationObligation, + PreservationInvariant, +) +from spatialcf.domain.profiles import ( + BackendDescriptorBundle, + BackendRoutingPolicy, + CounterfactualSolverConfig, + ImplementationRegistrySnapshot, + InterventionAuthorization, + ObjectiveExpression, + ProfileRef, + ProofPolicy, + ResourcePolicy, +) +from spatialcf.domain.scene import CanonicalScene +from spatialcf.domain.serialization import canonical_json_bytes, canonical_sha256 + +__all__ = ( + "CounterfactualProblemIR", + "CounterfactualSolveRequest", + "EditProgram", + "ExtensionFact", + "ExtensionFactBundle", + "SceneStateEnvelope", +) + +_ValueT = TypeVar("_ValueT") +_FactT = TypeVar("_FactT", bound=CanonicalModel) +_BASE_SCENE_HASH_DOMAIN = "spatialcf/counterfactual/base-scene-payload/3.0" +_BASE_SCENE_OBJECTS_FAMILY_REF: DefinitionRef = ( + "definition:spatialcf/counterfactual/base-scene/objects/3.0" +) +_BASE_SCENE_GEOMETRY_INSTANCES_FAMILY_REF: DefinitionRef = ( + "definition:spatialcf/counterfactual/base-scene/geometry-instances/3.0" +) +_BASE_SCENE_COLLISION_BODIES_FAMILY_REF: DefinitionRef = ( + "definition:spatialcf/counterfactual/base-scene/collision-bodies/3.0" +) +_BASE_SCENE_WORKSPACE_BOUNDARIES_FAMILY_REF: DefinitionRef = ( + "definition:spatialcf/counterfactual/base-scene/workspace-boundaries/3.0" +) +_BASE_SCENE_KNOWN_FREE_SPACES_FAMILY_REF: DefinitionRef = ( + "definition:spatialcf/counterfactual/base-scene/known-free-spaces/3.0" +) +_BASE_SCENE_SUPPORT_SURFACES_FAMILY_REF: DefinitionRef = ( + "definition:spatialcf/counterfactual/base-scene/support-surfaces/3.0" +) +_BASE_SCENE_CAMERAS_FAMILY_REF: DefinitionRef = ( + "definition:spatialcf/counterfactual/base-scene/cameras/3.0" +) +_BASE_SCENE_BASELINE_OBSERVATIONS_FAMILY_REF: DefinitionRef = ( + "definition:spatialcf/counterfactual/base-scene/baseline-observations/3.0" +) + + +def _require_sorted_unique_by_bytes( + values: tuple[_ValueT, ...], + label: str, + *, + nonempty: bool = False, +) -> None: + if nonempty and not values: + raise ValueError(f"{label} must not be empty") + encoded = tuple(canonical_json_bytes(value) for value in values) + if encoded != tuple(sorted(encoded)): + raise ValueError(f"{label} must be sorted") + if len(set(encoded)) != len(encoded): + raise ValueError(f"{label} must not contain duplicate entries") + + +def _all_fact_values(facts: FactSetV2[_FactT]) -> tuple[_FactT, ...]: + """Read every stable fact value without trusting a completeness branch.""" + + return tuple( + value + for values in (facts.values, facts.inner_values, facts.outer_values) + if values is not None + for value in values + ) + + +def _derived_base_fact_ownership_keys( + scene: CanonicalScene, +) -> frozenset[tuple[DefinitionRef, CanonicalId, CanonicalId]]: + """Derive non-overridable base ownership from the embedded current scene.""" + + ownership: set[tuple[DefinitionRef, CanonicalId, CanonicalId]] = set() + ownership.update( + (_BASE_SCENE_OBJECTS_FAMILY_REF, fact.object_id, fact.object_id) + for fact in _all_fact_values(scene.objects) + ) + ownership.update( + (_BASE_SCENE_GEOMETRY_INSTANCES_FAMILY_REF, fact.geometry_id, fact.geometry_id) + for fact in _all_fact_values(scene.geometry_instances) + ) + ownership.update( + (_BASE_SCENE_COLLISION_BODIES_FAMILY_REF, fact.body_id, fact.body_id) + for fact in _all_fact_values(scene.collision_bodies) + ) + ownership.update( + (_BASE_SCENE_WORKSPACE_BOUNDARIES_FAMILY_REF, fact.fact_id, fact.fact_id) + for fact in _all_fact_values(scene.workspace_boundaries) + ) + ownership.update( + (_BASE_SCENE_KNOWN_FREE_SPACES_FAMILY_REF, fact.fact_id, fact.fact_id) + for fact in _all_fact_values(scene.known_free_spaces) + ) + ownership.update( + (_BASE_SCENE_SUPPORT_SURFACES_FAMILY_REF, fact.surface_id, fact.surface_id) + for fact in _all_fact_values(scene.support_surfaces) + ) + ownership.update( + (_BASE_SCENE_CAMERAS_FAMILY_REF, fact.camera_id, fact.camera_id) + for fact in _all_fact_values(scene.cameras) + ) + ownership.update( + ( + _BASE_SCENE_BASELINE_OBSERVATIONS_FAMILY_REF, + fact.object_id, + fact.observation_id, + ) + for fact in _all_fact_values(scene.baseline_observations) + ) + return frozenset(ownership) + + +class ExtensionFact(CanonicalModel): + """One typed extension fact owned by exactly one fact-family triple.""" + + fact_family_ref: DefinitionRef + subject_entity_id: CanonicalId + fact_key: CanonicalId + value: TypedValue + + @property + def ownership_key(self) -> tuple[DefinitionRef, CanonicalId, CanonicalId]: + return (self.fact_family_ref, self.subject_entity_id, self.fact_key) + + +class ExtensionFactBundle(HashBoundCanonicalModel): + """A hash-bound, canonical set of typed extension facts.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/extension-fact-bundle/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "extension_fact_bundle_sha256" + + facts: tuple[ExtensionFact, ...] + extension_fact_bundle_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_extension_fact_ownership(self) -> Self: + _require_sorted_unique_by_bytes(self.facts, "extension facts") + ownership = tuple(fact.ownership_key for fact in self.facts) + if len(set(ownership)) != len(ownership): + raise ValueError("extension facts must not duplicate one ownership") + return self + + +class SceneStateEnvelope(HashBoundCanonicalModel): + """The complete current scene plus typed additive facts and state index.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/scene-state/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "scene_state_sha256" + + base_scene_schema_ref: SchemaRef + base_scene_payload: CanonicalScene + base_scene_sha256: Sha256Digest + extension_fact_bundles: tuple[ExtensionFactBundle, ...] + closed_entity_index: tuple[CanonicalId, ...] + canonical_state_leaf_index: StateLeafIndex + scene_state_sha256: Sha256Digest + + @classmethod + def seal(cls, **values) -> Self: + """Bind the frozen base scene using its additive, non-v2 digest domain.""" + + if "base_scene_sha256" in values: + raise ValueError("seal() derives the base scene digest") + if "base_scene_payload" not in values: + return super().seal(**values) + scene = CanonicalScene.model_validate(values["base_scene_payload"], strict=True) + return super().seal( + **( + values + | { + "base_scene_payload": scene, + "base_scene_sha256": canonical_sha256( + scene, + domain=_BASE_SCENE_HASH_DOMAIN, + ), + } + ) + ) + + @model_validator(mode="after") + def _validate_scene_composition(self) -> Self: + expected_base_digest = canonical_sha256( + self.base_scene_payload, + domain=_BASE_SCENE_HASH_DOMAIN, + ) + if self.base_scene_sha256 != expected_base_digest: + raise ValueError("base scene digest does not match the canonical payload") + + base_keys = _derived_base_fact_ownership_keys(self.base_scene_payload) + + _require_sorted_unique_by_bytes( + self.extension_fact_bundles, + "extension fact bundles", + ) + _require_sorted_unique_by_bytes( + self.closed_entity_index, + "closed entity index", + ) + entities = set(self.closed_entity_index) + extension_keys: set[tuple[DefinitionRef, CanonicalId, CanonicalId]] = set() + for bundle in self.extension_fact_bundles: + for fact in bundle.facts: + if fact.subject_entity_id not in entities: + raise ValueError( + "extension facts must belong to the closed entity index" + ) + if fact.ownership_key in base_keys: + raise ValueError( + "extension fact conflicts with base fact ownership" + ) + if fact.ownership_key in extension_keys: + raise ValueError("duplicate extension ownership") + extension_keys.add(fact.ownership_key) + return self + + +class EditProgram(HashBoundCanonicalModel): + """A deterministic ordered program with its complete hash-bound after state.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/edit-program/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "program_sha256" + + program_id: CanonicalId + semantic_problem_sha256: Sha256Digest + action_space_profile_sha256: Sha256Digest + steps: tuple[OperationInvocation, ...] + before_state_sha256: Sha256Digest + after_scene_state: SceneStateEnvelope + after_scene_state_sha256: Sha256Digest + state_delta_manifest: StateDeltaManifest + grounded_obligation_set_sha256: Sha256Digest + program_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_complete_after_state(self) -> Self: + if not self.steps: + raise ValueError( + "edit programs must contain at least one ordered invocation" + ) + if self.after_scene_state_sha256 != self.after_scene_state.scene_state_sha256: + raise ValueError( + "after scene state digest does not match the complete state" + ) + return self + + +class CounterfactualProblemSchemaIdentity(CanonicalModel): + """The one exact schema identity permitted for M1 semantic problem roots.""" + + schema_name: Literal["canonical-counterfactual-problem"] = ( + "canonical-counterfactual-problem" + ) + schema_version: Literal["3.0"] = "3.0" + + +class CounterfactualProblemIR(HashBoundCanonicalModel): + """A pure semantic counterfactual root without backend or native input.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/semantic-problem/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "semantic_problem_sha256" + + schema_identity: CounterfactualProblemSchemaIdentity = Field( + default_factory=CounterfactualProblemSchemaIdentity + ) + problem_id: CanonicalId + scene_state: SceneStateEnvelope + definition_bundle: DefinitionBundle + semantics_profile_ref: ProfileRef + action_space_profile_ref: ProfileRef + intervention_authorization: InterventionAuthorization + before_preconditions: tuple[BeforePrecondition, ...] + after_goal: AfterGoal + preservation_invariants: tuple[PreservationInvariant, ...] + explicit_observation_obligations: tuple[ObservationObligation, ...] + objective_expression: ObjectiveExpression + numeric_semantics_ref: DefinitionRef + semantic_problem_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_semantic_wrapper_sets(self) -> Self: + before_bytes = tuple( + canonical_json_bytes(item) for item in self.before_preconditions + ) + if len(set(before_bytes)) != len(before_bytes): + raise ValueError("duplicate before precondition") + if before_bytes != tuple(sorted(before_bytes)): + raise ValueError("before preconditions must be sorted") + _require_sorted_unique_by_bytes( + self.preservation_invariants, + "preservation invariants", + ) + _require_sorted_unique_by_bytes( + self.explicit_observation_obligations, + "explicit observation obligations", + ) + return self + + +class CounterfactualSolveRequest(HashBoundCanonicalModel): + """An operational root that embeds, but never changes, semantic identity.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/solve-request/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "solve_request_sha256" + + semantic_problem: CounterfactualProblemIR + semantic_problem_sha256: Sha256Digest + solve_policy_definition_bundle: DefinitionBundle + implementation_registry_snapshot: ImplementationRegistrySnapshot + backend_descriptor_bundle: BackendDescriptorBundle + solver_config: CounterfactualSolverConfig + proof_policy: ProofPolicy + resource_policy: ResourcePolicy + backend_routing_policy: BackendRoutingPolicy + solve_request_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_embedded_semantic_root(self) -> Self: + if ( + self.semantic_problem_sha256 + != self.semantic_problem.semantic_problem_sha256 + ): + raise ValueError("semantic problem digest does not match the embedded root") + return self diff --git a/src/spatialcf/domain/definitions.py b/src/spatialcf/domain/definitions.py new file mode 100644 index 0000000..4ed20f2 --- /dev/null +++ b/src/spatialcf/domain/definitions.py @@ -0,0 +1,674 @@ +"""Closed M1 definition and typed-value contracts. + +This module adds the small, immutable bootstrap vocabulary for the general +counterfactual IR. It intentionally performs only local structural checks; +cross-record schema and definition resolution belongs to the static registry. +""" + +from __future__ import annotations + +from copy import copy +from enum import StrEnum +from types import UnionType +from typing import ( + Annotated, + ClassVar, + Literal, + Self, + TypeAlias, + TypeVar, + Union, + get_args, + get_origin, +) + +from pydantic import ( + BeforeValidator, + Field, + GetCoreSchemaHandler, + StrictBool, + StrictInt, + create_model, + model_validator, +) +from pydantic.fields import FieldInfo +from pydantic_core import CoreSchema, core_schema + +from spatialcf.domain.base import ( + CanonicalId, + CanonicalModel, + FiniteFloat, + Quaternion, + Sha256Digest, + Vec2, + Vec3, +) +from spatialcf.domain.serialization import canonical_json_bytes, canonical_sha256 + +BOOTSTRAP_SCHEMA_SHA256 = ( + "6778bead7c5de0999af5768d2dd9747e20e08ab37fe110579c286a9e451e4fa4" +) + + +def _require_definition_ref(value): + if isinstance(value, str) and not value.startswith("definition:"): + raise ValueError("definition references must start with 'definition:'") + return value + + +def _require_schema_ref(value): + if isinstance(value, str) and not value.startswith("schema:"): + raise ValueError("schema references must start with 'schema:'") + return value + + +def _require_capability_ref(value): + if isinstance(value, str) and not value.startswith("capability:"): + raise ValueError("capability references must start with 'capability:'") + return value + + +DefinitionRef = Annotated[CanonicalId, BeforeValidator(_require_definition_ref)] +SchemaRef = Annotated[CanonicalId, BeforeValidator(_require_schema_ref)] +CapabilityRef = Annotated[CanonicalId, BeforeValidator(_require_capability_ref)] +NonNegativeStrictInt = Annotated[StrictInt, Field(ge=0)] + + +class ValueKind(StrEnum): + """The closed M1 bootstrap algebra for canonical typed values.""" + + BOOLEAN = "BOOLEAN" + INTEGER = "INTEGER" + FINITE_REAL = "FINITE_REAL" + CANONICAL_ID = "CANONICAL_ID" + DIGEST = "DIGEST" + ENUM_SYMBOL = "ENUM_SYMBOL" + LENGTH = "LENGTH" + AREA = "AREA" + ANGLE = "ANGLE" + TIME = "TIME" + PIXEL = "PIXEL" + UNIT_INTERVAL = "UNIT_INTERVAL" + ENTITY_REF = "ENTITY_REF" + OBJECT_REF = "OBJECT_REF" + GEOMETRY_REF = "GEOMETRY_REF" + BODY_REF = "BODY_REF" + SURFACE_REF = "SURFACE_REF" + CAMERA_REF = "CAMERA_REF" + FRAME_REF = "FRAME_REF" + REGION_REF = "REGION_REF" + PREDICATE_DEFINITION_REF = "PREDICATE_DEFINITION_REF" + OPERATOR_DEFINITION_REF = "OPERATOR_DEFINITION_REF" + OBJECTIVE_DEFINITION_REF = "OBJECTIVE_DEFINITION_REF" + POINT_2D = "POINT_2D" + POINT_3D = "POINT_3D" + VECTOR_2D = "VECTOR_2D" + VECTOR_3D = "VECTOR_3D" + RIGID_POSE = "RIGID_POSE" + INTERVAL = "INTERVAL" + CLOSED_BOX = "CLOSED_BOX" + FINITE_SET = "FINITE_SET" + FINITE_ORDERED_TUPLE = "FINITE_ORDERED_TUPLE" + RECORD = "RECORD" + + +_DIMENSIONED_KINDS = frozenset( + ( + ValueKind.LENGTH, + ValueKind.AREA, + ValueKind.ANGLE, + ValueKind.TIME, + ValueKind.PIXEL, + ValueKind.UNIT_INTERVAL, + ) +) +_GEOMETRIC_KINDS = frozenset( + ( + ValueKind.POINT_2D, + ValueKind.POINT_3D, + ValueKind.VECTOR_2D, + ValueKind.VECTOR_3D, + ValueKind.RIGID_POSE, + ValueKind.CLOSED_BOX, + ) +) +_SEQUENCE_KINDS = frozenset((ValueKind.FINITE_SET, ValueKind.FINITE_ORDERED_TUPLE)) +_AnnotationT = TypeVar("_AnnotationT") + + +class HashBoundCanonicalModel(CanonicalModel): + """A strict immutable model whose normal wire carries its own digest.""" + + HASH_DOMAIN: ClassVar[str] + SELF_DIGEST_FIELD: ClassVar[str] + + @staticmethod + def _replace_self_annotation( + annotation: _AnnotationT, + model_type: type[Self], + ) -> _AnnotationT: + """Recursively bind typing.Self to the concrete hash-bound model.""" + + if annotation is Self: + return model_type + origin = get_origin(annotation) + if origin is None: + return annotation + arguments = get_args(annotation) + rewritten_arguments = tuple( + HashBoundCanonicalModel._replace_self_annotation(argument, model_type) + for argument in arguments + ) + if rewritten_arguments == arguments: + return annotation + if origin is Annotated: + return Annotated[rewritten_arguments[0], *rewritten_arguments[1:]] + if origin is UnionType or origin is Union: + union = rewritten_arguments[0] + for argument in rewritten_arguments[1:]: + union = union | argument + return union + return origin[rewritten_arguments] + + @staticmethod + def _copy_field_info_with_annotation( + field_info: FieldInfo, + annotation: _AnnotationT, + ) -> FieldInfo: + """Keep public FieldInfo metadata while changing only its annotation.""" + + payload_field_info = copy(field_info) + payload_field_info.annotation = annotation + return payload_field_info + + @classmethod + def __get_pydantic_core_schema__( + cls, + source_type: type[Self], + handler: GetCoreSchemaHandler, + ) -> CoreSchema: + """Apply the digest check after every subclass-local validator.""" + + schema = handler(source_type) + original_ref = schema.get("ref") + if original_ref: + inner_schema = {**schema, "ref": f"{original_ref}:self-digest-inner"} + return core_schema.no_info_after_validator_function( + cls._assert_self_digest_and_return, + inner_schema, + ref=original_ref, + ) + return core_schema.no_info_after_validator_function( + cls._assert_self_digest_and_return, + schema, + ) + + @classmethod + def _assert_self_digest_and_return(cls, model: Self) -> Self: + field_name = cls.SELF_DIGEST_FIELD + if field_name not in cls.model_fields: + raise ValueError("hash-bound model has no declared self digest field") + payload = model.model_dump( + mode="python", + by_alias=True, + exclude={field_name}, + exclude_none=False, + exclude_defaults=False, + exclude_unset=False, + exclude_computed_fields=True, + round_trip=True, + ) + expected = canonical_sha256(payload, domain=cls.HASH_DOMAIN) + if getattr(model, field_name) != expected: + raise ValueError("submitted self digest does not match canonical payload") + return model + + @classmethod + def seal(cls, **values) -> Self: + """Strictly validate fields, compute the only excluded digest, and seal.""" + + field_name = cls.SELF_DIGEST_FIELD + if field_name in values: + raise ValueError("seal() does not accept a caller-supplied self-digest") + if field_name not in cls.model_fields: + raise ValueError("hash-bound model has no declared self digest field") + + payload_model = create_model( + f"_{cls.__name__}SealPayload", + __base__=CanonicalModel, + **{ + name: ( + rewritten_annotation := cls._replace_self_annotation( + field.annotation, + cls, + ), + cls._copy_field_info_with_annotation(field, rewritten_annotation), + ) + for name, field in cls.model_fields.items() + if name != field_name + }, + ) + payload = payload_model.model_validate(values, strict=True).model_dump( + mode="python", + by_alias=True, + exclude_none=False, + exclude_defaults=False, + exclude_unset=False, + exclude_computed_fields=True, + round_trip=True, + ) + digest = canonical_sha256(payload, domain=cls.HASH_DOMAIN) + return cls.model_validate(payload | {field_name: digest}, strict=True) + + +class ValueFieldDefinition(CanonicalModel): + """One canonical record field declaration without registry resolution.""" + + field_name: CanonicalId + value_schema_ref: SchemaRef + required: StrictBool = True + + +class ValueSchemaDefinition(HashBoundCanonicalModel): + """An immutable local description of one closed typed-value shape.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/value-schema-definition/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "value_schema_definition_sha256" + + value_schema_ref: SchemaRef + value_kind: ValueKind + fields: tuple[ValueFieldDefinition, ...] = () + enum_symbols: tuple[CanonicalId, ...] = () + unit_schema_ref: SchemaRef | None = None + dimension_schema_ref: SchemaRef | None = None + frame_schema_ref: SchemaRef | None = None + endpoint_schema_ref: SchemaRef | None = None + lower_closed: StrictBool | None = None + upper_closed: StrictBool | None = None + element_schema_ref: SchemaRef | None = None + min_cardinality: NonNegativeStrictInt | None = None + max_cardinality: NonNegativeStrictInt | None = None + value_schema_definition_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_local_schema_shape(self) -> Self: + if self.value_kind in _DIMENSIONED_KINDS: + if self.unit_schema_ref is None: + raise ValueError("dimensioned value schemas require a unit schema") + elif self.unit_schema_ref is not None: + raise ValueError("only dimensioned value schemas may carry a unit schema") + + if self.value_kind in _GEOMETRIC_KINDS: + if self.dimension_schema_ref is None or self.frame_schema_ref is None: + raise ValueError("geometric value schemas require dimension and frame") + elif self.dimension_schema_ref is not None or self.frame_schema_ref is not None: + raise ValueError( + "only geometric value schemas may carry dimension or frame" + ) + + if self.value_kind is ValueKind.INTERVAL: + if ( + self.endpoint_schema_ref is None + or self.lower_closed is None + or self.upper_closed is None + ): + raise ValueError("interval schemas require endpoint schema and closure") + elif ( + self.endpoint_schema_ref is not None + or self.lower_closed is not None + or self.upper_closed is not None + ): + raise ValueError("only interval schemas may carry endpoint closure") + + if self.value_kind in _SEQUENCE_KINDS: + if self.element_schema_ref is None: + raise ValueError("sequence schemas require an element schema") + if ( + self.max_cardinality is not None + and self.min_cardinality is not None + and self.max_cardinality < self.min_cardinality + ): + raise ValueError("maximum cardinality must not be below minimum") + elif ( + self.element_schema_ref is not None + or self.min_cardinality is not None + or self.max_cardinality is not None + ): + raise ValueError("only sequence schemas may carry cardinality") + + if self.value_kind is ValueKind.ENUM_SYMBOL: + _require_sorted_unique_ids(self.enum_symbols, "enum symbols", nonempty=True) + elif self.enum_symbols: + raise ValueError("only enum schemas may carry enum symbols") + + if self.value_kind is ValueKind.RECORD: + _require_sorted_unique_field_definitions(self.fields) + elif self.fields: + raise ValueError("only record schemas may carry field definitions") + return self + + +class BooleanValue(CanonicalModel): + kind: Literal[ValueKind.BOOLEAN] = ValueKind.BOOLEAN + value: StrictBool + + +class IntegerValue(CanonicalModel): + kind: Literal[ValueKind.INTEGER] = ValueKind.INTEGER + value: StrictInt + + +class FiniteRealValue(CanonicalModel): + kind: Literal[ValueKind.FINITE_REAL] = ValueKind.FINITE_REAL + value: FiniteFloat + + +class CanonicalIdValue(CanonicalModel): + kind: Literal[ValueKind.CANONICAL_ID] = ValueKind.CANONICAL_ID + value: CanonicalId + + +class DigestValue(CanonicalModel): + kind: Literal[ValueKind.DIGEST] = ValueKind.DIGEST + value: Sha256Digest + + +class EnumSymbolValue(CanonicalModel): + kind: Literal[ValueKind.ENUM_SYMBOL] = ValueKind.ENUM_SYMBOL + symbol: CanonicalId + + +ScalarPayload: TypeAlias = Annotated[ + BooleanValue + | IntegerValue + | FiniteRealValue + | CanonicalIdValue + | DigestValue + | EnumSymbolValue, + Field(discriminator="kind"), +] + + +class DimensionedQuantityValue(CanonicalModel): + kind: Literal[ + ValueKind.LENGTH, + ValueKind.AREA, + ValueKind.ANGLE, + ValueKind.TIME, + ValueKind.PIXEL, + ] + value: FiniteFloat + unit_schema_ref: SchemaRef + + +class UnitIntervalValue(CanonicalModel): + kind: Literal[ValueKind.UNIT_INTERVAL] = ValueKind.UNIT_INTERVAL + value: FiniteFloat + unit_schema_ref: SchemaRef + + @model_validator(mode="after") + def _validate_unit_interval(self) -> Self: + if not 0.0 <= self.value <= 1.0: + raise ValueError("unit interval values must lie within [0, 1]") + return self + + +class ReferenceValue(CanonicalModel): + kind: Literal[ + ValueKind.ENTITY_REF, + ValueKind.OBJECT_REF, + ValueKind.GEOMETRY_REF, + ValueKind.BODY_REF, + ValueKind.SURFACE_REF, + ValueKind.CAMERA_REF, + ValueKind.FRAME_REF, + ValueKind.REGION_REF, + ValueKind.PREDICATE_DEFINITION_REF, + ValueKind.OPERATOR_DEFINITION_REF, + ValueKind.OBJECTIVE_DEFINITION_REF, + ] + reference: CanonicalId + + +class Point2DValue(CanonicalModel): + kind: Literal[ValueKind.POINT_2D] = ValueKind.POINT_2D + coordinates: Vec2 + dimension_schema_ref: SchemaRef + frame_schema_ref: SchemaRef + + +class Point3DValue(CanonicalModel): + kind: Literal[ValueKind.POINT_3D] = ValueKind.POINT_3D + coordinates: Vec3 + dimension_schema_ref: SchemaRef + frame_schema_ref: SchemaRef + + +PointPayload: TypeAlias = Annotated[ + Point2DValue | Point3DValue, + Field(discriminator="kind"), +] + + +class Vector2DValue(CanonicalModel): + kind: Literal[ValueKind.VECTOR_2D] = ValueKind.VECTOR_2D + coordinates: Vec2 + dimension_schema_ref: SchemaRef + frame_schema_ref: SchemaRef + + +class Vector3DValue(CanonicalModel): + kind: Literal[ValueKind.VECTOR_3D] = ValueKind.VECTOR_3D + coordinates: Vec3 + dimension_schema_ref: SchemaRef + frame_schema_ref: SchemaRef + + +class RigidPoseValue(CanonicalModel): + kind: Literal[ValueKind.RIGID_POSE] = ValueKind.RIGID_POSE + translation: Vec3 + rotation: Quaternion + dimension_schema_ref: SchemaRef + frame_schema_ref: SchemaRef + + +class IntervalValue(CanonicalModel): + kind: Literal[ValueKind.INTERVAL] = ValueKind.INTERVAL + endpoint_schema_ref: SchemaRef + lower: ScalarPayload + upper: ScalarPayload + lower_closed: StrictBool + upper_closed: StrictBool + + @model_validator(mode="after") + def _validate_interval_structure(self) -> Self: + if self.lower.kind is not self.upper.kind: + raise ValueError("interval endpoints must share one scalar kind") + if isinstance(self.lower, (IntegerValue, FiniteRealValue)): + if self.lower.value > self.upper.value: + raise ValueError( + "interval lower endpoint must not exceed upper endpoint" + ) + if ( + self.lower.value == self.upper.value + and not self.lower_closed + and not self.upper_closed + ): + raise ValueError("a degenerate interval must include its endpoint") + return self + + +class ClosedBoxValue(CanonicalModel): + kind: Literal[ValueKind.CLOSED_BOX] = ValueKind.CLOSED_BOX + minimum: PointPayload + maximum: PointPayload + dimension_schema_ref: SchemaRef + frame_schema_ref: SchemaRef + + @model_validator(mode="after") + def _validate_closed_box(self) -> Self: + if self.minimum.kind is not self.maximum.kind: + raise ValueError("closed box endpoints must share one point dimension") + minimum = _coordinate_tuple(self.minimum) + maximum = _coordinate_tuple(self.maximum) + if any(lower > upper for lower, upper in zip(minimum, maximum, strict=True)): + raise ValueError("closed box minimum must not exceed maximum") + return self + + +class NamedTypedValue(CanonicalModel): + name: CanonicalId + value: TypedValue + + +class FiniteSetValue(CanonicalModel): + kind: Literal[ValueKind.FINITE_SET] = ValueKind.FINITE_SET + element_schema_ref: SchemaRef + elements: tuple[TypedValue, ...] + + @model_validator(mode="after") + def _canonicalize_elements(self) -> Self: + encoded = tuple(canonical_json_bytes(element) for element in self.elements) + if len(set(encoded)) != len(encoded): + raise ValueError("finite sets must not contain duplicate members") + ordered = tuple( + element + for _, element in sorted( + zip(encoded, self.elements, strict=True), key=lambda pair: pair[0] + ) + ) + object.__setattr__(self, "elements", ordered) + return self + + +class FiniteOrderedTupleValue(CanonicalModel): + kind: Literal[ValueKind.FINITE_ORDERED_TUPLE] = ValueKind.FINITE_ORDERED_TUPLE + element_schema_ref: SchemaRef + items: tuple[TypedValue, ...] + + +class RecordValue(CanonicalModel): + kind: Literal[ValueKind.RECORD] = ValueKind.RECORD + fields: tuple[NamedTypedValue, ...] + + @model_validator(mode="after") + def _validate_record_fields(self) -> Self: + _require_sorted_unique_named_values(self.fields) + return self + + +ValuePayload: TypeAlias = Annotated[ + ScalarPayload + | DimensionedQuantityValue + | UnitIntervalValue + | ReferenceValue + | PointPayload + | Vector2DValue + | Vector3DValue + | RigidPoseValue + | IntervalValue + | ClosedBoxValue + | FiniteSetValue + | FiniteOrderedTupleValue + | RecordValue, + Field(discriminator="kind"), +] + + +class TypedValue(CanonicalModel): + """A schema reference plus one node from the closed payload union.""" + + value_schema_ref: SchemaRef + payload: ValuePayload + + +NamedTypedValue.model_rebuild() +FiniteSetValue.model_rebuild() +FiniteOrderedTupleValue.model_rebuild() +RecordValue.model_rebuild() +TypedValue.model_rebuild() + + +class CanonicalDefinitionEnvelope(HashBoundCanonicalModel): + """One immutable definition record with its exact typed payload.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/definition-envelope/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "definition_sha256" + + definition_ref: DefinitionRef + definition_kind_ref: DefinitionRef + payload_schema_ref: SchemaRef + payload: TypedValue + definition_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_payload_schema_binding(self) -> Self: + if self.payload.value_schema_ref != self.payload_schema_ref: + raise ValueError( + "definition payload must carry the declared payload schema" + ) + return self + + +class DefinitionBundle(HashBoundCanonicalModel): + """The semantic definition closure with only local identity checks.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/definition-bundle/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "definition_bundle_sha256" + + bootstrap_schema_sha256: Sha256Digest = BOOTSTRAP_SCHEMA_SHA256 + definitions: tuple[CanonicalDefinitionEnvelope, ...] + definition_bundle_sha256: Sha256Digest + + @model_validator(mode="before") + @classmethod + def _reject_bootstrap_replacement(cls, values): + if ( + isinstance(values, dict) + and "bootstrap_schema_sha256" in values + and values["bootstrap_schema_sha256"] != BOOTSTRAP_SCHEMA_SHA256 + ): + raise ValueError("bootstrap schema replacement is not permitted") + return values + + @model_validator(mode="after") + def _validate_definition_order(self) -> Self: + refs = tuple(definition.definition_ref for definition in self.definitions) + if refs != tuple(sorted(refs, key=canonical_json_bytes)): + raise ValueError("definition bundle definitions must be sorted") + if len(set(refs)) != len(refs): + raise ValueError("duplicate definition reference in definition bundle") + return self + + +def _coordinate_tuple(value): + if isinstance(value, Point2DValue): + return (value.coordinates.x, value.coordinates.y) + return (value.coordinates.x, value.coordinates.y, value.coordinates.z) + + +def _require_sorted_unique_ids(values, label: str, *, nonempty: bool = False) -> None: + if nonempty and not values: + raise ValueError(f"{label} must not be empty") + if values != tuple(sorted(values, key=canonical_json_bytes)): + raise ValueError(f"{label} must be sorted") + if len(set(values)) != len(values): + raise ValueError(f"{label} must not contain duplicate entries") + + +def _require_sorted_unique_field_definitions( + fields: tuple[ValueFieldDefinition, ...], +) -> None: + names = tuple(field.field_name for field in fields) + if names != tuple(sorted(names, key=canonical_json_bytes)): + raise ValueError("record field definitions must be sorted") + if len(set(names)) != len(names): + raise ValueError("record field definitions must not contain duplicate fields") + + +def _require_sorted_unique_named_values(fields: tuple[NamedTypedValue, ...]) -> None: + names = tuple(field.name for field in fields) + if names != tuple(sorted(names, key=canonical_json_bytes)): + raise ValueError("record fields must be sorted") + if len(set(names)) != len(names): + raise ValueError("record fields must not contain duplicate names") diff --git a/src/spatialcf/domain/operators.py b/src/spatialcf/domain/operators.py new file mode 100644 index 0000000..86be83a --- /dev/null +++ b/src/spatialcf/domain/operators.py @@ -0,0 +1,343 @@ +"""Closed state-authority and transition-operator contracts for M1. + +This module owns only immutable, hash-bound structural contracts. It does not +apply a state transition, recompute derived facts, resolve references, or load +an implementation; those cross-record concerns belong to the later registry. +""" + +from __future__ import annotations + +from enum import StrEnum +from typing import Annotated, ClassVar, Self + +from pydantic import BeforeValidator, model_validator + +from spatialcf.domain.base import CanonicalId, CanonicalModel, Sha256Digest +from spatialcf.domain.definitions import ( + CapabilityRef, + DefinitionRef, + HashBoundCanonicalModel, + SchemaRef, + TypedValue, + canonical_json_bytes, +) +from spatialcf.domain.predicates import BeforePrecondition, GroundedObligation + +__all__ = ( + "DerivedFactRuleDefinition", + "OperationArgument", + "OperationInvocation", + "OperatorDefinition", + "StateAddressPattern", + "StateDeltaManifest", + "StateLeafIndex", + "StateVariableDefinition", + "StateVariableRef", + "TypedVariableBound", + "WriteAuthority", +) + + +def _require_field_path_ref(value): + if isinstance(value, str): + prefix = "field-path:" + suffix = value.removeprefix(prefix) + if not value.startswith(prefix) or not suffix: + raise ValueError("state field paths must use a field-path reference") + if any(token in suffix for token in (".", "/", "~", "*")): + raise ValueError("state field paths must be schema-owned references") + return value + + +def _require_parameter_ref(value): + if isinstance(value, str) and not value.startswith("parameter:"): + raise ValueError("state address parameters must start with 'parameter:'") + return value + + +FieldPathRef = Annotated[CanonicalId, BeforeValidator(_require_field_path_ref)] +ParameterRef = Annotated[CanonicalId, BeforeValidator(_require_parameter_ref)] + + +class WriteAuthority(StrEnum): + """The permanent, non-extensible M1 write-authority partition.""" + + PRIMARY_WRITABLE = "PRIMARY_WRITABLE" + DERIVED_ONLY = "DERIVED_ONLY" + + +class StateVariableDefinition(HashBoundCanonicalModel): + """One definition-level state-variable shape and its write authority.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/state-variable-definition/3.0" + ) + SELF_DIGEST_FIELD: ClassVar[str] = "state_variable_definition_sha256" + + state_variable_ref: DefinitionRef + state_variable_schema_ref: SchemaRef + value_schema_ref: SchemaRef + frame_ref: DefinitionRef + unit_ref: DefinitionRef + topology_ref: DefinitionRef + write_authority: WriteAuthority + derived_fact_rule_ref: DefinitionRef | None = None + state_variable_definition_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_write_authority(self) -> Self: + if self.write_authority is WriteAuthority.PRIMARY_WRITABLE: + if self.derived_fact_rule_ref is not None: + raise ValueError( + "primary writable state variables must not carry a derived rule" + ) + elif self.derived_fact_rule_ref is None: + raise ValueError("derived only state variables require exactly one rule") + return self + + +class StateVariableRef(CanonicalModel): + """One schema-owned addressable leaf, never a free-form selector string.""" + + state_variable_schema_ref: SchemaRef + state_schema_ref: SchemaRef + fact_family_ref: DefinitionRef + entity_or_fact_key: CanonicalId + field_path_ref: FieldPathRef + + +class StateAddressParameterBinding(CanonicalModel): + """A typed input used to instantiate one state-variable definition pattern.""" + + parameter_ref: ParameterRef + parameter_schema_ref: SchemaRef + + +class StateAddressPattern(CanonicalModel): + """A closed state-variable definition plus its typed instantiation inputs.""" + + state_variable_definition_ref: DefinitionRef + parameter_bindings: tuple[StateAddressParameterBinding, ...] = () + + @model_validator(mode="after") + def _validate_parameter_bindings(self) -> Self: + bindings = self.parameter_bindings + names = tuple(binding.parameter_ref for binding in bindings) + if names != tuple(sorted(names, key=canonical_json_bytes)): + raise ValueError("state address parameter bindings must be sorted") + if len(set(names)) != len(names): + raise ValueError("state address parameter bindings must not duplicate") + return self + + +class StateLeafIndex(HashBoundCanonicalModel): + """The complete locally canonical index of all addressable scene leaves.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/state-leaf-index/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "state_leaf_index_sha256" + + leaves: tuple[StateVariableRef, ...] + state_leaf_index_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_leaves(self) -> Self: + _require_sorted_unique_state_refs(self.leaves, "state leaf index leaves") + return self + + +class DerivedFactRuleDefinition(HashBoundCanonicalModel): + """A pure, fixed-footprint derived-fact recomputation contract.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/derived-fact-rule-definition/3.0" + ) + SELF_DIGEST_FIELD: ClassVar[str] = "derived_fact_rule_definition_sha256" + + derived_fact_rule_ref: DefinitionRef + fixed_read_set: tuple[StateVariableRef, ...] + fixed_output_set: tuple[StateVariableRef, ...] + evaluator_capability_ref: CapabilityRef + verifier_capability_ref: CapabilityRef + derived_fact_rule_definition_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_fixed_footprints(self) -> Self: + _require_sorted_unique_state_refs( + self.fixed_read_set, + "derived fact rule fixed read set", + ) + _require_sorted_unique_state_refs( + self.fixed_output_set, + "derived fact rule fixed output set", + nonempty=True, + ) + if self.evaluator_capability_ref == self.verifier_capability_ref: + raise ValueError("derived fact rule capability pair must be distinct") + return self + + +class TypedVariableBound(CanonicalModel): + """A typed bound with explicit value, frame, unit, and topology semantics.""" + + state_variable_ref: StateVariableRef + value_schema_ref: SchemaRef + typed_domain: TypedValue + frame_ref: DefinitionRef + unit_ref: DefinitionRef + topology_ref: DefinitionRef + + @model_validator(mode="after") + def _validate_typed_domain(self) -> Self: + if self.typed_domain.value_schema_ref != self.value_schema_ref: + raise ValueError("typed domain must carry the bound value schema") + return self + + +class OperatorDefinition(HashBoundCanonicalModel): + """The complete local transition meaning of one non-native operator.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/operator-definition/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "definition_sha256" + + operator_ref: DefinitionRef + parameter_schema_refs: tuple[SchemaRef, ...] + read_footprint: tuple[StateAddressPattern, ...] + primary_write_footprint: tuple[StateAddressPattern, ...] + derived_write_rule_refs: tuple[DefinitionRef, ...] + required_preconditions: tuple[BeforePrecondition, ...] + transition_semantics_ref: DefinitionRef + generated_obligations: tuple[GroundedObligation, ...] + composability_policy_ref: DefinitionRef + endpoint_or_path_semantics_ref: DefinitionRef + compiler_capability_ref: CapabilityRef + verifier_capability_ref: CapabilityRef + definition_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_definition_closure(self) -> Self: + _require_sorted_unique_by_bytes( + self.read_footprint, + "operator read footprint", + ) + _require_sorted_unique_by_bytes( + self.primary_write_footprint, + "operator primary write footprint", + ) + _require_sorted_unique_by_bytes( + self.derived_write_rule_refs, + "operator derived write rules", + ) + _require_sorted_unique_by_bytes( + self.required_preconditions, + "operator required preconditions", + ) + _require_sorted_unique_by_bytes( + self.generated_obligations, + "operator generated obligations", + ) + if self.compiler_capability_ref == self.verifier_capability_ref: + raise ValueError("operator capability pair must be distinct") + return self + + +class OperationArgument(CanonicalModel): + """One named typed value in an invocation's closed argument tuple.""" + + argument_name: CanonicalId + value: TypedValue + + +class OperationInvocation(CanonicalModel): + """One exact operator reference and its canonical named typed arguments.""" + + operator_ref: DefinitionRef + arguments: tuple[OperationArgument, ...] + + @model_validator(mode="after") + def _validate_arguments(self) -> Self: + names = tuple(argument.argument_name for argument in self.arguments) + if names != tuple(sorted(names, key=canonical_json_bytes)): + raise ValueError("operation arguments must be sorted") + if len(set(names)) != len(names): + raise ValueError("operation arguments must not duplicate") + return self + + +class StateDeltaManifest(HashBoundCanonicalModel): + """The local three-way before/after leaf-partition declaration.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/state-delta-manifest/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "state_delta_manifest_sha256" + + authorized_primary_writes: tuple[StateVariableRef, ...] + recomputed_derived_writes: tuple[StateVariableRef, ...] + unchanged_leaves_digest: Sha256Digest + complete_before_leaf_index_sha256: Sha256Digest + complete_after_leaf_index_sha256: Sha256Digest + state_delta_manifest_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_local_partition(self) -> Self: + _require_sorted_unique_state_refs( + self.authorized_primary_writes, + "authorized primary writes", + ) + _require_sorted_unique_state_refs( + self.recomputed_derived_writes, + "recomputed derived writes", + ) + primary_keys = { + _state_leaf_key(reference) for reference in self.authorized_primary_writes + } + derived_keys = { + _state_leaf_key(reference) for reference in self.recomputed_derived_writes + } + if primary_keys & derived_keys: + raise ValueError("primary and derived writes must not overlap") + return self + + +def _state_leaf_key(reference: StateVariableRef) -> bytes: + """Return the address identity that cannot be claimed by two schemas.""" + + return canonical_json_bytes( + ( + reference.state_schema_ref, + reference.fact_family_ref, + reference.entity_or_fact_key, + reference.field_path_ref, + ) + ) + + +def _require_sorted_unique_state_refs( + references: tuple[StateVariableRef, ...], + label: str, + *, + nonempty: bool = False, +) -> None: + if nonempty and not references: + raise ValueError(f"{label} must not be empty") + encoded = tuple(canonical_json_bytes(reference) for reference in references) + if encoded != tuple(sorted(encoded)): + raise ValueError(f"{label} must be sorted") + if len(set(encoded)) != len(encoded): + raise ValueError(f"{label} must not contain duplicate entries") + address_keys = tuple(_state_leaf_key(reference) for reference in references) + if len(set(address_keys)) != len(address_keys): + raise ValueError(f"{label} must not have two schemas claiming one leaf") + + +def _require_sorted_unique_by_bytes( + values, + label: str, + *, + nonempty: bool = False, +) -> None: + if nonempty and not values: + raise ValueError(f"{label} must not be empty") + encoded = tuple(canonical_json_bytes(value) for value in values) + if encoded != tuple(sorted(encoded)): + raise ValueError(f"{label} must be sorted") + if len(set(encoded)) != len(encoded): + raise ValueError(f"{label} must not contain duplicate entries") diff --git a/src/spatialcf/domain/outcomes.py b/src/spatialcf/domain/outcomes.py new file mode 100644 index 0000000..f54bde0 --- /dev/null +++ b/src/spatialcf/domain/outcomes.py @@ -0,0 +1,614 @@ +"""Typed counterfactual outcomes, certificates, and the one-way M1 hash DAG. + +The contracts here deliberately stop at local structural validation. They bind +every later record to the two roots and reject malformed local dependency +shapes, but they do not resolve definitions, select an implementation, execute +a backend, or certify a proposal. Those cross-record checks remain Task 8 +registry work. +""" + +from __future__ import annotations + +from enum import StrEnum +from typing import Annotated, ClassVar, Literal, Self, TypeAlias, TypeVar + +from pydantic import Field, StrictBool, model_validator + +from spatialcf.domain.base import CanonicalModel, NonNegativeFiniteFloat, Sha256Digest +from spatialcf.domain.definitions import ( + CapabilityRef, + DefinitionRef, + HashBoundCanonicalModel, + SchemaRef, + TypedValue, +) +from spatialcf.domain.profiles import BackendRef, OwnerRef +from spatialcf.domain.serialization import canonical_json_bytes + +__all__ = ( + "BackendProposal", + "BackendSelectionRecord", + "CapabilityMatch", + "CapabilityMismatch", + "CertifiedSolutionCertificate", + "CertifiedSolutionResult", + "CheckedProofOutcome", + "CheckerDisposition", + "CounterfactualCertificate", + "CounterfactualSolveResult", + "NoncertifiedWitnessResult", + "ProofMaterialEnvelope", + "ProvenUnsatCertificate", + "ProvenUnsatResult", + "ResourceUsage", + "TypedCompilationOutcome", + "UnknownResult", + "VerifierDispatchRecord", +) + +_ValueT = TypeVar("_ValueT") + + +def _require_sorted_unique_by_bytes( + values: tuple[_ValueT, ...], + label: str, + *, + nonempty: bool = False, +) -> None: + if nonempty and not values: + raise ValueError(f"{label} must not be empty") + encoded = tuple(canonical_json_bytes(value) for value in values) + if encoded != tuple(sorted(encoded)): + raise ValueError(f"{label} must be sorted") + if len(set(encoded)) != len(encoded): + raise ValueError(f"{label} must not contain duplicate entries") + + +class _ArtifactReference(CanonicalModel): + """One typed, content-addressed artifact without an independent identity.""" + + artifact_schema_ref: SchemaRef + artifact_sha256: Sha256Digest + + +class _ResourceUsageEntry(CanonicalModel): + """One deterministic resource counter closed by its definition reference.""" + + resource_definition_ref: DefinitionRef + used: NonNegativeFiniteFloat + + +class ResourceUsage(CanonicalModel): + """A closed embedded resource row; parent records bind it into their digest.""" + + accounting_claim_definition_ref: DefinitionRef + entries: tuple[_ResourceUsageEntry, ...] + exhausted: StrictBool + + @model_validator(mode="after") + def _validate_entries(self) -> Self: + _require_sorted_unique_by_bytes( + self.entries, + "resource usage entries", + nonempty=True, + ) + refs = tuple(entry.resource_definition_ref for entry in self.entries) + if len(set(refs)) != len(refs): + raise ValueError("resource usage must not duplicate one resource") + return self + + +class CapabilityMatch(CanonicalModel): + """A locally closed successful capability inspection row.""" + + kind: Literal["MATCH"] = "MATCH" + backend_ref: BackendRef + backend_descriptor_sha256: Sha256Digest + matched_capability_refs: tuple[CapabilityRef, ...] + match_claim_definition_ref: DefinitionRef + + @model_validator(mode="after") + def _validate_capabilities(self) -> Self: + _require_sorted_unique_by_bytes( + self.matched_capability_refs, + "matched capabilities", + nonempty=True, + ) + return self + + +class CapabilityMismatch(CanonicalModel): + """A locally closed typed non-support row rather than an exception.""" + + kind: Literal["MISMATCH"] = "MISMATCH" + backend_ref: BackendRef + backend_descriptor_sha256: Sha256Digest + missing_capability_refs: tuple[CapabilityRef, ...] + reason_claim_definition_ref: DefinitionRef + + @model_validator(mode="after") + def _validate_capabilities(self) -> Self: + _require_sorted_unique_by_bytes( + self.missing_capability_refs, + "missing capabilities", + nonempty=True, + ) + return self + + +_CapabilityRow: TypeAlias = Annotated[ + CapabilityMatch | CapabilityMismatch, + Field(discriminator="kind"), +] + + +class BackendSelectionRecord(HashBoundCanonicalModel): + """The ordered frozen backend routing record before any proposal is trusted.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/backend-selection-record/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "backend_selection_record_sha256" + + semantic_problem_sha256: Sha256Digest + solve_request_sha256: Sha256Digest + implementation_registry_snapshot_sha256: Sha256Digest + backend_descriptor_bundle_sha256: Sha256Digest + backend_routing_policy_sha256: Sha256Digest + ordered_candidate_backend_refs: tuple[BackendRef, ...] + capability_rows: tuple[_CapabilityRow, ...] + selection_disposition: Literal["SELECTED", "NO_SELECTION"] + selection_disposition_claim_ref: DefinitionRef + selected_backend_ref: BackendRef | None = None + selected_backend_descriptor_sha256: Sha256Digest | None = None + resource_allocation: ResourceUsage | None = None + deterministic_selection_reason_ref: DefinitionRef + backend_selection_record_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_local_selection(self) -> Self: + candidates = self.ordered_candidate_backend_refs + if not candidates: + raise ValueError("selection candidates must not be empty") + if len(set(candidates)) != len(candidates): + raise ValueError("selection candidates must not contain duplicate backends") + row_backends = tuple(row.backend_ref for row in self.capability_rows) + if row_backends != candidates: + raise ValueError("selection candidates must have one local row each") + + selected_values = ( + self.selected_backend_ref, + self.selected_backend_descriptor_sha256, + self.resource_allocation, + ) + if self.selection_disposition == "SELECTED": + if any(value is None for value in selected_values): + raise ValueError( + "selected disposition requires selected backend fields" + ) + assert self.selected_backend_ref is not None + assert self.selected_backend_descriptor_sha256 is not None + matching_rows = tuple( + row + for row in self.capability_rows + if row.backend_ref == self.selected_backend_ref + ) + if len(matching_rows) != 1 or not isinstance( + matching_rows[0], CapabilityMatch + ): + raise ValueError("selected backend must have one capability match") + if ( + matching_rows[0].backend_descriptor_sha256 + != self.selected_backend_descriptor_sha256 + ): + raise ValueError("selected backend descriptor does not match local row") + elif any(value is not None for value in selected_values): + raise ValueError("no-selection disposition forbids selected backend fields") + return self + + +class TypedCompilationOutcome(HashBoundCanonicalModel): + """An explicitly untrusted compilation-stage terminal record.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/typed-compilation-outcome/3.0" + ) + SELF_DIGEST_FIELD: ClassVar[str] = "typed_compilation_outcome_sha256" + + semantic_problem_sha256: Sha256Digest + solve_request_sha256: Sha256Digest + backend_selection_record_sha256: Sha256Digest + selected_backend_ref: BackendRef + selected_backend_descriptor_sha256: Sha256Digest + compilation_reason_claim_definition_ref: DefinitionRef + partial_artifact_refs: tuple[_ArtifactReference, ...] + resource_usage: ResourceUsage + typed_compilation_outcome_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_partial_artifacts(self) -> Self: + _require_sorted_unique_by_bytes( + self.partial_artifact_refs, + "compilation partial artifacts", + ) + return self + + +class ProofMaterialEnvelope(HashBoundCanonicalModel): + """A typed proof-material payload that remains untrusted until checked.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/proof-material-envelope/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "proof_material_sha256" + + semantic_problem_sha256: Sha256Digest + solve_request_sha256: Sha256Digest + backend_selection_record_sha256: Sha256Digest + proposal_backend_ref: BackendRef + proof_material_definition_ref: DefinitionRef + payload_schema_ref: SchemaRef + typed_payload: tuple[TypedValue, ...] + artifact_refs: tuple[_ArtifactReference, ...] + proof_material_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_payload_closure(self) -> Self: + _require_sorted_unique_by_bytes( + self.artifact_refs, + "proof material artifacts", + ) + return self + + +class BackendProposal(HashBoundCanonicalModel): + """An untrusted backend proposal that cannot name a certified result.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/backend-proposal/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "backend_proposal_sha256" + + semantic_problem_sha256: Sha256Digest + solve_request_sha256: Sha256Digest + backend_selection_record_sha256: Sha256Digest + proposal_backend_ref: BackendRef + proposal_backend_owner_ref: OwnerRef + proposal_backend_capability_ref: CapabilityRef + proposal_backend_build_sha256: Sha256Digest + proposal_claim_definition_ref: DefinitionRef + proof_material: ProofMaterialEnvelope + proof_material_sha256: Sha256Digest + program_sha256: Sha256Digest | None = None + after_scene_state_sha256: Sha256Digest | None = None + witness_artifact_refs: tuple[_ArtifactReference, ...] = () + model_artifact_refs: tuple[_ArtifactReference, ...] = () + partial_artifact_refs: tuple[_ArtifactReference, ...] = () + objective_lower_bound: NonNegativeFiniteFloat + objective_upper_bound: NonNegativeFiniteFloat + resource_usage: ResourceUsage + backend_proposal_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_untrusted_proposal(self) -> Self: + if self.proof_material_sha256 != self.proof_material.proof_material_sha256: + raise ValueError("proposal proof material digest does not match envelope") + if (self.program_sha256 is None) != (self.after_scene_state_sha256 is None): + raise ValueError( + "proposal program and after-state hashes must appear together" + ) + if self.objective_lower_bound > self.objective_upper_bound: + raise ValueError( + "proposal objective lower bound must not exceed upper bound" + ) + for label, artifacts in ( + ("proposal witness artifacts", self.witness_artifact_refs), + ("proposal model artifacts", self.model_artifact_refs), + ("proposal partial artifacts", self.partial_artifact_refs), + ): + _require_sorted_unique_by_bytes(artifacts, label) + return self + + +class CheckerDisposition(StrEnum): + """The complete structural disposition vocabulary for one trusted checker.""" + + ACCEPTED = "ACCEPTED" + REJECTED = "REJECTED" + LIMITED = "LIMITED" + + +class CheckedProofOutcome(HashBoundCanonicalModel): + """The checked claim before verifier dispatch or certificate assembly.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/checked-proof-outcome/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "checked_proof_outcome_sha256" + + semantic_problem_sha256: Sha256Digest + solve_request_sha256: Sha256Digest + backend_selection_record_sha256: Sha256Digest + proof_material_sha256: Sha256Digest + checker_capability_ref: CapabilityRef + checker_build_sha256: Sha256Digest + checker_disposition: CheckerDisposition + checked_claim_definition_ref: DefinitionRef + checked_fact_refs: tuple[_ArtifactReference, ...] + checked_proof_outcome_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_checked_facts(self) -> Self: + _require_sorted_unique_by_bytes( + self.checked_fact_refs, + "checked proof facts", + nonempty=True, + ) + return self + + +class VerifierDispatchRecord(HashBoundCanonicalModel): + """A dispatch record that keeps proposal and trusted checker identities apart.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/verifier-dispatch-record/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "verifier_dispatch_record_sha256" + + semantic_problem_sha256: Sha256Digest + solve_request_sha256: Sha256Digest + semantic_definition_bundle_sha256: Sha256Digest + solve_policy_definition_bundle_sha256: Sha256Digest + proof_policy_sha256: Sha256Digest + backend_selection_record_sha256: Sha256Digest + proposal_backend_owner_ref: OwnerRef + proposal_backend_capability_ref: CapabilityRef + proposal_backend_build_sha256: Sha256Digest + proof_material_definition_ref: DefinitionRef + checker_owner_ref: OwnerRef + checker_capability_ref: CapabilityRef + checker_build_sha256: Sha256Digest + checked_proof_outcome_sha256: Sha256Digest + verifier_dispatch_record_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_independent_checker(self) -> Self: + if self.proposal_backend_owner_ref == self.checker_owner_ref: + raise ValueError("proposal backend and checker owners must be distinct") + if self.proposal_backend_capability_ref == self.checker_capability_ref: + raise ValueError( + "proposal backend and checker capabilities must be distinct" + ) + return self + + +class _CertificateBase(HashBoundCanonicalModel): + """Shared exact certificate fields; subclasses supply the discriminated branch.""" + + SELF_DIGEST_FIELD: ClassVar[str] = "certificate_sha256" + + certificate_kind: str + semantic_problem_sha256: Sha256Digest + solve_request_sha256: Sha256Digest + scene_state_sha256: Sha256Digest + backend_selection_record_sha256: Sha256Digest + checked_proof_outcome_sha256: Sha256Digest + verifier_dispatch_record_sha256: Sha256Digest + semantic_definition_bundle_sha256: Sha256Digest + solve_policy_definition_bundle_sha256: Sha256Digest + semantics_profile_sha256: Sha256Digest + action_space_profile_sha256: Sha256Digest + intervention_authorization_sha256: Sha256Digest + objective_expression_sha256: Sha256Digest + proof_policy_sha256: Sha256Digest + resource_policy_sha256: Sha256Digest + backend_routing_policy_sha256: Sha256Digest + solver_config_sha256: Sha256Digest + implementation_registry_snapshot_sha256: Sha256Digest + backend_descriptor_bundle_sha256: Sha256Digest + proposal_backend_build_sha256: Sha256Digest + checker_build_sha256: Sha256Digest + claim_definition_ref: DefinitionRef + proof_material_definition_ref: DefinitionRef + proof_material_sha256: Sha256Digest + checker_disposition: Literal[CheckerDisposition.ACCEPTED] + resource_usage: ResourceUsage + certificate_sha256: Sha256Digest + + +class CertifiedSolutionCertificate(_CertificateBase): + """A trusted solution certificate with a complete program/state transition.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/certified-solution-certificate/3.0" + ) + + certificate_kind: Literal["CERTIFIED_SOLUTION"] = "CERTIFIED_SOLUTION" + program_sha256: Sha256Digest + after_scene_state_sha256: Sha256Digest + state_delta_manifest_sha256: Sha256Digest + grounded_obligation_set_sha256: Sha256Digest + + +class ProvenUnsatCertificate(_CertificateBase): + """A trusted complete-domain UNSAT certificate with no program payload.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/proven-unsat-certificate/3.0" + + certificate_kind: Literal["PROVEN_UNSAT"] = "PROVEN_UNSAT" + authorized_domain_sha256: Sha256Digest + complete_domain_coverage_artifact_sha256: Sha256Digest + complete_domain_claim_definition_ref: DefinitionRef + sound_complete_domain_claim_definition_ref: DefinitionRef + + +CounterfactualCertificate: TypeAlias = Annotated[ + CertifiedSolutionCertificate | ProvenUnsatCertificate, + Field(discriminator="certificate_kind"), +] + + +class _ResultBase(HashBoundCanonicalModel): + """Shared direct roots and checker-pair structure for all four outcomes.""" + + SELF_DIGEST_FIELD: ClassVar[str] = "solve_result_sha256" + + structural_outcome_class: str + semantic_problem_sha256: Sha256Digest + solve_request_sha256: Sha256Digest + claim_definition_ref: DefinitionRef + backend_selection_record_sha256: Sha256Digest + checked_proof_outcome_sha256: Sha256Digest | None = None + verifier_dispatch_record_sha256: Sha256Digest | None = None + checker_disposition: CheckerDisposition | None = None + resource_usage: ResourceUsage + solve_result_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_checker_pair(self) -> Self: + has_checked = self.checked_proof_outcome_sha256 is not None + has_dispatch = self.verifier_dispatch_record_sha256 is not None + if has_checked != has_dispatch: + raise ValueError("checker pair must be both present or both absent") + if has_checked and self.checker_disposition is None: + raise ValueError("checker pair requires a checker disposition") + if not has_checked and self.checker_disposition is not None: + raise ValueError("checker disposition requires the checker pair") + return self + + +def _validate_certificate_result_binding( + result: _ResultBase, + certificate: _CertificateBase, +) -> None: + for field_name in ( + "semantic_problem_sha256", + "solve_request_sha256", + "claim_definition_ref", + "backend_selection_record_sha256", + "checked_proof_outcome_sha256", + "verifier_dispatch_record_sha256", + ): + if getattr(result, field_name) != getattr(certificate, field_name): + raise ValueError("result direct root does not match accepted certificate") + if result.checker_disposition is not CheckerDisposition.ACCEPTED: + raise ValueError("certified results require ACCEPTED checker disposition") + + +class CertifiedSolutionResult(_ResultBase): + """A certified result whose direct certificate digest matches its payload.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/certified-solution-result/3.0" + ) + + structural_outcome_class: Literal["CERTIFIED_SOLUTION"] = "CERTIFIED_SOLUTION" + checker_disposition: Literal[CheckerDisposition.ACCEPTED] + accepted_certificate: CertifiedSolutionCertificate + certificate_sha256: Sha256Digest + program_sha256: Sha256Digest + after_scene_state_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_solution_certificate(self) -> Self: + if self.certificate_sha256 != self.accepted_certificate.certificate_sha256: + raise ValueError("certificate digest does not match accepted certificate") + _validate_certificate_result_binding(self, self.accepted_certificate) + if self.program_sha256 != self.accepted_certificate.program_sha256: + raise ValueError("solution program digest does not match certificate") + if ( + self.after_scene_state_sha256 + != self.accepted_certificate.after_scene_state_sha256 + ): + raise ValueError("solution after-state digest does not match certificate") + return self + + +class ProvenUnsatResult(_ResultBase): + """A certified complete-domain negative result without any edit or witness.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/proven-unsat-result/3.0" + + structural_outcome_class: Literal["PROVEN_UNSAT"] = "PROVEN_UNSAT" + checker_disposition: Literal[CheckerDisposition.ACCEPTED] + accepted_certificate: ProvenUnsatCertificate + certificate_sha256: Sha256Digest + complete_domain_coverage_artifact_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_unsat_certificate(self) -> Self: + if self.certificate_sha256 != self.accepted_certificate.certificate_sha256: + raise ValueError("certificate digest does not match accepted certificate") + _validate_certificate_result_binding(self, self.accepted_certificate) + if ( + self.complete_domain_coverage_artifact_sha256 + != self.accepted_certificate.complete_domain_coverage_artifact_sha256 + ): + raise ValueError( + "complete-domain coverage digest does not match certificate" + ) + return self + + +class NoncertifiedWitnessResult(_ResultBase): + """A typed diagnostic witness that cannot contain a trusted certificate.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/noncertified-witness-result/3.0" + ) + + structural_outcome_class: Literal["NONCERTIFIED_WITNESS"] = "NONCERTIFIED_WITNESS" + evidence_claim_definition_ref: DefinitionRef + program_sha256: Sha256Digest | None = None + after_scene_state_sha256: Sha256Digest | None = None + witness_artifact_refs: tuple[_ArtifactReference, ...] = () + model_artifact_refs: tuple[_ArtifactReference, ...] = () + + @model_validator(mode="after") + def _validate_noncertified_witness(self) -> Self: + if self.checker_disposition is CheckerDisposition.ACCEPTED: + raise ValueError( + "noncertified results may not carry ACCEPTED checker disposition" + ) + if (self.program_sha256 is None) != (self.after_scene_state_sha256 is None): + raise ValueError( + "witness program and after-state hashes must appear together" + ) + _require_sorted_unique_by_bytes( + self.witness_artifact_refs, + "witness artifacts", + ) + _require_sorted_unique_by_bytes( + self.model_artifact_refs, + "model artifacts", + ) + if ( + self.program_sha256 is None + and not self.witness_artifact_refs + and not self.model_artifact_refs + ): + raise ValueError( + "noncertified result requires a witness, program, or model" + ) + return self + + +class UnknownResult(_ResultBase): + """A hash-closed terminal unknown with typed reason and optional artifacts.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/unknown-result/3.0" + + structural_outcome_class: Literal["UNKNOWN"] = "UNKNOWN" + reason_claim_definition_ref: DefinitionRef + partial_artifact_refs: tuple[_ArtifactReference, ...] = () + + @model_validator(mode="after") + def _validate_unknown_result(self) -> Self: + if self.checker_disposition is CheckerDisposition.ACCEPTED: + raise ValueError( + "unknown results may not carry ACCEPTED checker disposition" + ) + _require_sorted_unique_by_bytes( + self.partial_artifact_refs, + "unknown partial artifacts", + ) + return self + + +CounterfactualSolveResult: TypeAlias = Annotated[ + CertifiedSolutionResult + | ProvenUnsatResult + | NoncertifiedWitnessResult + | UnknownResult, + Field(discriminator="structural_outcome_class"), +] diff --git a/src/spatialcf/domain/predicates.py b/src/spatialcf/domain/predicates.py new file mode 100644 index 0000000..659df5a --- /dev/null +++ b/src/spatialcf/domain/predicates.py @@ -0,0 +1,831 @@ +"""Closed typed predicate expressions and grounded obligations for M1. + +This module owns only local structural validation. Definition resolution, +semantic evaluation, and implementation capability checks belong to the later +static registry; no adapter, core, geometry, or runtime discovery is reachable +from these immutable domain contracts. +""" + +from __future__ import annotations + +from typing import Annotated, ClassVar, Literal, Self, TypeAlias + +from pydantic import Field, StrictBool, StrictInt, TypeAdapter, model_validator + +from spatialcf.domain.base import CanonicalId, CanonicalModel, Sha256Digest +from spatialcf.domain.definitions import ( + CapabilityRef, + DefinitionRef, + HashBoundCanonicalModel, + ReferenceValue, + SchemaRef, + TypedValue, + ValueKind, + canonical_json_bytes, + canonical_sha256, +) + +__all__ = ( + "AfterGoal", + "AllOfFormula", + "AnyOfFormula", + "BeforePrecondition", + "ExactlyKFormula", + "ExistsFormula", + "FiniteEntitySet", + "ForAllFormula", + "GroundedObligation", + "GroundedObligationSet", + "ImpliesFormula", + "NotFormula", + "ObservationObligation", + "PredicateAtom", + "PredicateDefinition", + "PreservationInvariant", +) + +_GROUNDING_ENTITY_SET_HASH_DOMAIN = "spatialcf/counterfactual/grounding-entity-set/3.0" +_GROUNDED_OBLIGATION_ID_DOMAIN = "spatialcf/counterfactual/grounded-obligation/3.0" + + +def _require_sorted_unique( + values: tuple[str, ...], + label: str, + *, + nonempty: bool = False, +) -> None: + if nonempty and not values: + raise ValueError(f"{label} must not be empty") + if values != tuple(sorted(values, key=canonical_json_bytes)): + raise ValueError(f"{label} must be sorted") + if len(set(values)) != len(values): + raise ValueError(f"{label} must not contain duplicate entries") + + +def _require_unique(values: tuple[str, ...], label: str) -> None: + if len(set(values)) != len(values): + raise ValueError(f"{label} must not contain duplicate entries") + + +class PredicateDefinition(HashBoundCanonicalModel): + """The complete local meaning closure for one predicate definition.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/predicate-definition/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "definition_sha256" + + predicate_ref: DefinitionRef + operand_schema_refs: tuple[SchemaRef, ...] + state_context_policy_ref: DefinitionRef + frame_requirement_ref: DefinitionRef + measurement_definition_ref: DefinitionRef + measurement_unit_ref: DefinitionRef + comparator_definition_ref: DefinitionRef + boundary_policy_ref: DefinitionRef + tolerance_policy_ref: DefinitionRef + uncertainty_policy_ref: DefinitionRef + observation_prerequisite_template_refs: tuple[DefinitionRef, ...] + evaluator_capability_ref: CapabilityRef + verifier_capability_ref: CapabilityRef + admissible_claim_definition_refs: tuple[DefinitionRef, ...] + definition_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_definition_closure(self) -> Self: + _require_unique(self.operand_schema_refs, "predicate operand schemas") + _require_sorted_unique( + self.observation_prerequisite_template_refs, + "predicate observation prerequisite templates", + ) + _require_sorted_unique( + self.admissible_claim_definition_refs, + "predicate admissible claim definitions", + ) + closure_refs = ( + self.state_context_policy_ref, + self.frame_requirement_ref, + self.measurement_definition_ref, + self.measurement_unit_ref, + self.comparator_definition_ref, + self.boundary_policy_ref, + self.tolerance_policy_ref, + self.uncertainty_policy_ref, + *self.observation_prerequisite_template_refs, + *self.admissible_claim_definition_refs, + ) + _require_unique(closure_refs, "predicate definition closure") + _require_unique( + (self.evaluator_capability_ref, self.verifier_capability_ref), + "predicate capability closure", + ) + return self + + +class _GroundableFormula(CanonicalModel): + """Private common grounding entry point for every closed formula node.""" + + def ground(self) -> _StateFormula | bool: + """Structurally expand finite quantifiers after validating closure.""" + + _assert_closed_formula(self, ()) + return _ground_formula(self, ()) + + +class PredicateAtom(_GroundableFormula): + """One ordered predicate application without a state selector.""" + + kind: Literal["PREDICATE_ATOM"] = "PREDICATE_ATOM" + predicate_ref: DefinitionRef + operands: tuple[TypedValue, ...] + + +class FiniteEntitySet(CanonicalModel): + """An explicit finite domain and its one statically named bound variable.""" + + variable_ref: CanonicalId + entity_schema_ref: SchemaRef + entities: tuple[TypedValue, ...] + + @model_validator(mode="after") + def _validate_explicit_entity_domain(self) -> Self: + if not self.variable_ref.startswith("variable:"): + raise ValueError("finite entity set variable must start with 'variable:'") + encoded = tuple(canonical_json_bytes(entity) for entity in self.entities) + if len(set(encoded)) != len(encoded): + raise ValueError("finite entity sets must not contain duplicate entities") + if encoded != tuple(sorted(encoded)): + raise ValueError("finite entity sets must be sorted") + for entity in self.entities: + if entity.value_schema_ref != self.entity_schema_ref: + raise ValueError( + "finite entity set entity schema must match its domain" + ) + if not isinstance(entity.payload, ReferenceValue) or ( + entity.payload.kind is not ValueKind.ENTITY_REF + ): + raise ValueError( + "finite entity sets must contain typed entity references" + ) + if entity.payload.reference.startswith("variable:"): + raise ValueError("finite entity sets may not discover another variable") + return self + + +class NotFormula(_GroundableFormula): + kind: Literal["NOT"] = "NOT" + formula: _StateFormula + + +class AllOfFormula(_GroundableFormula): + kind: Literal["ALL_OF"] = "ALL_OF" + formulas: tuple[_StateFormula, ...] + + @model_validator(mode="after") + def _normalize_formulas(self) -> Self: + object.__setattr__( + self, + "formulas", + _canonicalize_commutative_formulas(self.formulas, "all-of formulas"), + ) + return self + + +class AnyOfFormula(_GroundableFormula): + kind: Literal["ANY_OF"] = "ANY_OF" + formulas: tuple[_StateFormula, ...] + + @model_validator(mode="after") + def _normalize_formulas(self) -> Self: + object.__setattr__( + self, + "formulas", + _canonicalize_commutative_formulas(self.formulas, "any-of formulas"), + ) + return self + + +class ImpliesFormula(_GroundableFormula): + kind: Literal["IMPLIES"] = "IMPLIES" + antecedent: _StateFormula + consequent: _StateFormula + + +class ExactlyKFormula(_GroundableFormula): + kind: Literal["EXACTLY_K"] = "EXACTLY_K" + k: Annotated[StrictInt, Field(ge=0)] + formulas: tuple[_StateFormula, ...] + + @model_validator(mode="after") + def _normalize_formulas_and_validate_k(self) -> Self: + formulas = _canonicalize_commutative_formulas( + self.formulas, + "exactly-k formulas", + ) + if self.k > len(formulas): + raise ValueError("exactly-k k must not exceed its formula count") + object.__setattr__(self, "formulas", formulas) + return self + + +class ForAllFormula(_GroundableFormula): + kind: Literal["FOR_ALL"] = "FOR_ALL" + entity_set: FiniteEntitySet + formula: _StateFormula + + +class ExistsFormula(_GroundableFormula): + kind: Literal["EXISTS"] = "EXISTS" + entity_set: FiniteEntitySet + formula: _StateFormula + + +_StateFormula: TypeAlias = Annotated[ + PredicateAtom + | NotFormula + | AllOfFormula + | AnyOfFormula + | ImpliesFormula + | ExactlyKFormula + | ForAllFormula + | ExistsFormula, + Field(discriminator="kind"), +] + +# Finite grounding may reduce an otherwise closed formula to True or False. +# Those strict terminals are legal only as a context wrapper's root; every +# recursive formula field above remains the closed eight-case AST. +_GroundedContextFormula: TypeAlias = StrictBool | _StateFormula + + +class BeforePrecondition(CanonicalModel): + """A before-state formula or strict terminal produced by finite grounding.""" + + kind: Literal["BEFORE_PRECONDITION"] = "BEFORE_PRECONDITION" + formula: _GroundedContextFormula + + @model_validator(mode="after") + def _validate_closed_formula(self) -> Self: + _assert_closed_context_formula(self.formula) + return self + + +class AfterGoal(CanonicalModel): + """An after-state formula or strict terminal produced by finite grounding.""" + + kind: Literal["AFTER_GOAL"] = "AFTER_GOAL" + formula: _GroundedContextFormula + + @model_validator(mode="after") + def _validate_closed_formula(self) -> Self: + _assert_closed_context_formula(self.formula) + return self + + +class PreservationInvariant(CanonicalModel): + """An explicit before/after transition obligation with grounded terminals.""" + + kind: Literal["PRESERVATION_INVARIANT"] = "PRESERVATION_INVARIANT" + before_formula: _GroundedContextFormula + after_formula: _GroundedContextFormula + transition_comparator_ref: DefinitionRef + + @model_validator(mode="after") + def _validate_closed_formulas(self) -> Self: + _assert_closed_context_formula(self.before_formula) + _assert_closed_context_formula(self.after_formula) + return self + + +class ObservationObligation(CanonicalModel): + """A semantic observation with a formula or finite-grounding terminal.""" + + kind: Literal["OBSERVATION_OBLIGATION"] = "OBSERVATION_OBLIGATION" + phase: Literal["BEFORE", "AFTER"] + formula: _GroundedContextFormula + evidence_policy_ref: DefinitionRef + + @model_validator(mode="after") + def _validate_closed_formula(self) -> Self: + _assert_closed_context_formula(self.formula) + return self + + +_ContextWrapper: TypeAlias = Annotated[ + BeforePrecondition | AfterGoal | PreservationInvariant | ObservationObligation, + Field(discriminator="kind"), +] + + +class GroundedObligation(CanonicalModel): + """One fully grounded context plus source refs carried on its wire. + + The context-derived ``obligation_id`` deliberately stays non-wire. Source + references remain wire data and therefore contribute to the containing + grounded-obligation set's canonical self digest. + """ + + context: _ContextWrapper + source_definition_refs: tuple[DefinitionRef, ...] + + @model_validator(mode="after") + def _validate_grounded_obligation(self) -> Self: + _require_sorted_unique( + self.source_definition_refs, + "grounded obligation source definition references", + nonempty=True, + ) + if _contains_quantifier(_context_formulas(self.context)): + raise ValueError( + "grounded obligations must not contain unexpanded quantifiers" + ) + return self + + @property + def obligation_id(self) -> CanonicalId: + """Stable context-derived semantic ID, deliberately excluding sources.""" + + return f"obligation:{canonical_sha256(self.context, domain=_GROUNDED_OBLIGATION_ID_DOMAIN)}" + + @property + def _semantic_bytes(self) -> bytes: + return canonical_json_bytes(self.context) + + +class GroundedObligationSet(HashBoundCanonicalModel): + """The complete hash-bound four-way partition and source closure.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/grounded-obligation-set/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "grounded_obligation_set_sha256" + + before_preconditions: tuple[GroundedObligation, ...] = () + after_goals: tuple[GroundedObligation, ...] = () + preservation_invariants: tuple[GroundedObligation, ...] = () + observation_obligations: tuple[GroundedObligation, ...] = () + grounding_entity_sets: tuple[FiniteEntitySet, ...] = () + source_definition_refs: tuple[DefinitionRef, ...] + grounding_entity_set_sha256: Sha256Digest + grounded_obligation_set_sha256: Sha256Digest + + @classmethod + def seal(cls, **values) -> Self: + """Normalize semantic duplicates before binding the two declared hashes.""" + + for field_name in ( + "source_definition_refs", + "grounding_entity_set_sha256", + ): + if field_name in values: + raise ValueError(f"seal() derives {field_name}") + return super().seal(**values | cls._canonical_values(values)) + + @classmethod + def _canonical_values(cls, values): + before_preconditions = _obligation_tuple(values.get("before_preconditions", ())) + after_goals = _obligation_tuple(values.get("after_goals", ())) + preservation_invariants = _obligation_tuple( + values.get("preservation_invariants", ()) + ) + observation_obligations = _obligation_tuple( + values.get("observation_obligations", ()) + ) + grounding_entity_sets = _finite_entity_set_tuple( + values.get("grounding_entity_sets", ()) + ) + normalized_before = _normalize_partition( + before_preconditions, + BeforePrecondition, + "before precondition partition", + ) + normalized_after = _normalize_partition( + after_goals, + AfterGoal, + "after goal partition", + ) + normalized_preservation = _normalize_partition( + preservation_invariants, + PreservationInvariant, + "preservation invariant partition", + ) + normalized_observations = _normalize_partition( + observation_obligations, + ObservationObligation, + "observation obligation partition", + ) + normalized_entity_sets = _normalize_entity_sets(grounding_entity_sets) + source_definition_refs = _sorted_unique_refs( + tuple( + reference + for obligation in ( + *normalized_before, + *normalized_after, + *normalized_preservation, + *normalized_observations, + ) + for reference in obligation.source_definition_refs + ) + ) + return { + "before_preconditions": normalized_before, + "after_goals": normalized_after, + "preservation_invariants": normalized_preservation, + "observation_obligations": normalized_observations, + "grounding_entity_sets": normalized_entity_sets, + "source_definition_refs": source_definition_refs, + "grounding_entity_set_sha256": canonical_sha256( + normalized_entity_sets, + domain=_GROUNDING_ENTITY_SET_HASH_DOMAIN, + ), + } + + @model_validator(mode="after") + def _validate_canonical_partition(self) -> Self: + canonical = self._canonical_values( + { + "before_preconditions": self.before_preconditions, + "after_goals": self.after_goals, + "preservation_invariants": self.preservation_invariants, + "observation_obligations": self.observation_obligations, + "grounding_entity_sets": self.grounding_entity_sets, + } + ) + for field_name in ( + "before_preconditions", + "after_goals", + "preservation_invariants", + "observation_obligations", + "grounding_entity_sets", + "source_definition_refs", + "grounding_entity_set_sha256", + ): + if getattr(self, field_name) != canonical[field_name]: + raise ValueError( + "grounded obligation set must use its canonical partition" + ) + return self + + +def _canonicalize_commutative_formulas( + formulas: tuple[_StateFormula, ...], + label: str, +) -> tuple[_StateFormula, ...]: + if not formulas: + raise ValueError(f"{label} must not be empty") + encoded = tuple(canonical_json_bytes(formula) for formula in formulas) + if len(set(encoded)) != len(encoded): + raise ValueError(f"{label} must not contain duplicate formulas") + return tuple( + formula + for _encoded, formula in sorted( + zip(encoded, formulas, strict=True), key=lambda item: item[0] + ) + ) + + +def _variable_ref(value: TypedValue) -> CanonicalId | None: + if ( + isinstance(value.payload, ReferenceValue) + and value.payload.kind is ValueKind.ENTITY_REF + and value.payload.reference.startswith("variable:") + ): + return value.payload.reference + return None + + +def _assert_closed_formula( + formula: _StateFormula, + bindings: tuple[tuple[CanonicalId, SchemaRef, TypedValue | None], ...], +) -> None: + if isinstance(formula, PredicateAtom): + for operand in formula.operands: + variable_ref = _variable_ref(operand) + if variable_ref is None: + continue + binding = _find_binding(variable_ref, bindings) + if binding is None: + raise ValueError(f"unbound variable {variable_ref!r}") + if operand.value_schema_ref != binding[1]: + raise ValueError(f"bound variable type mismatch for {variable_ref!r}") + return + if isinstance(formula, NotFormula): + _assert_closed_formula(formula.formula, bindings) + return + if isinstance(formula, (AllOfFormula, AnyOfFormula, ExactlyKFormula)): + for child in formula.formulas: + _assert_closed_formula(child, bindings) + return + if isinstance(formula, ImpliesFormula): + _assert_closed_formula(formula.antecedent, bindings) + _assert_closed_formula(formula.consequent, bindings) + return + _assert_closed_formula_quantifier(formula, bindings) + + +def _assert_closed_context_formula(formula: _GroundedContextFormula) -> None: + if type(formula) is bool: + return + _assert_closed_formula(formula, ()) + + +def _assert_closed_formula_quantifier( + formula: ForAllFormula | ExistsFormula, + bindings: tuple[tuple[CanonicalId, SchemaRef, TypedValue | None], ...], +) -> None: + if _find_binding(formula.entity_set.variable_ref, bindings) is not None: + raise ValueError("quantifier variables must not shadow an outer binding") + _assert_closed_formula( + formula.formula, + bindings + + ( + ( + formula.entity_set.variable_ref, + formula.entity_set.entity_schema_ref, + None, + ), + ), + ) + + +def _find_binding( + variable_ref: CanonicalId, + bindings: tuple[tuple[CanonicalId, SchemaRef, TypedValue | None], ...], +) -> tuple[CanonicalId, SchemaRef, TypedValue | None] | None: + for binding in reversed(bindings): + if binding[0] == variable_ref: + return binding + return None + + +def _ground_formula( + formula: _StateFormula, + bindings: tuple[tuple[CanonicalId, SchemaRef, TypedValue | None], ...], +) -> _StateFormula | bool: + if isinstance(formula, PredicateAtom): + operands: list[TypedValue] = [] + for operand in formula.operands: + variable_ref = _variable_ref(operand) + if variable_ref is None: + operands.append(operand) + continue + binding = _find_binding(variable_ref, bindings) + if binding is None: + raise ValueError(f"unbound variable {variable_ref!r}") + if operand.value_schema_ref != binding[1]: + raise ValueError(f"bound variable type mismatch for {variable_ref!r}") + if binding[2] is None: + raise ValueError(f"unbound variable {variable_ref!r}") + operands.append(binding[2]) + return formula.model_copy(update={"operands": tuple(operands)}) + if isinstance(formula, NotFormula): + grounded = _ground_formula(formula.formula, bindings) + return not grounded if type(grounded) is bool else NotFormula(formula=grounded) + if isinstance(formula, AllOfFormula): + return _ground_all( + tuple(_ground_formula(child, bindings) for child in formula.formulas) + ) + if isinstance(formula, AnyOfFormula): + return _ground_any( + tuple(_ground_formula(child, bindings) for child in formula.formulas) + ) + if isinstance(formula, ImpliesFormula): + antecedent = _ground_formula(formula.antecedent, bindings) + consequent = _ground_formula(formula.consequent, bindings) + if antecedent is False or consequent is True: + return True + if antecedent is True: + return consequent + if consequent is False: + return NotFormula(formula=antecedent) + return ImpliesFormula(antecedent=antecedent, consequent=consequent) + if isinstance(formula, ExactlyKFormula): + return _ground_exactly_k(formula, bindings) + if isinstance(formula, ForAllFormula): + return _ground_all( + tuple( + _ground_formula( + formula.formula, + bindings + + ( + ( + formula.entity_set.variable_ref, + formula.entity_set.entity_schema_ref, + entity, + ), + ), + ) + for entity in formula.entity_set.entities + ) + ) + return _ground_any( + tuple( + _ground_formula( + formula.formula, + bindings + + ( + ( + formula.entity_set.variable_ref, + formula.entity_set.entity_schema_ref, + entity, + ), + ), + ) + for entity in formula.entity_set.entities + ) + ) + + +def _ground_all(values: tuple[_StateFormula | bool, ...]) -> _StateFormula | bool: + if any(value is False for value in values): + return False + formulas = _unique_grounded_formulas( + tuple(value for value in values if type(value) is not bool) + ) + if not formulas: + return True + if len(formulas) == 1: + return formulas[0] + return AllOfFormula(formulas=formulas) + + +def _ground_any(values: tuple[_StateFormula | bool, ...]) -> _StateFormula | bool: + if any(value is True for value in values): + return True + formulas = _unique_grounded_formulas( + tuple(value for value in values if type(value) is not bool) + ) + if not formulas: + return False + if len(formulas) == 1: + return formulas[0] + return AnyOfFormula(formulas=formulas) + + +def _ground_exactly_k( + formula: ExactlyKFormula, + bindings: tuple[tuple[CanonicalId, SchemaRef, TypedValue | None], ...], +) -> _StateFormula | bool: + values = tuple(_ground_formula(child, bindings) for child in formula.formulas) + true_count = sum(value is True for value in values) + formulas = tuple(value for value in values if type(value) is not bool) + required_k = formula.k - true_count + if required_k < 0 or required_k > len(formulas): + return False + if not formulas: + return required_k == 0 + grouped_formulas = _group_grounded_formulas(formulas) + if all(multiplicity == 1 for _formula, multiplicity in grouped_formulas): + return ExactlyKFormula( + k=required_k, + formulas=tuple(formula for formula, _multiplicity in grouped_formulas), + ) + return _lower_weighted_exactly_k(grouped_formulas, required_k) + + +def _unique_grounded_formulas( + formulas: tuple[_StateFormula, ...], +) -> tuple[_StateFormula, ...]: + return tuple( + formula for formula, _multiplicity in _group_grounded_formulas(formulas) + ) + + +def _group_grounded_formulas( + formulas: tuple[_StateFormula, ...], +) -> tuple[tuple[_StateFormula, int], ...]: + grouped: list[tuple[_StateFormula, int]] = [] + last_encoded: bytes | None = None + for encoded, formula in sorted( + ((canonical_json_bytes(formula), formula) for formula in formulas), + key=lambda item: item[0], + ): + if encoded == last_encoded: + previous_formula, multiplicity = grouped[-1] + grouped[-1] = (previous_formula, multiplicity + 1) + else: + grouped.append((formula, 1)) + last_encoded = encoded + return tuple(grouped) + + +def _lower_weighted_exactly_k( + grouped_formulas: tuple[tuple[_StateFormula, int], ...], + required_k: int, +) -> _StateFormula | bool: + clauses: list[_StateFormula | bool] = [] + for assignment in range(1 << len(grouped_formulas)): + weighted_total = sum( + multiplicity + for index, (_formula, multiplicity) in enumerate(grouped_formulas) + if assignment & (1 << index) + ) + if weighted_total != required_k: + continue + clauses.append( + _ground_all( + tuple( + formula + if assignment & (1 << index) + else NotFormula(formula=formula) + for index, (formula, _multiplicity) in enumerate(grouped_formulas) + ) + ) + ) + return _ground_any(tuple(clauses)) + + +def _context_formulas( + context: _ContextWrapper, +) -> tuple[_GroundedContextFormula, ...]: + if isinstance(context, PreservationInvariant): + return (context.before_formula, context.after_formula) + return (context.formula,) + + +def _contains_quantifier(formulas: tuple[_GroundedContextFormula, ...]) -> bool: + for formula in formulas: + if type(formula) is bool: + continue + if isinstance(formula, (ForAllFormula, ExistsFormula)): + return True + if isinstance(formula, NotFormula) and _contains_quantifier((formula.formula,)): + return True + if isinstance(formula, (AllOfFormula, AnyOfFormula, ExactlyKFormula)) and ( + _contains_quantifier(formula.formulas) + ): + return True + if isinstance(formula, ImpliesFormula) and _contains_quantifier( + (formula.antecedent, formula.consequent) + ): + return True + return False + + +def _obligation_tuple(value) -> tuple[GroundedObligation, ...]: + return TypeAdapter(tuple[GroundedObligation, ...]).validate_python( + value, strict=True + ) + + +def _finite_entity_set_tuple(value) -> tuple[FiniteEntitySet, ...]: + return TypeAdapter(tuple[FiniteEntitySet, ...]).validate_python(value, strict=True) + + +def _normalize_partition( + obligations: tuple[GroundedObligation, ...], + wrapper_type: type[CanonicalModel], + label: str, +) -> tuple[GroundedObligation, ...]: + for obligation in obligations: + if not isinstance(obligation.context, wrapper_type): + raise TypeError(f"{label} contains an obligation in the wrong partition") + ordered = tuple( + sorted(obligations, key=lambda obligation: obligation._semantic_bytes) + ) + normalized: list[GroundedObligation] = [] + for obligation in ordered: + if normalized and normalized[-1]._semantic_bytes == obligation._semantic_bytes: + merged_refs = _sorted_unique_refs( + normalized[-1].source_definition_refs + + obligation.source_definition_refs + ) + normalized[-1] = GroundedObligation( + context=normalized[-1].context, + source_definition_refs=merged_refs, + ) + else: + normalized.append(obligation) + return tuple(normalized) + + +def _normalize_entity_sets( + entity_sets: tuple[FiniteEntitySet, ...], +) -> tuple[FiniteEntitySet, ...]: + encoded = tuple(canonical_json_bytes(entity_set) for entity_set in entity_sets) + if len(set(encoded)) != len(encoded): + raise ValueError("grounding entity sets must not contain duplicate domains") + return tuple( + entity_set + for _encoded, entity_set in sorted( + zip(encoded, entity_sets, strict=True), key=lambda item: item[0] + ) + ) + + +def _sorted_unique_refs( + references: tuple[DefinitionRef, ...], +) -> tuple[DefinitionRef, ...]: + return tuple(sorted(set(references), key=canonical_json_bytes)) + + +PredicateAtom.model_rebuild() +NotFormula.model_rebuild() +AllOfFormula.model_rebuild() +AnyOfFormula.model_rebuild() +ImpliesFormula.model_rebuild() +ExactlyKFormula.model_rebuild() +ForAllFormula.model_rebuild() +ExistsFormula.model_rebuild() +BeforePrecondition.model_rebuild() +AfterGoal.model_rebuild() +PreservationInvariant.model_rebuild() +ObservationObligation.model_rebuild() +GroundedObligation.model_rebuild() +GroundedObligationSet.model_rebuild() diff --git a/src/spatialcf/domain/profiles.py b/src/spatialcf/domain/profiles.py new file mode 100644 index 0000000..b21f2f8 --- /dev/null +++ b/src/spatialcf/domain/profiles.py @@ -0,0 +1,587 @@ +"""Immutable profile, policy, and availability contracts for M1. + +This module closes only local structural invariants. It intentionally does +not resolve definition references, select a backend, execute routing, track a +resource ledger, or dispatch a checker; those cross-record operations belong +to the later static registry. +""" + +from __future__ import annotations + +from typing import Annotated, ClassVar, Self, TypeVar + +from pydantic import BeforeValidator, Field, StrictBool, StrictInt, model_validator + +from spatialcf.domain.base import ( + CanonicalId, + CanonicalModel, + NonNegativeFiniteFloat, + Sha256Digest, +) +from spatialcf.domain.definitions import ( + CapabilityRef, + DefinitionRef, + HashBoundCanonicalModel, + SchemaRef, + canonical_json_bytes, +) +from spatialcf.domain.operators import StateVariableRef, TypedVariableBound + +__all__ = ( + "ActionSpaceProfile", + "BackendDescriptorBundle", + "BackendRoutingPolicy", + "CounterfactualSolverConfig", + "ImplementationOwnerBinding", + "ImplementationRegistrySnapshot", + "InterventionAuthorization", + "ObjectiveExpression", + "ObjectiveTerm", + "ProofPolicy", + "ResourceLimit", + "ResourcePolicy", + "SemanticsProfile", + "SolverBackendDescriptor", + "UnavailableBackendRecord", +) + +_ValueT = TypeVar("_ValueT") +_PositiveStrictInt = Annotated[StrictInt, Field(gt=0)] + + +def _require_profile_ref(value: str) -> str: + if isinstance(value, str): + profile_prefix = "spatialcf/" + if not value.startswith(profile_prefix) or "*" in value: + raise ValueError("profile references must be exact spatialcf versioned IDs") + profile_path_and_version = value[len(profile_prefix) :] + if profile_path_and_version.count("@") != 1: + raise ValueError("profile references must be exact spatialcf versioned IDs") + profile_path, profile_version = profile_path_and_version.split("@") + if ( + not profile_path + or not profile_version + or any(segment in ("", ".", "..") for segment in profile_path.split("/")) + ): + raise ValueError("profile references must be exact spatialcf versioned IDs") + return value + + +def _has_exact_prefixed_suffix(value: str, prefixes: tuple[str, ...]) -> bool: + return "*" not in value and any( + value.startswith(prefix) and len(value) > len(prefix) for prefix in prefixes + ) + + +def _require_exact_entity_id(value: str) -> str: + if isinstance(value, str) and not _has_exact_prefixed_suffix(value, ("entity:",)): + raise ValueError("editable entities must use exact entity IDs") + return value + + +def _require_owner_ref(value: str) -> str: + if isinstance(value, str) and not _has_exact_prefixed_suffix(value, ("owner:",)): + raise ValueError("implementation owners must use exact owner references") + return value + + +def _require_backend_ref(value: str) -> str: + if isinstance(value, str) and not _has_exact_prefixed_suffix(value, ("backend:",)): + raise ValueError("backend references must use exact backend IDs") + return value + + +def _require_definition_or_capability_ref(value: str) -> str: + if isinstance(value, str) and not _has_exact_prefixed_suffix( + value, + ("definition:", "capability:"), + ): + raise ValueError("owner bindings must name an exact definition or capability") + return value + + +ProfileRef = Annotated[CanonicalId, BeforeValidator(_require_profile_ref)] +ExactEntityId = Annotated[CanonicalId, BeforeValidator(_require_exact_entity_id)] +OwnerRef = Annotated[CanonicalId, BeforeValidator(_require_owner_ref)] +BackendRef = Annotated[CanonicalId, BeforeValidator(_require_backend_ref)] +DefinitionOrCapabilityRef = Annotated[ + CanonicalId, + BeforeValidator(_require_definition_or_capability_ref), +] + + +def _require_sorted_unique_by_bytes( + values: tuple[_ValueT, ...], + label: str, + *, + nonempty: bool = False, +) -> None: + if nonempty and not values: + raise ValueError(f"{label} must not be empty") + encoded = tuple(canonical_json_bytes(value) for value in values) + if encoded != tuple(sorted(encoded)): + raise ValueError(f"{label} must be sorted") + if len(set(encoded)) != len(encoded): + raise ValueError(f"{label} must not contain duplicate entries") + + +def _state_leaf_key(reference: StateVariableRef) -> bytes: + return canonical_json_bytes( + ( + reference.state_schema_ref, + reference.fact_family_ref, + reference.entity_or_fact_key, + reference.field_path_ref, + ) + ) + + +def _require_sorted_unique_state_refs( + references: tuple[StateVariableRef, ...], + label: str, + *, + nonempty: bool = False, +) -> None: + _require_sorted_unique_by_bytes(references, label, nonempty=nonempty) + leaf_keys = tuple(_state_leaf_key(reference) for reference in references) + if len(set(leaf_keys)) != len(leaf_keys): + raise ValueError(f"{label} must not claim one leaf through two schemas") + if any("*" in reference.entity_or_fact_key for reference in references): + raise ValueError(f"{label} must name exact leaf references") + + +class SemanticsProfile(HashBoundCanonicalModel): + """The immutable interpretation closure shared by compatible problems.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/semantics-profile/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "semantics_profile_sha256" + + semantics_profile_ref: ProfileRef + accepted_scene_and_fact_schema_refs: tuple[SchemaRef, ...] + predicate_definition_refs: tuple[DefinitionRef, ...] + transition_semantics_refs: tuple[DefinitionRef, ...] + objective_definition_refs: tuple[DefinitionRef, ...] + numeric_semantics_ref: DefinitionRef + completeness_policy_ref: DefinitionRef + uncertainty_policy_ref: DefinitionRef + derived_fact_rule_refs: tuple[DefinitionRef, ...] + observation_obligation_policy_ref: DefinitionRef + semantics_profile_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_reference_sets(self) -> Self: + _require_sorted_unique_by_bytes( + self.accepted_scene_and_fact_schema_refs, + "accepted scene and fact schemas", + ) + _require_sorted_unique_by_bytes( + self.predicate_definition_refs, + "predicate definitions", + ) + _require_sorted_unique_by_bytes( + self.transition_semantics_refs, + "transition semantics", + ) + _require_sorted_unique_by_bytes( + self.objective_definition_refs, + "objective definitions", + ) + _require_sorted_unique_by_bytes( + self.derived_fact_rule_refs, + "derived fact rules", + ) + return self + + +class ActionSpaceProfile(HashBoundCanonicalModel): + """The reusable state/action capability universe without implementation code.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/action-space-profile/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "action_space_profile_sha256" + + action_space_profile_ref: ProfileRef + accepted_scene_schema_refs: tuple[SchemaRef, ...] + state_variable_definition_refs: tuple[DefinitionRef, ...] + allowed_operator_refs: tuple[DefinitionRef, ...] + mandatory_invariant_template_refs: tuple[DefinitionRef, ...] + predicate_capability_refs: tuple[CapabilityRef, ...] + objective_capability_refs: tuple[CapabilityRef, ...] + numeric_semantics_ref: DefinitionRef + allowed_claim_definition_refs: tuple[DefinitionRef, ...] + backend_capability_requirements: tuple[CapabilityRef, ...] + adapter_capability_requirements: tuple[CapabilityRef, ...] + publication_proof_policy_ref: DefinitionRef + action_space_profile_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_capability_sets(self) -> Self: + _require_sorted_unique_by_bytes( + self.accepted_scene_schema_refs, + "accepted scene schemas", + ) + _require_sorted_unique_by_bytes( + self.state_variable_definition_refs, + "state variable definitions", + ) + _require_sorted_unique_by_bytes( + self.allowed_operator_refs, + "allowed operators", + ) + _require_sorted_unique_by_bytes( + self.mandatory_invariant_template_refs, + "mandatory invariant templates", + ) + _require_sorted_unique_by_bytes( + self.predicate_capability_refs, + "predicate capabilities", + ) + _require_sorted_unique_by_bytes( + self.objective_capability_refs, + "objective capabilities", + ) + _require_sorted_unique_by_bytes( + self.allowed_claim_definition_refs, + "allowed claims", + ) + _require_sorted_unique_by_bytes( + self.backend_capability_requirements, + "backend capability requirements", + nonempty=True, + ) + _require_sorted_unique_by_bytes( + self.adapter_capability_requirements, + "adapter capability requirements", + ) + return self + + +class InterventionAuthorization(HashBoundCanonicalModel): + """Request-local exact write authority, never a profile-level capability grant.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/intervention-authorization/3.0" + ) + SELF_DIGEST_FIELD: ClassVar[str] = "intervention_authorization_sha256" + + editable_entity_ids: tuple[ExactEntityId, ...] + allowed_operator_refs: tuple[DefinitionRef, ...] + authorized_primary_write_set: tuple[StateVariableRef, ...] + variable_bounds: tuple[TypedVariableBound, ...] + maximum_program_steps: _PositiveStrictInt + maximum_edited_entities: _PositiveStrictInt + required_derived_rule_refs: tuple[DefinitionRef, ...] + complete_state_delta_policy_ref: DefinitionRef + intervention_authorization_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_exact_authorization(self) -> Self: + _require_sorted_unique_by_bytes( + self.editable_entity_ids, + "editable entity IDs", + nonempty=True, + ) + _require_sorted_unique_by_bytes( + self.allowed_operator_refs, + "authorized operators", + nonempty=True, + ) + _require_sorted_unique_state_refs( + self.authorized_primary_write_set, + "authorized primary write set", + nonempty=True, + ) + _require_sorted_unique_by_bytes( + self.required_derived_rule_refs, + "required derived rules", + ) + _require_sorted_unique_by_bytes( + self.variable_bounds, + "variable bounds", + ) + bound_keys = tuple( + _state_leaf_key(bound.state_variable_ref) for bound in self.variable_bounds + ) + if len(set(bound_keys)) != len(bound_keys): + raise ValueError("variable bounds must not duplicate one state leaf") + authorized_keys = { + _state_leaf_key(reference) + for reference in self.authorized_primary_write_set + } + if any(key not in authorized_keys for key in bound_keys): + raise ValueError("variable bounds must target authorized primary writes") + if any( + "*" in bound.state_variable_ref.entity_or_fact_key + for bound in self.variable_bounds + ): + raise ValueError("variable bounds must name exact leaf references") + return self + + +class ObjectiveTerm(CanonicalModel): + """One ordered, typed term whose metric semantics remain definition-bound.""" + + term_id: CanonicalId + objective_definition_ref: DefinitionRef + input_selector_definition_ref: DefinitionRef + unit_ref: DefinitionRef + normalization_definition_ref: DefinitionRef + + +class ObjectiveExpression(HashBoundCanonicalModel): + """A deterministic objective expression with preserved declared term order.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/objective-expression/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "objective_expression_sha256" + + aggregation_definition_ref: DefinitionRef + terms: tuple[ObjectiveTerm, ...] + deterministic_tie_break_definition_ref: DefinitionRef + objective_expression_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_ordered_terms(self) -> Self: + if not self.terms: + raise ValueError("objective terms must not be empty") + term_ids = tuple(term.term_id for term in self.terms) + if len(set(term_ids)) != len(term_ids): + raise ValueError("objective expression must not contain duplicate term IDs") + return self + + +class ProofPolicy(HashBoundCanonicalModel): + """The immutable claim/checker policy required to publish a terminal record.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/proof-policy/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "proof_policy_sha256" + + proof_policy_ref: DefinitionRef + accepted_claim_definition_refs: tuple[DefinitionRef, ...] + required_checker_capability_refs: tuple[CapabilityRef, ...] + publication_minimum_claim_ref: DefinitionRef + permit_noncertified_terminal_records: StrictBool + proof_policy_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_policy_sets(self) -> Self: + _require_sorted_unique_by_bytes( + self.accepted_claim_definition_refs, + "accepted proof claims", + nonempty=True, + ) + _require_sorted_unique_by_bytes( + self.required_checker_capability_refs, + "required checker capabilities", + nonempty=True, + ) + return self + + +class ResourceLimit(CanonicalModel): + """A finite limit whose unit, counting, and overflow semantics are referenced.""" + + definition_ref: DefinitionRef + finite_limit: NonNegativeFiniteFloat + + +class ResourcePolicy(HashBoundCanonicalModel): + """The declarative resource closure; it does not contain a runtime ledger.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/resource-policy/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "resource_policy_sha256" + + resource_policy_ref: DefinitionRef + limits: tuple[ResourceLimit, ...] + exhaustion_claim_ref: DefinitionRef + shared_ledger_policy_ref: DefinitionRef + resource_policy_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_limits(self) -> Self: + _require_sorted_unique_by_bytes(self.limits, "resource limits") + limit_refs = tuple(limit.definition_ref for limit in self.limits) + if len(set(limit_refs)) != len(limit_refs): + raise ValueError("resource limits must not duplicate one definition") + return self + + +class BackendRoutingPolicy(HashBoundCanonicalModel): + """A versioned routing declaration without executable selection hooks.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/backend-routing-policy/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "backend_routing_policy_sha256" + + routing_policy_ref: DefinitionRef + capability_filter_definition_ref: DefinitionRef + deterministic_order_definition_ref: DefinitionRef + portfolio_composition_definition_ref: DefinitionRef + stop_condition_definition_ref: DefinitionRef + resource_partition_definition_ref: DefinitionRef + backend_routing_policy_sha256: Sha256Digest + + +class CounterfactualSolverConfig(HashBoundCanonicalModel): + """The frozen compilation/proposal configuration consumed by a backend.""" + + HASH_DOMAIN: ClassVar[str] = "spatialcf/counterfactual/solver-config/3.0" + SELF_DIGEST_FIELD: ClassVar[str] = "solver_config_sha256" + + solver_config_ref: DefinitionRef + compilation_policy_ref: DefinitionRef + proposal_policy_ref: DefinitionRef + objective_bound_policy_ref: DefinitionRef + determinism_policy_ref: DefinitionRef + solver_config_sha256: Sha256Digest + + +class ImplementationOwnerBinding(CanonicalModel): + """One committed definition/capability-to-static-owner mapping.""" + + definition_or_capability_ref: DefinitionOrCapabilityRef + implementation_owner_ref: OwnerRef + + +class ImplementationRegistrySnapshot(HashBoundCanonicalModel): + """A closed operational owner/build snapshot independent of ambient installs.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/implementation-registry-snapshot/3.0" + ) + SELF_DIGEST_FIELD: ClassVar[str] = "implementation_registry_snapshot_sha256" + + definition_and_capability_owner_bindings: tuple[ImplementationOwnerBinding, ...] + implementation_build_hashes: tuple[tuple[OwnerRef, Sha256Digest], ...] + dependency_lock_sha256: Sha256Digest + implementation_registry_snapshot_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_snapshot_closure(self) -> Self: + bindings = self.definition_and_capability_owner_bindings + _require_sorted_unique_by_bytes( + bindings, + "definition and capability owner bindings", + nonempty=True, + ) + binding_refs = tuple( + binding.definition_or_capability_ref for binding in bindings + ) + if len(set(binding_refs)) != len(binding_refs): + raise ValueError( + "same definition or capability may not bind different owners" + ) + + owner_builds = self.implementation_build_hashes + encoded_builds = tuple(canonical_json_bytes(build) for build in owner_builds) + if encoded_builds != tuple(sorted(encoded_builds)): + raise ValueError("implementation owner builds must be sorted") + if len(set(encoded_builds)) != len(encoded_builds): + raise ValueError("duplicate owner-build entry") + if len({owner for owner, _build_hash in owner_builds}) != len(owner_builds): + raise ValueError("duplicate implementation owner build") + build_owners = {owner for owner, _build_hash in owner_builds} + binding_owners = {binding.implementation_owner_ref for binding in bindings} + if build_owners != binding_owners: + raise ValueError("owner bindings and exact owner builds must close") + return self + + +class SolverBackendDescriptor(HashBoundCanonicalModel): + """One available backend's complete, hash-bound capability declaration.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/solver-backend-descriptor/3.0" + ) + SELF_DIGEST_FIELD: ClassVar[str] = "backend_descriptor_sha256" + + backend_ref: BackendRef + implementation_build_sha256: Sha256Digest + supported_profile_hashes: tuple[Sha256Digest, ...] + supported_predicate_capabilities: tuple[CapabilityRef, ...] + supported_operator_capabilities: tuple[CapabilityRef, ...] + supported_objective_capabilities: tuple[CapabilityRef, ...] + supported_numeric_semantics: tuple[DefinitionRef, ...] + emitted_proof_material_definition_refs: tuple[DefinitionRef, ...] + compatible_checker_capability_refs: tuple[CapabilityRef, ...] + resource_definition_refs: tuple[DefinitionRef, ...] + backend_descriptor_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_capability_closure(self) -> Self: + _require_sorted_unique_by_bytes( + self.supported_profile_hashes, + "supported profile hashes", + nonempty=True, + ) + _require_sorted_unique_by_bytes( + self.supported_predicate_capabilities, + "supported predicate capabilities", + ) + _require_sorted_unique_by_bytes( + self.supported_operator_capabilities, + "supported operator capabilities", + ) + _require_sorted_unique_by_bytes( + self.supported_objective_capabilities, + "supported objective capabilities", + ) + _require_sorted_unique_by_bytes( + self.supported_numeric_semantics, + "supported numeric semantics", + ) + _require_sorted_unique_by_bytes( + self.emitted_proof_material_definition_refs, + "emitted proof material definitions", + ) + _require_sorted_unique_by_bytes( + self.compatible_checker_capability_refs, + "compatible checker capabilities", + ) + _require_sorted_unique_by_bytes( + self.resource_definition_refs, + "resource definitions", + ) + return self + + +class UnavailableBackendRecord(CanonicalModel): + """One explicitly considered but unavailable optional backend.""" + + backend_ref: BackendRef + reason_claim_definition_ref: DefinitionRef + + +class BackendDescriptorBundle(HashBoundCanonicalModel): + """The full canonical backend universe for a single solve request.""" + + HASH_DOMAIN: ClassVar[str] = ( + "spatialcf/counterfactual/backend-descriptor-bundle/3.0" + ) + SELF_DIGEST_FIELD: ClassVar[str] = "backend_descriptor_bundle_sha256" + + backend_descriptors: tuple[SolverBackendDescriptor, ...] + unavailable_optional_backends: tuple[UnavailableBackendRecord, ...] + backend_descriptor_bundle_sha256: Sha256Digest + + @model_validator(mode="after") + def _validate_complete_backend_universe(self) -> Self: + _require_sorted_unique_by_bytes( + self.backend_descriptors, + "available backend descriptors", + nonempty=True, + ) + _require_sorted_unique_by_bytes( + self.unavailable_optional_backends, + "unavailable backend records", + ) + available_refs = tuple( + descriptor.backend_ref for descriptor in self.backend_descriptors + ) + unavailable_refs = tuple( + record.backend_ref for record in self.unavailable_optional_backends + ) + if len(set(available_refs)) != len(available_refs): + raise ValueError("duplicate backend descriptor") + if len(set(unavailable_refs)) != len(unavailable_refs): + raise ValueError("duplicate unavailable backend") + if set(available_refs) & set(unavailable_refs): + raise ValueError("backend cannot be both available and unavailable") + return self diff --git a/src/spatialcf/generation/planning/problem.py b/src/spatialcf/generation/planning/problem.py index 76b9c9b..9c3e424 100644 --- a/src/spatialcf/generation/planning/problem.py +++ b/src/spatialcf/generation/planning/problem.py @@ -1338,7 +1338,11 @@ def _runtime_collision_delegation_candidates( support_id = subject.support_object_id result = set() for native_id, obstacle in prepared.collision_proxies: - if native_id in {subject.object_id, support_id}: + if native_id in { + subject.object_id, + support_id, + prepared.intervention.reference_id, + }: continue if _conservative_source_overlap(subject.obb, obstacle): result.add(native_id)