diff --git a/docs/SCHEMA_INDEX.md b/docs/SCHEMA_INDEX.md index 0fb7c80..090d9ad 100644 --- a/docs/SCHEMA_INDEX.md +++ b/docs/SCHEMA_INDEX.md @@ -20,7 +20,10 @@ JSON schemas for OVK objects. See also [ARTIFACTS.md](ARTIFACTS.md). | [artifact.manifest.schema.json](../schemas/artifact.manifest.schema.json) | ovk.artifact_manifest.v1 | `ovk-artifact-manifest.json`; validated by `ovk validate-outputs` | | [verification.intent.schema.json](../schemas/verification.intent.schema.json) | n/a | `templates/**/*.intent.json` | | [verification.capability.schema.json](../schemas/verification.capability.schema.json) | n/a | `adapters/*/capability.json` | -| [verification.obligation.schema.json](../schemas/verification.obligation.schema.json) | n/a | obligation payloads | +| [verification.obligation.schema.json](../schemas/verification.obligation.schema.json) | ovk.obligation.v1 | typed backend-neutral obligations (`ovk.core.execution_models`) | +| [backend.routing.schema.json](../schemas/backend.routing.schema.json) | ovk.routing.v1 | typed routing decisions | +| [backend.execution.schema.json](../schemas/backend.execution.schema.json) | n/a | backend obligations, attempts, normalized results, execution records | +| [abstraction.coverage.schema.json](../schemas/abstraction.coverage.schema.json) | n/a | abstraction coverage reports | | [verification.result.schema.json](../schemas/verification.result.schema.json) | n/a | backend result payloads | | [self_protection.input.schema.json](../schemas/self_protection.input.schema.json) | n/a | `examples/no_agent_self_approval/` metadata and canonical inputs | | [infrastructure.input.schema.json](../schemas/infrastructure.input.schema.json) | ovk.infrastructure.input.v1 | `examples/infrastructure_exposure/` | diff --git a/ovk/core/execution_models.py b/ovk/core/execution_models.py new file mode 100644 index 0000000..5170bf4 --- /dev/null +++ b/ovk/core/execution_models.py @@ -0,0 +1,585 @@ +"""Typed execution-plane models for the solver-agnostic control plane. + +These models are the serialization and digest foundation for obligations, routing, +backend execution, and coverage. They intentionally do not change runtime behavior; +later PRs wire them into the registry, router, and control plane. + +Invariants +---------- +* ``obligation_id`` is a content digest of all semantically relevant obligation + fields except ``obligation_id`` itself. +* ``routing_id`` digests routing components including router version and budget. +* Material ``uri`` values are repository-relative or use a documented scheme; + arbitrary absolute local paths are rejected. +* Digests use the same canonical JSON hashing as ``ovk.core.bundle.content_digest``. +""" + +from __future__ import annotations + +import re +from typing import Any, Literal + +from pydantic import BaseModel, Field, field_validator + +from ovk.core.bundle import content_digest +from ovk.core.models import ( + MergeRecommendation, + RiskSeverity, + SourceRange, + VerificationStatus, + VerificationSubject, +) + +# Documented material URI schemes. Bare repository-relative paths are also allowed. +ALLOWED_MATERIAL_URI_SCHEMES: frozenset[str] = frozenset( + { + "repo", + "ovk-material", + "https", + "http", + "git", + } +) + +MaterialKind = Literal[ + "diff", + "source_file", + "workflow", + "terraform_plan", + "kubernetes_object", + "policy", + "branch_protection", + "deployment_policy", + "generated_harness", + "explicit_harness", +] + +CoverageStatus = Literal["complete", "partial", "unknown", "inapplicable"] +SupportLevel = Literal["supported", "partial", "unsupported", "unavailable"] +TerminationKind = Literal[ + "completed", + "timeout", + "resource_exhausted", + "tool_unavailable", + "tool_error", + "invalid_output", + "cancelled", +] +FallbackOutcome = Literal["unknown", "error", "fail", "fallback"] +TimeoutBehavior = Literal["unknown", "error", "fail"] + +_WINDOWS_DRIVE_RE = re.compile(r"^[A-Za-z]:[\\/]") +_URI_SCHEME_RE = re.compile(r"^([A-Za-z][A-Za-z0-9+.-]*):") + + +def is_absolute_local_path(uri: str) -> bool: + """Return True when *uri* looks like an absolute local filesystem path.""" + value = uri.strip() + if not value: + return False + if value.startswith("\\\\") or value.startswith("//"): + # UNC paths (\\server\share) or protocol-relative //host — treat as absolute local/network paths. + if value.startswith("//") and not value.lower().startswith(("//repo",)): + # protocol-relative URLs are not repo-relative materials + return True + return value.startswith("\\\\") + if _WINDOWS_DRIVE_RE.match(value): + return True + if value.startswith("file:"): + return True + # POSIX absolute path without a documented scheme + if value.startswith("/") and not _URI_SCHEME_RE.match(value): + return True + return False + + +def validate_material_uri(uri: str) -> str: + """Validate a material URI; reject empty values and absolute local paths. + + Allowed forms: + * repository-relative paths (``src/foo.py``, ``.github/workflows/ci.yml``) + * documented schemes in ``ALLOWED_MATERIAL_URI_SCHEMES`` (``repo:...``, ``ovk-material:...``, ...) + """ + value = uri.strip() + if not value: + raise ValueError("material uri must be non-empty") + if is_absolute_local_path(value): + raise ValueError( + "material uri must not be an arbitrary absolute local path; " + "use a repository-relative path or a documented material scheme" + ) + scheme_match = _URI_SCHEME_RE.match(value) + if scheme_match is not None: + scheme = scheme_match.group(1).lower() + # Windows drive letters are already rejected above; remaining schemes must be allowlisted. + if len(scheme) == 1 and scheme.isalpha(): + raise ValueError("material uri must not use a filesystem drive letter") + if scheme not in ALLOWED_MATERIAL_URI_SCHEMES: + raise ValueError( + f"material uri scheme {scheme!r} is not allowed; " + f"permitted schemes: {sorted(ALLOWED_MATERIAL_URI_SCHEMES)}" + ) + return value + + +def _dump_json(value: BaseModel | dict[str, Any] | list[Any] | Any) -> Any: + if isinstance(value, BaseModel): + return value.model_dump(mode="json") + return value + + +def _sorted_str_list(values: list[str]) -> list[str]: + return sorted(values) + + +def _sorted_by_key(items: list[Any], key: str) -> list[Any]: + dumped = [_dump_json(item) for item in items] + return sorted(dumped, key=lambda item: str(item.get(key, ""))) + + +# --------------------------------------------------------------------------- +# Supporting identity / capability / environment types +# --------------------------------------------------------------------------- + + +class CompilerIdentity(BaseModel): + """Compiler that produced an obligation or abstraction.""" + + compiler_id: str + compiler_version: str + + +class BackendToolIdentity(BaseModel): + """Tool and adapter identity inside a capability manifest.""" + + name: str + adapter: str + adapter_version: str + version: str | None = None + + +class BackendGuaranteeDeclaration(BaseModel): + """Guarantee semantics advertised by a backend.""" + + type: str + meaning_of_pass: str + meaning_of_fail: str + meaning_of_unknown: str + + +class BackendCapabilityManifest(BaseModel): + """Typed capability declaration for a registered backend.""" + + capability_id: str + tool: BackendToolIdentity + backend_class: str + guarantee: BackendGuaranteeDeclaration + input_languages: list[str] = Field(default_factory=list) + supported_domains: list[str] = Field(default_factory=list) + supported_property_kinds: list[str] = Field(default_factory=list) + assumptions: list[str] = Field(default_factory=list) + limits: list[str] = Field(default_factory=list) + result_format: str | None = None + counterexample_format: str | None = None + timeout_behavior: TimeoutBehavior = "unknown" + + +class BackendEnvironmentFingerprint(BaseModel): + """Environment fingerprint recorded before or after backend execution.""" + + backend: str + adapter_version: str + environment_digest: str + tool_version: str | None = None + tool_digest: str | None = None + worker_image_digest: str | None = None + native_available: bool = False + + +class ExecutionBudget(BaseModel): + """Runtime and isolation budget for obligation execution.""" + + total_wall_time_seconds: float + per_backend_wall_time_seconds: float + max_memory_mb: int + max_parallel_backends: int + allow_network: bool + allow_repository_write: bool + allowed_backends: list[str] | None = None + denied_backends: list[str] = Field(default_factory=list) + + +class FallbackPolicy(BaseModel): + """Policy controlling whether and how backends may fall back.""" + + allow_fallback: bool = False + fallback_backends: list[str] = Field(default_factory=list) + on_timeout: FallbackOutcome = "unknown" + on_tool_unavailable: FallbackOutcome = "unknown" + on_invalid_output: FallbackOutcome = "unknown" + + +class BackendCapabilityAssessment(BaseModel): + """Assessment of whether a backend can handle an obligation.""" + + backend: str + support: SupportLevel + score: float + guarantee_type: str + material_requirements_met: bool + coverage_requirements_met: bool + native_available: bool + estimated_wall_time_seconds: float + estimated_memory_mb: int + reasons: list[str] = Field(default_factory=list) + + +class BackendCandidate(BaseModel): + """Eligible backend considered during routing.""" + + backend: str + score: float + support: SupportLevel + guarantee_type: str + reasons: list[str] = Field(default_factory=list) + native_available: bool = False + + +class BackendSelection(BaseModel): + """Backend selected for execution.""" + + backend: str + reason: str + expected_guarantee: str + required: bool = True + score: float = 0.0 + + +class BackendRejection(BaseModel): + """Backend considered and rejected during routing.""" + + backend: str + reason: str + support: SupportLevel | None = None + + +class HumanExplanation(BaseModel): + """Human-readable explanation of a normalized backend result.""" + + summary: str + repair_hint: str + failure_mode: str | None = None + + +class ExecutionContext(BaseModel): + """Repository and policy context supplied to adapters and the registry.""" + + subject: VerificationSubject + actor_type: str = "unknown" + changed_files: list[str] = Field(default_factory=list) + policy_digest: str | None = None + budget: ExecutionBudget | None = None + surfaces: list[dict[str, Any]] = Field(default_factory=list) + metadata: dict[str, Any] = Field(default_factory=dict) + + +# --------------------------------------------------------------------------- +# Core execution-plane models +# --------------------------------------------------------------------------- + + +class MaterialReference(BaseModel): + """Content-addressed reference to an input material.""" + + material_id: str + kind: MaterialKind + uri: str + sha256: str + size_bytes: int + source_revision: str | None = None + source_range: SourceRange | None = None + trusted: bool = False + + @field_validator("uri") + @classmethod + def _check_uri(cls, value: str) -> str: + return validate_material_uri(value) + + +class AbstractionCoverage(BaseModel): + """How completely a compiler abstracted the subject materials.""" + + status: CoverageStatus + confidence: float + extracted_elements: int + expected_elements: int | None = None + unsupported_constructs: list[str] = Field(default_factory=list) + warnings: list[str] = Field(default_factory=list) + source_ranges: list[SourceRange] = Field(default_factory=list) + + +class VerificationObligation(BaseModel): + """Backend-neutral verification obligation (schema ``ovk.obligation.v1``).""" + + obligation_id: str + schema_version: Literal["ovk.obligation.v1"] = "ovk.obligation.v1" + subject: VerificationSubject + intent_id: str + intent_version: str + lane: str + property_kind: str + severity: RiskSeverity + compiler_id: str + compiler_version: str + materials: list[MaterialReference] + abstraction: dict[str, Any] + abstraction_digest: str + coverage: AbstractionCoverage + acceptable_guarantees: list[str] + required_capabilities: list[str] + policy_digest: str + + +class RoutingDecision(BaseModel): + """Typed routing decision for one obligation (schema ``ovk.routing.v1``).""" + + routing_id: str + schema_version: Literal["ovk.routing.v1"] = "ovk.routing.v1" + obligation_id: str + requested: list[str] + eligible: list[BackendCandidate] + selected: list[BackendSelection] + rejected: list[BackendRejection] + aggregation_policy: str + fallback_policy: FallbackPolicy + budget: ExecutionBudget + policy_digest: str + + +class BackendObligation(BaseModel): + """Backend-specific compiled obligation ready for execution.""" + + backend_obligation_id: str + obligation_id: str + routing_id: str + backend: str + adapter_version: str + compiler_version: str + input_language: str + payload: dict[str, Any] + payload_digest: str + command_plan: list[str] = Field(default_factory=list) + environment_requirements: dict[str, Any] = Field(default_factory=dict) + expected_guarantee: str + + +class RawBackendExecution(BaseModel): + """Raw backend execution artifact before normalization.""" + + backend: str + backend_obligation_id: str + termination: TerminationKind + native_execution: bool + exit_code: int | None = None + stdout: str | None = None + stderr: str | None = None + raw_result: dict[str, Any] = Field(default_factory=dict) + stdout_digest: str | None = None + stderr_digest: str | None = None + raw_result_digest: str | None = None + started_at: str | None = None + finished_at: str | None = None + duration_ms: float | None = None + tool_version: str | None = None + tool_digest: str | None = None + worker_image_digest: str | None = None + + +class ExecutionAttempt(BaseModel): + """One recorded attempt to execute a backend obligation.""" + + attempt_id: str + backend_obligation_id: str + backend: str + required: bool + started_at: str + finished_at: str + duration_ms: float + termination: TerminationKind + native_execution: bool + tool_version: str | None = None + tool_digest: str | None = None + worker_image_digest: str | None = None + exit_code: int | None = None + stdout_digest: str | None = None + stderr_digest: str | None = None + raw_result_digest: str | None = None + + +class NormalizedBackendResult(BaseModel): + """Normalized result produced from a raw backend execution.""" + + attempt_id: str + backend: str + status: VerificationStatus + guarantee_type: str + assumptions: list[str] = Field(default_factory=list) + limits: list[str] = Field(default_factory=list) + counterexamples: list[dict[str, Any]] = Field(default_factory=list) + generated_artifacts: list[dict[str, Any]] = Field(default_factory=list) + + +class ObligationExecutionRecord(BaseModel): + """Full typed record of compiling, routing, and executing one obligation.""" + + obligation: VerificationObligation + routing: RoutingDecision + backend_obligations: list[BackendObligation] + attempts: list[ExecutionAttempt] + results: list[NormalizedBackendResult] + aggregate_status: VerificationStatus + merge_recommendation: MergeRecommendation + aggregation_reason: str + open_obligations: list[dict[str, Any]] = Field(default_factory=list) + + +# --------------------------------------------------------------------------- +# Canonical digests +# --------------------------------------------------------------------------- + + +def compute_abstraction_digest(abstraction: dict[str, Any]) -> str: + """Return the content digest of a property abstraction.""" + return content_digest(abstraction) + + +def compute_payload_digest(payload: dict[str, Any]) -> str: + """Return the content digest of a backend obligation payload.""" + return content_digest(payload) + + +def obligation_digest_input( + obligation: VerificationObligation | dict[str, Any], +) -> dict[str, Any]: + """Return the canonical digest payload for an obligation (excludes ``obligation_id``).""" + data = dict(_dump_json(obligation)) + data.pop("obligation_id", None) + data["acceptable_guarantees"] = _sorted_str_list(list(data.get("acceptable_guarantees") or [])) + data["required_capabilities"] = _sorted_str_list(list(data.get("required_capabilities") or [])) + materials = list(data.get("materials") or []) + data["materials"] = sorted(materials, key=lambda item: str(item.get("material_id", ""))) + return data + + +def compute_obligation_id(obligation: VerificationObligation | dict[str, Any]) -> str: + """Compute ``obligation_id`` from all semantically relevant fields except itself.""" + return content_digest(obligation_digest_input(obligation)) + + +def routing_digest_input( + *, + obligation_id: str, + requested: list[str], + eligible: list[BackendCandidate] | list[dict[str, Any]], + selected: list[BackendSelection] | list[dict[str, Any]], + rejected: list[BackendRejection] | list[dict[str, Any]], + aggregation_policy: str, + fallback_policy: FallbackPolicy | dict[str, Any], + budget: ExecutionBudget | dict[str, Any], + policy_digest: str, + router_version: str, + assessments: list[BackendCapabilityAssessment] | list[dict[str, Any]] | None = None, +) -> dict[str, Any]: + """Return the canonical digest payload used to derive ``routing_id``.""" + payload: dict[str, Any] = { + "obligation_id": obligation_id, + "requested": _sorted_str_list(list(requested)), + "eligible": _sorted_by_key(list(eligible), "backend"), + "selected": _sorted_by_key(list(selected), "backend"), + "rejected": _sorted_by_key(list(rejected), "backend"), + "aggregation_policy": aggregation_policy, + "fallback_policy": _dump_json(fallback_policy), + "budget": _dump_json(budget), + "policy_digest": policy_digest, + "router_version": router_version, + } + if assessments is not None: + payload["assessments"] = _sorted_by_key(list(assessments), "backend") + return payload + + +def compute_routing_id( + *, + obligation_id: str, + requested: list[str], + eligible: list[BackendCandidate] | list[dict[str, Any]], + selected: list[BackendSelection] | list[dict[str, Any]], + rejected: list[BackendRejection] | list[dict[str, Any]], + aggregation_policy: str, + fallback_policy: FallbackPolicy | dict[str, Any], + budget: ExecutionBudget | dict[str, Any], + policy_digest: str, + router_version: str, + assessments: list[BackendCapabilityAssessment] | list[dict[str, Any]] | None = None, +) -> str: + """Compute ``routing_id`` from routing components and router version.""" + return content_digest( + routing_digest_input( + obligation_id=obligation_id, + requested=requested, + eligible=eligible, + selected=selected, + rejected=rejected, + aggregation_policy=aggregation_policy, + fallback_policy=fallback_policy, + budget=budget, + policy_digest=policy_digest, + router_version=router_version, + assessments=assessments, + ) + ) + + +def backend_obligation_digest_input( + backend_obligation: BackendObligation | dict[str, Any], +) -> dict[str, Any]: + """Canonical digest payload for a backend obligation (excludes its id).""" + data = dict(_dump_json(backend_obligation)) + data.pop("backend_obligation_id", None) + return data + + +def compute_backend_obligation_id( + backend_obligation: BackendObligation | dict[str, Any], +) -> str: + """Compute ``backend_obligation_id`` from semantically relevant fields except itself.""" + return content_digest(backend_obligation_digest_input(backend_obligation)) + + +def attempt_digest_input(attempt: ExecutionAttempt | dict[str, Any]) -> dict[str, Any]: + """Canonical digest payload for an execution attempt (excludes ``attempt_id`` and wall-clock times). + + Timestamps are excluded so identical executions remain content-addressable when + wall-clock values differ; ``duration_ms`` and termination/output digests remain. + """ + data = dict(_dump_json(attempt)) + data.pop("attempt_id", None) + data.pop("started_at", None) + data.pop("finished_at", None) + return data + + +def compute_attempt_id(attempt: ExecutionAttempt | dict[str, Any]) -> str: + """Compute ``attempt_id`` from stable attempt fields.""" + return content_digest(attempt_digest_input(attempt)) + + +def compute_raw_execution_digests(raw: RawBackendExecution) -> dict[str, str]: + """Compute stdout/stderr/raw_result digests for a raw execution.""" + digests: dict[str, str] = {} + if raw.stdout is not None: + digests["stdout_digest"] = content_digest(raw.stdout) + if raw.stderr is not None: + digests["stderr_digest"] = content_digest(raw.stderr) + digests["raw_result_digest"] = content_digest(raw.raw_result) + return digests diff --git a/ovk/core/models.py b/ovk/core/models.py index 4fdcfd7..3d5df29 100644 --- a/ovk/core/models.py +++ b/ovk/core/models.py @@ -35,6 +35,25 @@ class RiskSeverity(str, Enum): CRITICAL = "critical" +class SourceRange(BaseModel): + """Byte- or line-oriented span within a repository path.""" + + path: str + start_line: int | None = None + end_line: int | None = None + start_column: int | None = None + end_column: int | None = None + + +class VerificationSubject(BaseModel): + """Repository revision under verification (matches evidence subject shape).""" + + repo: str + head_sha: str + pull_request: int | str | None = None + base_sha: str | None = None + + class VerificationIntent(BaseModel): intent_id: str version: str = "0.1.0" diff --git a/schemas/abstraction.coverage.schema.json b/schemas/abstraction.coverage.schema.json new file mode 100644 index 0000000..368edd8 --- /dev/null +++ b/schemas/abstraction.coverage.schema.json @@ -0,0 +1,43 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://openverification.dev/schemas/abstraction.coverage.schema.json", + "title": "Abstraction Coverage", + "type": "object", + "required": ["status", "confidence", "extracted_elements"], + "properties": { + "status": { + "type": "string", + "enum": ["complete", "partial", "unknown", "inapplicable"] + }, + "confidence": { "type": "number", "minimum": 0, "maximum": 1 }, + "extracted_elements": { "type": "integer", "minimum": 0 }, + "expected_elements": { "type": ["integer", "null"], "minimum": 0 }, + "unsupported_constructs": { + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "warnings": { + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "source_ranges": { + "type": "array", + "items": { + "type": "object", + "required": ["path"], + "properties": { + "path": { "type": "string", "minLength": 1 }, + "start_line": { "type": ["integer", "null"], "minimum": 1 }, + "end_line": { "type": ["integer", "null"], "minimum": 1 }, + "start_column": { "type": ["integer", "null"], "minimum": 0 }, + "end_column": { "type": ["integer", "null"], "minimum": 0 } + }, + "additionalProperties": true + }, + "default": [] + } + }, + "additionalProperties": true +} diff --git a/schemas/backend.execution.schema.json b/schemas/backend.execution.schema.json new file mode 100644 index 0000000..a6d59a3 --- /dev/null +++ b/schemas/backend.execution.schema.json @@ -0,0 +1,196 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://openverification.dev/schemas/backend.execution.schema.json", + "title": "Backend Execution Artifacts", + "description": "Schemas for backend obligations, execution attempts, normalized results, and aggregate execution records.", + "type": "object", + "oneOf": [ + { "$ref": "#/$defs/backend_obligation" }, + { "$ref": "#/$defs/execution_attempt" }, + { "$ref": "#/$defs/normalized_backend_result" }, + { "$ref": "#/$defs/obligation_execution_record" } + ], + "$defs": { + "backend_obligation": { + "type": "object", + "required": [ + "backend_obligation_id", + "obligation_id", + "routing_id", + "backend", + "adapter_version", + "compiler_version", + "input_language", + "payload", + "payload_digest", + "expected_guarantee" + ], + "properties": { + "backend_obligation_id": { "type": "string", "minLength": 1 }, + "obligation_id": { "type": "string", "minLength": 1 }, + "routing_id": { "type": "string", "minLength": 1 }, + "backend": { "type": "string", "minLength": 1 }, + "adapter_version": { "type": "string", "minLength": 1 }, + "compiler_version": { "type": "string", "minLength": 1 }, + "input_language": { "type": "string", "minLength": 1 }, + "payload": { "type": "object", "additionalProperties": true }, + "payload_digest": { "type": "string", "minLength": 1 }, + "command_plan": { + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "environment_requirements": { + "type": "object", + "additionalProperties": true, + "default": {} + }, + "expected_guarantee": { "type": "string", "minLength": 1 } + }, + "additionalProperties": true + }, + "execution_attempt": { + "type": "object", + "required": [ + "attempt_id", + "backend_obligation_id", + "backend", + "required", + "started_at", + "finished_at", + "duration_ms", + "termination", + "native_execution" + ], + "properties": { + "attempt_id": { "type": "string", "minLength": 1 }, + "backend_obligation_id": { "type": "string", "minLength": 1 }, + "backend": { "type": "string", "minLength": 1 }, + "required": { "type": "boolean" }, + "started_at": { "type": "string", "minLength": 1 }, + "finished_at": { "type": "string", "minLength": 1 }, + "duration_ms": { "type": "number", "minimum": 0 }, + "termination": { + "type": "string", + "enum": [ + "completed", + "timeout", + "resource_exhausted", + "tool_unavailable", + "tool_error", + "invalid_output", + "cancelled" + ] + }, + "native_execution": { "type": "boolean" }, + "tool_version": { "type": ["string", "null"] }, + "tool_digest": { "type": ["string", "null"] }, + "worker_image_digest": { "type": ["string", "null"] }, + "exit_code": { "type": ["integer", "null"] }, + "stdout_digest": { "type": ["string", "null"] }, + "stderr_digest": { "type": ["string", "null"] }, + "raw_result_digest": { "type": ["string", "null"] } + }, + "additionalProperties": true + }, + "normalized_backend_result": { + "type": "object", + "required": [ + "attempt_id", + "backend", + "status", + "guarantee_type", + "assumptions", + "limits", + "counterexamples", + "generated_artifacts" + ], + "properties": { + "attempt_id": { "type": "string", "minLength": 1 }, + "backend": { "type": "string", "minLength": 1 }, + "status": { + "type": "string", + "enum": ["pass", "fail", "unknown", "error", "skipped"] + }, + "guarantee_type": { "type": "string", "minLength": 1 }, + "assumptions": { + "type": "array", + "items": { "type": "string" } + }, + "limits": { + "type": "array", + "items": { "type": "string" } + }, + "counterexamples": { + "type": "array", + "items": { "type": "object", "additionalProperties": true } + }, + "generated_artifacts": { + "type": "array", + "items": { "type": "object", "additionalProperties": true } + } + }, + "additionalProperties": true + }, + "obligation_execution_record": { + "type": "object", + "required": [ + "obligation", + "routing", + "backend_obligations", + "attempts", + "results", + "aggregate_status", + "merge_recommendation", + "aggregation_reason", + "open_obligations" + ], + "properties": { + "obligation": { + "$ref": "https://openverification.dev/schemas/verification.obligation.schema.json" + }, + "routing": { + "$ref": "https://openverification.dev/schemas/backend.routing.schema.json" + }, + "backend_obligations": { + "type": "array", + "items": { + "$ref": "https://openverification.dev/schemas/backend.execution.schema.json#/$defs/backend_obligation" + } + }, + "attempts": { + "type": "array", + "items": { + "$ref": "https://openverification.dev/schemas/backend.execution.schema.json#/$defs/execution_attempt" + } + }, + "results": { + "type": "array", + "items": { + "$ref": "https://openverification.dev/schemas/backend.execution.schema.json#/$defs/normalized_backend_result" + } + }, + "aggregate_status": { + "type": "string", + "enum": ["pass", "fail", "unknown", "error", "skipped"] + }, + "merge_recommendation": { + "type": "string", + "enum": [ + "allow", + "block", + "require_human_review", + "allow_with_warning", + "require_stronger_check" + ] + }, + "aggregation_reason": { "type": "string" }, + "open_obligations": { + "type": "array", + "items": { "type": "object", "additionalProperties": true } + } + }, + "additionalProperties": true + } + } +} diff --git a/schemas/backend.routing.schema.json b/schemas/backend.routing.schema.json new file mode 100644 index 0000000..f88cd34 --- /dev/null +++ b/schemas/backend.routing.schema.json @@ -0,0 +1,147 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://openverification.dev/schemas/backend.routing.schema.json", + "title": "Backend Routing Decision", + "type": "object", + "required": [ + "routing_id", + "schema_version", + "obligation_id", + "requested", + "eligible", + "selected", + "rejected", + "aggregation_policy", + "fallback_policy", + "budget", + "policy_digest" + ], + "properties": { + "routing_id": { "type": "string", "minLength": 1 }, + "schema_version": { "type": "string", "const": "ovk.routing.v1" }, + "obligation_id": { "type": "string", "minLength": 1 }, + "requested": { + "type": "array", + "items": { "type": "string" } + }, + "eligible": { + "type": "array", + "items": { + "type": "object", + "required": ["backend", "score", "support", "guarantee_type"], + "properties": { + "backend": { "type": "string", "minLength": 1 }, + "score": { "type": "number" }, + "support": { + "type": "string", + "enum": ["supported", "partial", "unsupported", "unavailable"] + }, + "guarantee_type": { "type": "string", "minLength": 1 }, + "reasons": { + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "native_available": { "type": "boolean", "default": false } + }, + "additionalProperties": true + } + }, + "selected": { + "type": "array", + "items": { + "type": "object", + "required": ["backend", "reason", "expected_guarantee"], + "properties": { + "backend": { "type": "string", "minLength": 1 }, + "reason": { "type": "string" }, + "expected_guarantee": { "type": "string" }, + "required": { "type": "boolean", "default": true }, + "score": { "type": "number", "default": 0 } + }, + "additionalProperties": true + } + }, + "rejected": { + "type": "array", + "items": { + "type": "object", + "required": ["backend", "reason"], + "properties": { + "backend": { "type": "string", "minLength": 1 }, + "reason": { "type": "string" }, + "support": { + "anyOf": [ + { + "type": "string", + "enum": ["supported", "partial", "unsupported", "unavailable"] + }, + { "type": "null" } + ] + } + }, + "additionalProperties": true + } + }, + "aggregation_policy": { "type": "string", "minLength": 1 }, + "fallback_policy": { + "type": "object", + "required": ["allow_fallback"], + "properties": { + "allow_fallback": { "type": "boolean" }, + "fallback_backends": { + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "on_timeout": { + "type": "string", + "enum": ["unknown", "error", "fail", "fallback"], + "default": "unknown" + }, + "on_tool_unavailable": { + "type": "string", + "enum": ["unknown", "error", "fail", "fallback"], + "default": "unknown" + }, + "on_invalid_output": { + "type": "string", + "enum": ["unknown", "error", "fail", "fallback"], + "default": "unknown" + } + }, + "additionalProperties": true + }, + "budget": { + "type": "object", + "required": [ + "total_wall_time_seconds", + "per_backend_wall_time_seconds", + "max_memory_mb", + "max_parallel_backends", + "allow_network", + "allow_repository_write" + ], + "properties": { + "total_wall_time_seconds": { "type": "number", "minimum": 0 }, + "per_backend_wall_time_seconds": { "type": "number", "minimum": 0 }, + "max_memory_mb": { "type": "integer", "minimum": 1 }, + "max_parallel_backends": { "type": "integer", "minimum": 1 }, + "allow_network": { "type": "boolean" }, + "allow_repository_write": { "type": "boolean" }, + "allowed_backends": { + "type": ["array", "null"], + "items": { "type": "string" } + }, + "denied_backends": { + "type": "array", + "items": { "type": "string" }, + "default": [] + } + }, + "additionalProperties": true + }, + "policy_digest": { "type": "string", "minLength": 1 } + }, + "additionalProperties": true +} diff --git a/schemas/verification.obligation.schema.json b/schemas/verification.obligation.schema.json index d0f4cc5..c600f2c 100644 --- a/schemas/verification.obligation.schema.json +++ b/schemas/verification.obligation.schema.json @@ -3,29 +3,106 @@ "$id": "https://openverification.dev/schemas/verification.obligation.schema.json", "title": "Verification Obligation", "type": "object", - "required": ["obligation_id", "intent_id", "backend"], + "required": [ + "obligation_id", + "schema_version", + "subject", + "intent_id", + "intent_version", + "lane", + "property_kind", + "severity", + "compiler_id", + "compiler_version", + "materials", + "abstraction", + "abstraction_digest", + "coverage", + "acceptable_guarantees", + "required_capabilities", + "policy_digest" + ], "properties": { - "obligation_id": { "type": "string" }, - "intent_id": { "type": "string" }, - "backend": { "type": "string" }, - "query_polarity": { - "type": "string", - "enum": ["find_counterexample", "prove_property", "evaluate_policy", "check_model", "custom"] - }, - "input": { "type": "object", "additionalProperties": true }, - "policy": { "type": "string" }, - "query": { "type": "string" }, - "constraints": { "type": "array", "items": { "type": "string" } }, - "model": { "type": "object", "additionalProperties": true }, - "assumptions": { "type": "array", "items": { "type": "string" } }, - "budget": { + "obligation_id": { "type": "string", "minLength": 1 }, + "schema_version": { "type": "string", "const": "ovk.obligation.v1" }, + "subject": { "type": "object", + "required": ["repo", "head_sha"], "properties": { - "timeout_seconds": { "type": "integer", "minimum": 1 }, - "max_memory_mb": { "type": "integer", "minimum": 1 } + "repo": { "type": "string", "minLength": 1 }, + "head_sha": { "type": "string", "minLength": 1 }, + "pull_request": { "type": ["integer", "string", "null"] }, + "base_sha": { "type": ["string", "null"] } }, "additionalProperties": true - } + }, + "intent_id": { "type": "string", "minLength": 1 }, + "intent_version": { "type": "string", "minLength": 1 }, + "lane": { "type": "string", "minLength": 1 }, + "property_kind": { "type": "string", "minLength": 1 }, + "severity": { + "type": "string", + "enum": ["low", "medium", "high", "critical"] + }, + "compiler_id": { "type": "string", "minLength": 1 }, + "compiler_version": { "type": "string", "minLength": 1 }, + "materials": { + "type": "array", + "items": { + "type": "object", + "required": ["material_id", "kind", "uri", "sha256", "size_bytes"], + "properties": { + "material_id": { "type": "string", "minLength": 1 }, + "kind": { + "type": "string", + "enum": [ + "diff", + "source_file", + "workflow", + "terraform_plan", + "kubernetes_object", + "policy", + "branch_protection", + "deployment_policy", + "generated_harness", + "explicit_harness" + ] + }, + "uri": { "type": "string", "minLength": 1 }, + "sha256": { "type": "string", "minLength": 64, "maxLength": 64 }, + "size_bytes": { "type": "integer", "minimum": 0 }, + "source_revision": { "type": ["string", "null"] }, + "source_range": { + "type": ["object", "null"], + "required": ["path"], + "properties": { + "path": { "type": "string", "minLength": 1 }, + "start_line": { "type": ["integer", "null"] }, + "end_line": { "type": ["integer", "null"] }, + "start_column": { "type": ["integer", "null"] }, + "end_column": { "type": ["integer", "null"] } + }, + "additionalProperties": true + }, + "trusted": { "type": "boolean", "default": false } + }, + "additionalProperties": true + } + }, + "abstraction": { "type": "object", "additionalProperties": true }, + "abstraction_digest": { "type": "string", "minLength": 1 }, + "coverage": { + "$ref": "https://openverification.dev/schemas/abstraction.coverage.schema.json" + }, + "acceptable_guarantees": { + "type": "array", + "items": { "type": "string" } + }, + "required_capabilities": { + "type": "array", + "items": { "type": "string" } + }, + "policy_digest": { "type": "string", "minLength": 1 } }, "additionalProperties": true } diff --git a/tests/test_execution_models.py b/tests/test_execution_models.py new file mode 100644 index 0000000..08e26ff --- /dev/null +++ b/tests/test_execution_models.py @@ -0,0 +1,501 @@ +"""Serialization, digest determinism, and schema tests for execution models.""" + +from __future__ import annotations + +import copy +from pathlib import Path +from typing import Any + +import pytest +from pydantic import ValidationError + +from ovk.core.bundle import content_digest +from ovk.core.execution_models import ( + AbstractionCoverage, + BackendCandidate, + BackendObligation, + BackendRejection, + BackendSelection, + ExecutionAttempt, + ExecutionBudget, + FallbackPolicy, + MaterialReference, + NormalizedBackendResult, + ObligationExecutionRecord, + RoutingDecision, + VerificationObligation, + attempt_digest_input, + compute_abstraction_digest, + compute_attempt_id, + compute_backend_obligation_id, + compute_obligation_id, + compute_payload_digest, + compute_routing_id, + is_absolute_local_path, + obligation_digest_input, + validate_material_uri, +) +from ovk.core.models import ( + MergeRecommendation, + RiskSeverity, + SourceRange, + VerificationStatus, + VerificationSubject, +) +from ovk.core.schema_validation import load_json, validate_against_schema + +SCHEMA_ROOT = Path("schemas") + + +def _subject() -> VerificationSubject: + return VerificationSubject(repo="example/repo", head_sha="abc123", base_sha="def456", pull_request=7) + + +def _coverage() -> AbstractionCoverage: + return AbstractionCoverage( + status="complete", + confidence=1.0, + extracted_elements=2, + expected_elements=2, + source_ranges=[SourceRange(path="src/auth.py", start_line=1, end_line=10)], + ) + + +def _material(*, material_id: str = "mat-1", uri: str = "src/auth.py") -> MaterialReference: + return MaterialReference( + material_id=material_id, + kind="source_file", + uri=uri, + sha256="a" * 64, + size_bytes=128, + source_revision="abc123", + source_range=SourceRange(path=uri, start_line=1, end_line=4), + trusted=True, + ) + + +def _budget() -> ExecutionBudget: + return ExecutionBudget( + total_wall_time_seconds=60.0, + per_backend_wall_time_seconds=30.0, + max_memory_mb=512, + max_parallel_backends=2, + allow_network=False, + allow_repository_write=False, + allowed_backends=["z3", "deterministic"], + denied_backends=["lean"], + ) + + +def _fallback() -> FallbackPolicy: + return FallbackPolicy(allow_fallback=False, fallback_backends=[]) + + +def _obligation(*, abstraction: dict[str, Any] | None = None) -> VerificationObligation: + abs_payload = abstraction if abstraction is not None else {"kind": "access_control", "routes": ["/admin"]} + materials = [_material(material_id="mat-b", uri="src/b.py"), _material(material_id="mat-a", uri="src/a.py")] + provisional = VerificationObligation( + obligation_id="pending", + subject=_subject(), + intent_id="no_admin_route_bypass", + intent_version="0.1.0", + lane="authorization", + property_kind="access_control", + severity=RiskSeverity.HIGH, + compiler_id="authorization-compiler", + compiler_version="0.1.0", + materials=materials, + abstraction=abs_payload, + abstraction_digest=compute_abstraction_digest(abs_payload), + coverage=_coverage(), + acceptable_guarantees=["smt_satisfiability", "deterministic_evaluation"], + required_capabilities=["smt", "json-constraints"], + policy_digest=content_digest({"mode": "advisory"}), + ) + return provisional.model_copy(update={"obligation_id": compute_obligation_id(provisional)}) + + +def _routing(obligation_id: str) -> RoutingDecision: + eligible = [ + BackendCandidate( + backend="z3", + score=0.9, + support="supported", + guarantee_type="smt_satisfiability", + reasons=["domain match"], + native_available=True, + ), + BackendCandidate( + backend="deterministic", + score=0.7, + support="supported", + guarantee_type="deterministic_evaluation", + reasons=["always available"], + ), + ] + selected = [ + BackendSelection( + backend="z3", + reason="highest score", + expected_guarantee="smt_satisfiability", + required=True, + score=0.9, + ) + ] + rejected = [ + BackendRejection(backend="lean", reason="denied by budget", support="unsupported"), + ] + budget = _budget() + fallback = _fallback() + policy_digest = content_digest({"routing": {"mode": "shadow"}}) + routing_id = compute_routing_id( + obligation_id=obligation_id, + requested=["z3", "deterministic"], + eligible=eligible, + selected=selected, + rejected=rejected, + aggregation_policy="fail_dominant", + fallback_policy=fallback, + budget=budget, + policy_digest=policy_digest, + router_version="0.1.0", + ) + return RoutingDecision( + routing_id=routing_id, + obligation_id=obligation_id, + requested=["z3", "deterministic"], + eligible=eligible, + selected=selected, + rejected=rejected, + aggregation_policy="fail_dominant", + fallback_policy=fallback, + budget=budget, + policy_digest=policy_digest, + ) + + +def _backend_obligation(obligation_id: str, routing_id: str) -> BackendObligation: + payload = {"query": "unsat", "formula": "(assert false)"} + provisional = BackendObligation( + backend_obligation_id="pending", + obligation_id=obligation_id, + routing_id=routing_id, + backend="z3", + adapter_version="0.1.0", + compiler_version="0.1.0", + input_language="smtlib2", + payload=payload, + payload_digest=compute_payload_digest(payload), + command_plan=["z3", "-T:30", "-"], + expected_guarantee="smt_satisfiability", + ) + return provisional.model_copy(update={"backend_obligation_id": compute_backend_obligation_id(provisional)}) + + +def _attempt(backend_obligation_id: str) -> ExecutionAttempt: + provisional = ExecutionAttempt( + attempt_id="pending", + backend_obligation_id=backend_obligation_id, + backend="z3", + required=True, + started_at="2026-01-01T00:00:00Z", + finished_at="2026-01-01T00:00:01Z", + duration_ms=1000.0, + termination="completed", + native_execution=True, + tool_version="4.13.0", + exit_code=0, + stdout_digest=content_digest("unsat"), + stderr_digest=content_digest(""), + raw_result_digest=content_digest({"status": "unsat"}), + ) + return provisional.model_copy(update={"attempt_id": compute_attempt_id(provisional)}) + + +def _result(attempt_id: str) -> NormalizedBackendResult: + return NormalizedBackendResult( + attempt_id=attempt_id, + backend="z3", + status=VerificationStatus.PASS, + guarantee_type="smt_satisfiability", + assumptions=["finite abstraction"], + limits=["timeout may yield unknown"], + counterexamples=[], + generated_artifacts=[], + ) + + +def _execution_record() -> ObligationExecutionRecord: + obligation = _obligation() + routing = _routing(obligation.obligation_id) + backend_obl = _backend_obligation(obligation.obligation_id, routing.routing_id) + attempt = _attempt(backend_obl.backend_obligation_id) + return ObligationExecutionRecord( + obligation=obligation, + routing=routing, + backend_obligations=[backend_obl], + attempts=[attempt], + results=[_result(attempt.attempt_id)], + aggregate_status=VerificationStatus.PASS, + merge_recommendation=MergeRecommendation.ALLOW, + aggregation_reason="single required backend passed", + open_obligations=[], + ) + + +# --------------------------------------------------------------------------- +# Round-trip serialization +# --------------------------------------------------------------------------- + + +@pytest.mark.parametrize( + "builder", + [ + _obligation, + lambda: _routing(_obligation().obligation_id), + lambda: _backend_obligation("obl", "route"), + lambda: _attempt("bo"), + lambda: _result("att"), + _execution_record, + _coverage, + _budget, + _fallback, + _material, + ], +) +def test_model_json_round_trip(builder: Any) -> None: + model = builder() + payload = model.model_dump(mode="json") + restored = type(model).model_validate(payload) + assert restored.model_dump(mode="json") == payload + + +def test_obligation_execution_record_nested_round_trip() -> None: + record = _execution_record() + restored = ObligationExecutionRecord.model_validate(record.model_dump(mode="json")) + assert restored.obligation.obligation_id == record.obligation.obligation_id + assert restored.routing.routing_id == record.routing.routing_id + assert restored.attempts[0].attempt_id == record.attempts[0].attempt_id + + +# --------------------------------------------------------------------------- +# Digest determinism and sensitivity +# --------------------------------------------------------------------------- + + +def test_obligation_id_is_deterministic() -> None: + first = _obligation() + second = _obligation() + assert first.obligation_id == second.obligation_id + assert compute_obligation_id(first) == first.obligation_id + + +def test_obligation_id_excludes_itself() -> None: + obligation = _obligation() + digest_input = obligation_digest_input(obligation) + assert "obligation_id" not in digest_input + mutated = obligation.model_copy(update={"obligation_id": "totally-different"}) + assert compute_obligation_id(mutated) == compute_obligation_id(obligation) + + +def test_obligation_id_changes_when_semantic_field_changes() -> None: + base = _obligation() + changed = _obligation(abstraction={"kind": "access_control", "routes": ["/admin", "/root"]}) + assert compute_obligation_id(base) != compute_obligation_id(changed) + + +def test_abstraction_and_payload_digests_are_deterministic() -> None: + abstraction = {"a": 1, "b": [2, 3]} + payload = {"query": "sat", "b": 2, "a": 1} + assert compute_abstraction_digest(abstraction) == compute_abstraction_digest({"b": [2, 3], "a": 1}) + assert compute_payload_digest(payload) == compute_payload_digest({"a": 1, "b": 2, "query": "sat"}) + assert compute_abstraction_digest(abstraction) != compute_abstraction_digest({"a": 2}) + + +def test_routing_id_is_deterministic_and_order_insensitive_for_sets() -> None: + obligation = _obligation() + kwargs = dict( + obligation_id=obligation.obligation_id, + requested=["deterministic", "z3"], + eligible=[ + BackendCandidate(backend="z3", score=0.9, support="supported", guarantee_type="smt"), + BackendCandidate(backend="deterministic", score=0.5, support="supported", guarantee_type="det"), + ], + selected=[ + BackendSelection(backend="z3", reason="score", expected_guarantee="smt", score=0.9), + ], + rejected=[ + BackendRejection(backend="lean", reason="denied"), + ], + aggregation_policy="fail_dominant", + fallback_policy=_fallback(), + budget=_budget(), + policy_digest="policy", + router_version="0.1.0", + ) + left = compute_routing_id(**kwargs) + reordered = dict(kwargs) + reordered["requested"] = ["z3", "deterministic"] + reordered["eligible"] = list(reversed(kwargs["eligible"])) + right = compute_routing_id(**reordered) + assert left == right + + +def test_routing_id_changes_when_budget_or_router_version_changes() -> None: + obligation = _obligation() + base_kwargs = dict( + obligation_id=obligation.obligation_id, + requested=["z3"], + eligible=[BackendCandidate(backend="z3", score=1.0, support="supported", guarantee_type="smt")], + selected=[BackendSelection(backend="z3", reason="only", expected_guarantee="smt")], + rejected=[], + aggregation_policy="fail_dominant", + fallback_policy=_fallback(), + budget=_budget(), + policy_digest="policy", + router_version="0.1.0", + ) + base = compute_routing_id(**base_kwargs) + other_budget = _budget().model_copy(update={"max_memory_mb": 256}) + assert compute_routing_id(**{**base_kwargs, "budget": other_budget}) != base + assert compute_routing_id(**{**base_kwargs, "router_version": "0.2.0"}) != base + + +def test_attempt_id_excludes_wall_clock_timestamps() -> None: + attempt = _attempt("bo-1") + digest_input = attempt_digest_input(attempt) + assert "attempt_id" not in digest_input + assert "started_at" not in digest_input + assert "finished_at" not in digest_input + shifted = attempt.model_copy( + update={"started_at": "2099-01-01T00:00:00Z", "finished_at": "2099-01-01T00:00:01Z"} + ) + assert compute_attempt_id(shifted) == compute_attempt_id(attempt) + + +def test_attempt_id_changes_when_termination_changes() -> None: + attempt = _attempt("bo-1") + other = attempt.model_copy(update={"termination": "timeout", "exit_code": None}) + assert compute_attempt_id(attempt) != compute_attempt_id(other) + + +def test_materials_order_does_not_affect_obligation_id() -> None: + obligation = _obligation() + reversed_materials = list(reversed(obligation.materials)) + reordered = obligation.model_copy(update={"materials": reversed_materials}) + assert compute_obligation_id(reordered) == compute_obligation_id(obligation) + + +# --------------------------------------------------------------------------- +# Material URI validation +# --------------------------------------------------------------------------- + + +@pytest.mark.parametrize( + "uri", + [ + "src/auth.py", + ".github/workflows/ci.yml", + "repo:src/auth.py", + "ovk-material:diff/pr-1", + "https://example.com/plan.json", + "git:refs/heads/main", + ], +) +def test_material_uri_accepts_repo_relative_and_documented_schemes(uri: str) -> None: + assert validate_material_uri(uri) == uri + MaterialReference( + material_id="m", + kind="diff", + uri=uri, + sha256="b" * 64, + size_bytes=1, + ) + + +@pytest.mark.parametrize( + "uri", + [ + "/etc/passwd", + "C:\\Users\\secret\\file.txt", + "C:/Users/secret/file.txt", + "\\\\server\\share\\file", + "file:///tmp/x", + "file:/tmp/x", + ], +) +def test_material_uri_rejects_absolute_local_paths(uri: str) -> None: + assert is_absolute_local_path(uri) or uri.lower().startswith("file:") + with pytest.raises(ValueError, match="absolute local path|drive letter|not allowed"): + validate_material_uri(uri) + with pytest.raises(ValidationError): + MaterialReference( + material_id="m", + kind="source_file", + uri=uri, + sha256="c" * 64, + size_bytes=1, + ) + + +def test_material_uri_rejects_unknown_schemes() -> None: + with pytest.raises(ValueError, match="not allowed"): + validate_material_uri("s3://bucket/key") + + +# --------------------------------------------------------------------------- +# Schema validation +# --------------------------------------------------------------------------- + + +def test_coverage_schema_accepts_model() -> None: + report = validate_against_schema( + _coverage().model_dump(mode="json"), + load_json(SCHEMA_ROOT / "abstraction.coverage.schema.json"), + ) + assert report.valid, report.issues + + +def test_obligation_schema_accepts_model() -> None: + report = validate_against_schema( + _obligation().model_dump(mode="json"), + load_json(SCHEMA_ROOT / "verification.obligation.schema.json"), + ) + assert report.valid, report.issues + + +def test_routing_schema_accepts_model() -> None: + obligation = _obligation() + report = validate_against_schema( + _routing(obligation.obligation_id).model_dump(mode="json"), + load_json(SCHEMA_ROOT / "backend.routing.schema.json"), + ) + assert report.valid, report.issues + + +def test_execution_schema_accepts_all_artifact_shapes() -> None: + schema = load_json(SCHEMA_ROOT / "backend.execution.schema.json") + record = _execution_record() + payloads = [ + record.backend_obligations[0].model_dump(mode="json"), + record.attempts[0].model_dump(mode="json"), + record.results[0].model_dump(mode="json"), + record.model_dump(mode="json"), + ] + for payload in payloads: + report = validate_against_schema(payload, schema) + assert report.valid, report.issues + + +def test_obligation_schema_rejects_missing_required_field() -> None: + payload = _obligation().model_dump(mode="json") + del payload["policy_digest"] + report = validate_against_schema(payload, load_json(SCHEMA_ROOT / "verification.obligation.schema.json")) + assert not report.valid + + +def test_deep_copy_preserves_digests() -> None: + record = _execution_record() + cloned = ObligationExecutionRecord.model_validate(copy.deepcopy(record.model_dump(mode="json"))) + assert compute_obligation_id(cloned.obligation) == cloned.obligation.obligation_id + assert cloned.routing.routing_id == record.routing.routing_id