diff --git a/README.md b/README.md index 34bb8aa..2a3b54e 100644 --- a/README.md +++ b/README.md @@ -78,6 +78,7 @@ solving remains future work. | Native solver event trace | Implemented as separate opt-in reference/optimized entry points with bounded observed events, full initial state, checkpoints, manifest v3, independent offline replay, and deterministic PNG/GIF views | | Reproducible Z3 summaries | Implemented for fixed seed/thread settings and explicit Boolean/Wang encoding order, result/model, and stable project-owned counts; no internal Z3 trace claim | | Observed-run dossier | Implemented as one opt-in generator of closed raw run metadata, fixed LaTeX, PDF, and reused trace/square/hex assets; four versioned SAT/UNSAT case definitions cover distinct execution shapes | +| Full-pipeline multi-engine capture | Implemented as separate closed v2 case/run contracts and one atomic raw capture over Boolean Z3, one native reduction, reference, optimized, Wang Z3, and existing independent checkers; narrative assets and PDF v2 remain downstream work | | Native C JSON layer | Not implemented; `src/io/json.c` is a placeholder | | `TaskPlan` and native OpenMP solver | Not implemented; only the build scaffold exists | diff --git a/docs/plans/2026-08-31-narrative-migration-checklist.md b/docs/plans/2026-08-31-narrative-migration-checklist.md index 8c682e8..9327972 100644 --- a/docs/plans/2026-08-31-narrative-migration-checklist.md +++ b/docs/plans/2026-08-31-narrative-migration-checklist.md @@ -141,15 +141,15 @@ checks prove the old files are unreferenced before deletion. | `wang-run-case-v1` | `/run-dossiers/` | Preserve exact diagnostic case meaning and initial-domain override support | | `wang-run-dossier-v1` | `/run-dossiers/` | Preserve exact single-native-run report meaning and output shape | -- [ ] Add separate closed v2 case and dossier contracts; do not extend or +- [x] Add separate closed v2 case and dossier contracts; do not extend or loosen either v1 schema. -- [ ] Name Boolean Z3, reduction, reference, optimized, Wang Z3, verification, +- [x] Name Boolean Z3, reduction, reference, optimized, Wang Z3, verification, presentation, timings, and artifacts explicitly; do not use a generic stage array or plugin registry. -- [ ] Require one formula/region/tileset/provenance identity across all named +- [x] Require one formula/region/tileset/provenance identity across all named native and Z3 components. -- [ ] Forbid initial-domain overrides in full-pipeline v2 cases. -- [ ] Capture each engine once and reuse its result; do not solve during +- [x] Forbid initial-domain overrides in full-pipeline v2 cases. +- [x] Capture each engine once and reuse its result; do not solve during validation, rendering, Pages build, or PDF formatting. ## 7. Dossier v1 preservation checklist @@ -173,7 +173,7 @@ checks prove the old files are unreferenced before deletion. 1. [x] Freeze and test the exact generalized 14-to-23 mapping without changing the atomic tileset or standard square/hex output. -2. [ ] Capture the explicit v2 multi-engine fields once per engine and bind all +2. [x] Capture the explicit v2 multi-engine fields once per engine and bind all component identities by SHA-256. 3. [ ] Produce shared assets through the existing validators, replay, and compositor, including static semantic milestones. diff --git a/docs/run_dossiers.md b/docs/run_dossiers.md index 2d4383a..e731a5a 100644 --- a/docs/run_dossiers.md +++ b/docs/run_dossiers.md @@ -2,20 +2,25 @@ layout: page title: Observed-run dossiers and example index permalink: /run-dossiers/ -description: Opt-in LaTeX/PDF reports built from hash-bound solver traces, raw run metadata, and the existing square and hex render chain. +description: Opt-in v1 diagnostic reports and v2 multi-engine captures built from hash-bound traces, summaries, witnesses, and raw run metadata. section: Architecture and correctness document_kind: Reproduction and report contract status: Current implementation -updated: 2026-08-28 +updated: 2026-09-01 nav_order: 35 --- # Observed-run dossiers and example index -The report generator turns one configured native run into a self-contained -directory with `run.json`, `report.tex`, `report.pdf`, and `assets/`. It is -explicitly opt-in and does not change parsing, reduction, ordinary solving, -snapshot export, or the default Wang renderer. +The sole public generator dispatches closed v1 and v2 case documents to +separate implementations. Both are explicitly opt-in and leave parsing, +reduction, ordinary solving, snapshot export, and the default Wang renderer +unchanged. + +The v1 path turns one configured native run into a self-contained directory +with `run.json`, `report.tex`, `report.pdf`, and `assets/`. Its four diagnostic +cases, schemas, formatter, template, initial-domain behavior, and output shape +remain unchanged. `run.json` is the authoritative report input. It records the source and Git identity, environment, solver options and result, complete trace counters, @@ -94,3 +99,42 @@ Every example requires a complete trace. Selected frames remain a presentation subset of that trace. For UNSAT, `unsat_certificate` is always false: conflicts and trail history diagnose what the run observed but do not constitute a standalone mathematical proof of unsatisfiability. + +## Full-pipeline v2 capture + +`wang-run-case-v2` deliberately has no initial-domain override field. Its +canonical case follows `tests/instances/pipeline_sat.cm13` through the four +named engines and one shared native reduction: + +```sh +make shared +uv run --frozen python tools/generate_run_dossier.py \ + examples/run-cases-v2/pipeline-sat.json \ + build/run-dossiers/pipeline-sat-v2 +``` + +The v2 implementation parses and reduces once, then runs the traced reference +and optimized solvers exactly once while the same native formula and reduction +are alive. It invokes the existing Boolean Z3 and Wang Z3 summary producers +once each. SAT assignments and tilings are checked with the existing pure +Python checkers; native tilings also retain the assignment extracted by the +existing Yang--Zhang witness bridge. + +The raw v2 directory contains `run.json`, the copied CM1-in-3 input, two +existing trace-v3 manifests, their content-addressed snapshots, and the two +existing Z3 summary documents. Both native manifests bind the same formula, +tileset, region, and construction-provenance hashes. Agreement means equal +SAT/UNSAT status plus independently valid SAT witnesses; different valid +witnesses are not required to be byte-equal. UNKNOWN, mismatch, a truncated +trace, or a failed checker aborts the capture before installation. + +The raw-capture implementation intentionally produces no v2 PDF or narrative +raster. The closed run contract names the square, generalized, and hex +relationships and leaves their artifact references null for the shared-asset +pass. A later PDF formatter will consume those validated static assets without +solving, checking, replaying, or rendering again. + +All v2 durations use one monotonic nanosecond clock and are labelled +`run-specific-observation-not-a-benchmark`. They are raw facts about that +capture, never a performance comparison. SAT-only checker timings are null for +UNSAT rather than fabricated as zero. diff --git a/examples/run-cases-v2/pipeline-sat.json b/examples/run-cases-v2/pipeline-sat.json new file mode 100644 index 0000000..c0edcff --- /dev/null +++ b/examples/run-cases-v2/pipeline-sat.json @@ -0,0 +1,18 @@ +{ + "schema": "wang-run-case-v2", + "id": "pipeline-sat-v2", + "title": "Canonical SAT full-pipeline multi-engine capture", + "purpose": "Capture the named Boolean Z3, native reduction, reference, optimized, Wang Z3, and independent verification results for the canonical pipeline_sat.cm13 instance without domain overrides.", + "source": "tests/instances/pipeline_sat.cm13", + "expected_status": "sat", + "reference_trace": { + "event_capacity": 8192, + "checkpoint_interval": 128, + "checkpoint_capacity": 64 + }, + "optimized_trace": { + "event_capacity": 8192, + "checkpoint_interval": 128, + "checkpoint_capacity": 64 + } +} diff --git a/python/dossier/__init__.py b/python/dossier/__init__.py new file mode 100644 index 0000000..64edd0b --- /dev/null +++ b/python/dossier/__init__.py @@ -0,0 +1 @@ +"""Opt-in dossier capture leaves; core and oracle modules never import this package.""" diff --git a/python/dossier/multi_engine.py b/python/dossier/multi_engine.py new file mode 100644 index 0000000..d6b0432 --- /dev/null +++ b/python/dossier/multi_engine.py @@ -0,0 +1,419 @@ +"""Atomic full-pipeline v2 capture over fixed named engines.""" + +from __future__ import annotations + +from datetime import datetime, timezone +import hashlib +import os +from pathlib import Path +import platform as platform_module +import shutil +import subprocess +import tempfile +from time import perf_counter_ns + +from formats.pipeline_snapshot import _encode_document, _write_atomic +from formats.run_case_v2 import ( + MultiEngineRunCase, + TraceConfiguration, + load_run_case_v2, +) +from formats.run_dossier_v2 import ARTIFACT_NAMES +from formats.run_dossier_v2_builder import build_run_dossier_v2 +from formats.run_dossier_v2_bundle import load_run_dossier_v2 +from formats.solver_trace_snapshot import ( + dump_solver_trace_bundle, + load_solver_trace_bundle, +) +from formats.z3_encoding_summary import ( + build_boolean_z3_summary, + build_wang_z3_summary, +) +from native.multi_engine_pipeline import ( + TraceCaptureOptions, + capture_multi_engine_native_pipeline, +) +from oracles.tiling_check import is_valid_tiling +from oracles.witness_check import is_valid_assignment +from model.tileset import TILESET + + +ROOT = Path(__file__).resolve().parents[2] + + +class MultiEngineDossierError(RuntimeError): + """The fixed v2 capture could not be completed atomically.""" + + +def _git_commit() -> str: + try: + completed = subprocess.run( + ["git", "rev-parse", "HEAD"], + cwd=ROOT, + check=True, + capture_output=True, + text=True, + timeout=10, + ) + except (OSError, subprocess.SubprocessError) as error: + raise MultiEngineDossierError( + f"cannot identify repository commit: {error}" + ) from error + return completed.stdout.strip() + + +def _native_options(configuration: TraceConfiguration) -> TraceCaptureOptions: + return TraceCaptureOptions( + event_capacity=configuration.event_capacity, + checkpoint_interval=configuration.checkpoint_interval, + checkpoint_capacity=configuration.checkpoint_capacity, + ) + + +def _artifact( + dossier_root: Path, + path: Path, + *, + source_sha256: str, + media_type: str, + schema: str | None, + role: str, + semantics: str, +) -> dict[str, object]: + try: + encoded = path.read_bytes() + relative = path.relative_to(dossier_root).as_posix() + except (OSError, ValueError) as error: + raise MultiEngineDossierError(f"cannot bind artifact {path!s}: {error}") from error + return { + "path": relative, + "sha256": hashlib.sha256(encoded).hexdigest(), + "media_type": media_type, + "schema": schema, + "role": role, + "semantics": semantics, + "form": "data", + "source_sha256": source_sha256, + } + + +def _manifest_artifact( + dossier_root: Path, + manifest_path: Path, + manifest: dict[str, object], + name: str, + *, + source_sha256: str, + role: str, + semantics: str, +) -> dict[str, object] | None: + references = manifest["artifacts"] + assert isinstance(references, dict) + reference = references[name] + if reference is None: + return None + assert isinstance(reference, dict) + return _artifact( + dossier_root, + manifest_path.parent / str(reference["path"]), + source_sha256=source_sha256, + media_type="application/json", + schema=str(reference["schema"]), + role=role, + semantics=semantics, + ) + + +def _collect_artifacts( + staging: Path, + source_copy: Path, + source_sha256: str, + reference_manifest_path: Path, + reference_manifest: dict[str, object], + optimized_manifest_path: Path, + optimized_manifest: dict[str, object], + boolean_summary_path: Path, + wang_summary_path: Path, +) -> dict[str, dict[str, object] | None]: + artifacts: dict[str, dict[str, object] | None] = { + "source_input": _artifact( + staging, + source_copy, + source_sha256=source_sha256, + media_type="text/plain", + schema=None, + role="self-contained CM1-in-3 source input", + semantics="observed", + ), + "formula_snapshot": _manifest_artifact( + staging, + reference_manifest_path, + reference_manifest, + "formula", + source_sha256=source_sha256, + role="parsed formula snapshot shared by all engines", + semantics="observed", + ), + "tileset_snapshot": _manifest_artifact( + staging, + reference_manifest_path, + reference_manifest, + "tileset", + source_sha256=source_sha256, + role="canonical 23-tile table shared by Wang engines", + semantics="canonical-construction", + ), + "region_snapshot": _manifest_artifact( + staging, + reference_manifest_path, + reference_manifest, + "region", + source_sha256=source_sha256, + role="single native reduction region", + semantics="observed", + ), + "provenance_snapshot": _manifest_artifact( + staging, + reference_manifest_path, + reference_manifest, + "reduction", + source_sha256=source_sha256, + role="single native reduction provenance", + semantics="canonical-construction", + ), + "boolean_z3_summary": _artifact( + staging, + boolean_summary_path, + source_sha256=source_sha256, + media_type="application/json", + schema="z3-encoding-summary-v1", + role="Boolean Z3 encoding and returned model summary", + semantics="encoding-order", + ), + "reference_trace_manifest": _artifact( + staging, + reference_manifest_path, + source_sha256=source_sha256, + media_type="application/json", + schema="wang-explain-manifest-v3", + role="reference solver trace manifest", + semantics="observed", + ), + "reference_trace": _manifest_artifact( + staging, + reference_manifest_path, + reference_manifest, + "trace", + source_sha256=source_sha256, + role="complete observed reference trace", + semantics="observed", + ), + "reference_solution": _manifest_artifact( + staging, + reference_manifest_path, + reference_manifest, + "solution", + source_sha256=source_sha256, + role="verified reference square witness", + semantics="observed", + ), + "optimized_trace_manifest": _artifact( + staging, + optimized_manifest_path, + source_sha256=source_sha256, + media_type="application/json", + schema="wang-explain-manifest-v3", + role="optimized solver trace manifest", + semantics="observed", + ), + "optimized_trace": _manifest_artifact( + staging, + optimized_manifest_path, + optimized_manifest, + "trace", + source_sha256=source_sha256, + role="complete observed optimized trace", + semantics="observed", + ), + "optimized_solution": _manifest_artifact( + staging, + optimized_manifest_path, + optimized_manifest, + "solution", + source_sha256=source_sha256, + role="verified optimized square witness", + semantics="observed", + ), + "wang_z3_summary": _artifact( + staging, + wang_summary_path, + source_sha256=source_sha256, + media_type="application/json", + schema="z3-encoding-summary-v1", + role="Wang Z3 encoding and returned model summary", + semantics="encoding-order", + ), + "square_presentation": None, + "generalized_presentation": None, + "hex_presentation": None, + } + if tuple(artifacts) != ARTIFACT_NAMES: + raise MultiEngineDossierError("internal artifact order diverged from contract") + return artifacts + + +def _install_directory(staging: Path, destination: Path) -> None: + """Single replace boundary kept injectable for atomic failure tests.""" + os.replace(staging, destination) + + +def generate_multi_engine_dossier( + case_path: str | Path, + output_directory: str | Path, +) -> Path: + """Capture all named engines once and atomically install the raw v2 dossier.""" + case: MultiEngineRunCase = load_run_case_v2(case_path, ROOT) + destination = Path(output_directory).resolve() + if destination.exists(): + raise MultiEngineDossierError( + f"output directory already exists: {destination!s}" + ) + destination.parent.mkdir(parents=True, exist_ok=True) + staging = Path( + tempfile.mkdtemp(prefix=f".{destination.name}.", dir=destination.parent) + ) + try: + source_path = ROOT / case.source + source_bytes = source_path.read_bytes() + source_sha256 = hashlib.sha256(source_bytes).hexdigest() + capture = capture_multi_engine_native_pipeline( + source_path, + reference_options=_native_options(case.reference_trace), + optimized_options=_native_options(case.optimized_trace), + ) + + data = staging / "assets/data" + data.mkdir(parents=True) + source_copy = data / source_path.name + reference_manifest_path = data / "reference-manifest.json" + optimized_manifest_path = data / "optimized-manifest.json" + boolean_summary_path = data / "boolean-z3.json" + wang_summary_path = data / "wang-z3.json" + + started = perf_counter_ns() + _write_atomic(source_copy, source_bytes) + dump_solver_trace_bundle( + reference_manifest_path, + source_path, + capture.formula, + capture.region, + capture.explanation, + capture.reference.result, + capture.reference.trace, + ) + dump_solver_trace_bundle( + optimized_manifest_path, + source_path, + capture.formula, + capture.region, + capture.explanation, + capture.optimized.result, + capture.optimized.trace, + ) + reference_manifest, _ = load_solver_trace_bundle(reference_manifest_path) + optimized_manifest, _ = load_solver_trace_bundle(optimized_manifest_path) + export_ns = perf_counter_ns() - started + region_reference = reference_manifest["artifacts"]["region"] + assert isinstance(region_reference, dict) + region_sha256 = str(region_reference["sha256"]) + + started = perf_counter_ns() + boolean_summary = build_boolean_z3_summary( + capture.formula, + source_formula_sha256=source_sha256, + ) + boolean_z3_ns = perf_counter_ns() - started + boolean_assignment = boolean_summary["model"]["assignment"] + if boolean_summary["status"] == "sat": + started = perf_counter_ns() + if not isinstance(boolean_assignment, list) or not is_valid_assignment( + capture.formula, boolean_assignment + ): + raise MultiEngineDossierError( + "Boolean Z3 assignment failed the independent checker" + ) + boolean_z3_verify_ns: int | None = perf_counter_ns() - started + else: + boolean_z3_verify_ns = None + + started = perf_counter_ns() + wang_summary = build_wang_z3_summary( + capture.formula, + capture.region, + source_formula_sha256=source_sha256, + region_sha256=region_sha256, + ) + wang_z3_ns = perf_counter_ns() - started + wang_cells = wang_summary["model"]["cells"] + if wang_summary["status"] == "sat": + started = perf_counter_ns() + if not isinstance(wang_cells, list) or not is_valid_tiling( + capture.region, TILESET, wang_cells + ): + raise MultiEngineDossierError( + "Wang Z3 tiling failed the independent checker" + ) + wang_z3_verify_ns: int | None = perf_counter_ns() - started + else: + wang_z3_verify_ns = None + + started = perf_counter_ns() + _write_atomic(boolean_summary_path, _encode_document(boolean_summary)) + _write_atomic(wang_summary_path, _encode_document(wang_summary)) + artifacts = _collect_artifacts( + staging, + source_copy, + source_sha256, + reference_manifest_path, + reference_manifest, + optimized_manifest_path, + optimized_manifest, + boolean_summary_path, + wang_summary_path, + ) + export_ns += perf_counter_ns() - started + + captured_at = datetime.now(timezone.utc).replace(microsecond=0) + timings_ns: dict[str, int | None] = { + "parse_ns": capture.timings.parse_ns, + "reduction_ns": capture.timings.reduction_ns, + "boolean_z3_ns": boolean_z3_ns, + "boolean_z3_verify_ns": boolean_z3_verify_ns, + "reference_solve_ns": capture.timings.reference_solve_ns, + "reference_verify_ns": capture.timings.reference_verify_ns, + "optimized_solve_ns": capture.timings.optimized_solve_ns, + "optimized_verify_ns": capture.timings.optimized_verify_ns, + "wang_z3_ns": wang_z3_ns, + "wang_z3_verify_ns": wang_z3_verify_ns, + "export_ns": export_ns, + } + run_document = build_run_dossier_v2( + case, + capture, + source_sha256=source_sha256, + captured_at_utc=captured_at.strftime("%Y-%m-%dT%H:%M:%SZ"), + platform=platform_module.platform(), + python_version=platform_module.python_version(), + git_commit=_git_commit(), + boolean_summary=boolean_summary, + wang_summary=wang_summary, + timings_ns=timings_ns, + artifacts=artifacts, + ) + _write_atomic(staging / "run.json", _encode_document(run_document)) + load_run_dossier_v2(staging / "run.json") + _install_directory(staging, destination) + return destination + except Exception: + shutil.rmtree(staging, ignore_errors=True) + raise diff --git a/python/formats/run_case_v2.py b/python/formats/run_case_v2.py new file mode 100644 index 0000000..47003c1 --- /dev/null +++ b/python/formats/run_case_v2.py @@ -0,0 +1,138 @@ +"""Closed full-pipeline case contract for multi-engine dossiers.""" + +from __future__ import annotations + +from dataclasses import dataclass +from pathlib import Path +import re +from typing import Final + +from formats.pipeline_snapshot import ( + PipelineSnapshotError, + _load_json_bytes, + _require_exact_fields, + _require_integer, + _require_literal, + _require_object, +) +from formats.run_contract import _nonempty_string, _relative_path + + +CASE_SCHEMA: Final = "wang-run-case-v2" +_STATUSES: Final = frozenset({"sat", "unsat"}) +_CASE_ID = re.compile(r"[a-z0-9]+(?:-[a-z0-9]+)*\Z") +_TRACE_FIELDS = frozenset( + {"event_capacity", "checkpoint_interval", "checkpoint_capacity"} +) + + +@dataclass(frozen=True, slots=True) +class TraceConfiguration: + event_capacity: int + checkpoint_interval: int + checkpoint_capacity: int + + +@dataclass(frozen=True, slots=True) +class MultiEngineRunCase: + identifier: str + title: str + purpose: str + source: str + expected_status: str + reference_trace: TraceConfiguration + optimized_trace: TraceConfiguration + + +def _load_trace_configuration(value: object, path: str) -> TraceConfiguration: + trace = _require_object(value, path) + _require_exact_fields(trace, _TRACE_FIELDS, path) + event_capacity = _require_integer( + trace["event_capacity"], f"{path}.event_capacity", nonnegative=True + ) + checkpoint_interval = _require_integer( + trace["checkpoint_interval"], + f"{path}.checkpoint_interval", + nonnegative=True, + ) + checkpoint_capacity = _require_integer( + trace["checkpoint_capacity"], + f"{path}.checkpoint_capacity", + nonnegative=True, + ) + if not 2 <= event_capacity <= 100_000: + raise PipelineSnapshotError( + f"{path}.event_capacity: must be in [2, 100000]" + ) + if (checkpoint_interval == 0) != (checkpoint_capacity == 0): + raise PipelineSnapshotError( + f"{path}: checkpoint interval and capacity must be jointly set" + ) + return TraceConfiguration( + event_capacity=event_capacity, + checkpoint_interval=checkpoint_interval, + checkpoint_capacity=checkpoint_capacity, + ) + + +def load_run_case_v2( + path: str | Path, + repository_root: str | Path, +) -> MultiEngineRunCase: + """Load one strict full-pipeline case; overrides are not in its vocabulary.""" + case_path = Path(path) + try: + document = _load_json_bytes(case_path.read_bytes(), str(case_path)) + except OSError as error: + raise PipelineSnapshotError( + f"cannot read v2 case {case_path!s}: {error}" + ) from error + _require_exact_fields( + document, + frozenset( + { + "schema", + "id", + "title", + "purpose", + "source", + "expected_status", + "reference_trace", + "optimized_trace", + } + ), + "$", + ) + _require_literal(document["schema"], CASE_SCHEMA, "$.schema") + identifier = _nonempty_string(document["id"], "$.id") + if _CASE_ID.fullmatch(identifier) is None: + raise PipelineSnapshotError( + "$.id: must be a lowercase hyphenated identifier" + ) + title = _nonempty_string(document["title"], "$.title") + purpose = _nonempty_string(document["purpose"], "$.purpose") + source = _relative_path(document["source"], "$.source") + if not source.endswith(".cm13"): + raise PipelineSnapshotError("$.source: must name a .cm13 input") + if not (Path(repository_root) / source).is_file(): + raise PipelineSnapshotError( + f"$.source: repository input does not exist: {source}" + ) + expected_status = _nonempty_string( + document["expected_status"], "$.expected_status" + ) + if expected_status not in _STATUSES: + raise PipelineSnapshotError("$.expected_status: must equal sat or unsat") + return MultiEngineRunCase( + identifier=identifier, + title=title, + purpose=purpose, + source=source, + expected_status=expected_status, + reference_trace=_load_trace_configuration( + document["reference_trace"], "$.reference_trace" + ), + optimized_trace=_load_trace_configuration( + document["optimized_trace"], "$.optimized_trace" + ), + ) diff --git a/python/formats/run_contract.py b/python/formats/run_contract.py new file mode 100644 index 0000000..3211a0c --- /dev/null +++ b/python/formats/run_contract.py @@ -0,0 +1,45 @@ +"""Small transport-validation helpers shared by closed dossier versions.""" + +from pathlib import PurePosixPath +import re + +from formats.pipeline_snapshot import ( + PipelineSnapshotError, + _require_integer, + _require_string, +) + + +def _nonempty_string(value: object, path: str) -> str: + text = _require_string(value, path) + if not text or text != text.strip(): + raise PipelineSnapshotError(f"{path}: must be nonempty without edge space") + return text + + +def _boolean(value: object, path: str) -> bool: + if type(value) is not bool: + raise PipelineSnapshotError(f"{path}: must be a boolean") + return value + + +def _nullable_integer(value: object, path: str) -> int | None: + if value is None: + return None + return _require_integer(value, path, nonnegative=True) + + +def _relative_path(value: object, path: str, *, prefix: str | None = None) -> str: + text = _nonempty_string(value, path) + if "\\" in text or re.fullmatch(r"[A-Za-z0-9._/-]+", text) is None: + raise PipelineSnapshotError( + f"{path}: must use only portable POSIX path characters" + ) + parsed = PurePosixPath(text) + if parsed.is_absolute() or parsed.as_posix() != text or any( + part in ("", ".", "..") for part in parsed.parts + ): + raise PipelineSnapshotError(f"{path}: must be a normalized relative path") + if prefix is not None and (not parsed.parts or parsed.parts[0] != prefix): + raise PipelineSnapshotError(f"{path}: must remain below {prefix}/") + return text diff --git a/python/formats/run_dossier.py b/python/formats/run_dossier.py index a3ff085..a301844 100644 --- a/python/formats/run_dossier.py +++ b/python/formats/run_dossier.py @@ -4,7 +4,7 @@ from dataclasses import dataclass import hashlib -from pathlib import Path, PurePosixPath +from pathlib import Path import re from typing import Final @@ -17,7 +17,12 @@ _require_literal, _require_object, _require_sha256, - _require_string, +) +from formats.run_contract import ( + _boolean, + _nonempty_string, + _nullable_integer, + _relative_path, ) from model.region import Region from model.solver_trace import DOMAIN_ALL, SolverTrace @@ -69,41 +74,6 @@ class RunCase: initial_domain_overrides: tuple[InitialDomainOverride, ...] -def _nonempty_string(value: object, path: str) -> str: - text = _require_string(value, path) - if not text or text != text.strip(): - raise PipelineSnapshotError(f"{path}: must be nonempty without edge space") - return text - - -def _boolean(value: object, path: str) -> bool: - if type(value) is not bool: - raise PipelineSnapshotError(f"{path}: must be a boolean") - return value - - -def _nullable_integer(value: object, path: str) -> int | None: - if value is None: - return None - return _require_integer(value, path, nonnegative=True) - - -def _relative_path(value: object, path: str, *, prefix: str | None = None) -> str: - text = _nonempty_string(value, path) - if "\\" in text or re.fullmatch(r"[A-Za-z0-9._/-]+", text) is None: - raise PipelineSnapshotError( - f"{path}: must use only portable POSIX path characters" - ) - parsed = PurePosixPath(text) - if parsed.is_absolute() or parsed.as_posix() != text or any( - part in ("", ".", "..") for part in parsed.parts - ): - raise PipelineSnapshotError(f"{path}: must be a normalized relative path") - if prefix is not None and (not parsed.parts or parsed.parts[0] != prefix): - raise PipelineSnapshotError(f"{path}: must remain below {prefix}/") - return text - - def _validate_case_override_shape( classification: str, overrides: tuple[InitialDomainOverride, ...], diff --git a/python/formats/run_dossier_v2.py b/python/formats/run_dossier_v2.py new file mode 100644 index 0000000..26ede0e --- /dev/null +++ b/python/formats/run_dossier_v2.py @@ -0,0 +1,611 @@ +"""Closed full-pipeline case and run contracts for multi-engine dossiers.""" + +from __future__ import annotations + +import hashlib +import re +from typing import Final, Sequence + +from formats.pipeline_snapshot import ( + PipelineSnapshotError, + _encode_document, + _require_exact_fields, + _require_integer, + _require_literal, + _require_object, + _require_sha256, +) +from formats.run_case_v2 import _load_trace_configuration +from formats.run_contract import _boolean, _nonempty_string, _relative_path +from model.tileset import TILESET + + +RUN_SCHEMA: Final = "wang-run-dossier-v2" +STATUSES: Final = frozenset({"sat", "unsat"}) +_CASE_ID = re.compile(r"[a-z0-9]+(?:-[a-z0-9]+)*\Z") +_GIT_COMMIT = re.compile(r"[0-9a-f]{40}\Z") +_TRACE_FIELDS = frozenset( + {"event_capacity", "checkpoint_interval", "checkpoint_capacity"} +) +_ARTIFACT_FIELDS = frozenset( + { + "path", + "sha256", + "media_type", + "schema", + "role", + "semantics", + "form", + "source_sha256", + } +) +_MEDIA_TYPES = frozenset( + {"application/json", "text/plain", "image/png", "image/gif"} +) +_SEMANTICS = frozenset( + { + "observed", + "canonical-construction", + "encoding-order", + "verified-transformation", + "didactic", + } +) +_FORMS = frozenset({"data", "static", "animated"}) +_JSON_ARTIFACTS = frozenset( + { + "formula_snapshot", + "tileset_snapshot", + "region_snapshot", + "provenance_snapshot", + "boolean_z3_summary", + "reference_trace_manifest", + "reference_trace", + "reference_solution", + "optimized_trace_manifest", + "optimized_trace", + "optimized_solution", + "wang_z3_summary", + } +) +ARTIFACT_NAMES: Final = ( + "source_input", + "formula_snapshot", + "tileset_snapshot", + "region_snapshot", + "provenance_snapshot", + "boolean_z3_summary", + "reference_trace_manifest", + "reference_trace", + "reference_solution", + "optimized_trace_manifest", + "optimized_trace", + "optimized_solution", + "wang_z3_summary", + "square_presentation", + "generalized_presentation", + "hex_presentation", +) +_PRESENTATION_ARTIFACTS = frozenset( + {"square_presentation", "generalized_presentation", "hex_presentation"} +) +_TIMING_FIELDS = frozenset( + { + "clock", + "identity", + "parse_ns", + "reduction_ns", + "boolean_z3_ns", + "boolean_z3_verify_ns", + "reference_solve_ns", + "reference_verify_ns", + "optimized_solve_ns", + "optimized_verify_ns", + "wang_z3_ns", + "wang_z3_verify_ns", + "export_ns", + } +) + + +def _nullable_nonnegative(value: object, path: str) -> int | None: + if value is None: + return None + return _require_integer(value, path, nonnegative=True) + + +def witness_sha256(values: Sequence[bool | int | None] | None) -> str | None: + """Hash one witness payload without binding it to an engine document.""" + if values is None: + return None + return hashlib.sha256(_encode_document({"witness": list(values)})).hexdigest() + + +def _validate_assignment(value: object, path: str) -> tuple[bool, ...] | None: + if value is None: + return None + if type(value) is not list or any(type(item) is not bool for item in value): + raise PipelineSnapshotError(f"{path}: must be null or a boolean array") + return tuple(value) + + +def _validate_cells(value: object, path: str) -> tuple[int | None, ...] | None: + if value is None: + return None + if type(value) is not list: + raise PipelineSnapshotError(f"{path}: must be null or a dense cell array") + cells: list[int | None] = [] + for index, tile_id in enumerate(value): + if tile_id is None: + cells.append(None) + continue + parsed = _require_integer(tile_id, f"{path}[{index}]", nonnegative=True) + if parsed >= len(TILESET): + raise PipelineSnapshotError( + f"{path}[{index}]: lies outside the canonical tileset" + ) + cells.append(parsed) + return tuple(cells) + + +def _validate_z3_record(value: object, path: str, *, wang: bool) -> str: + record = _require_object(value, path) + witness_field = "cells" if wang else "assignment" + _require_exact_fields( + record, + frozenset( + { + "status", + "configuration", + "encoding_summary_sha256", + witness_field, + "witness_sha256", + } + ), + path, + ) + status = _nonempty_string(record["status"], f"{path}.status") + if status not in STATUSES: + raise PipelineSnapshotError(f"{path}.status: must equal sat or unsat") + configuration = _require_object(record["configuration"], f"{path}.configuration") + _require_exact_fields( + configuration, frozenset({"random_seed", "threads"}), f"{path}.configuration" + ) + if configuration != {"random_seed": 0, "threads": 1}: + raise PipelineSnapshotError(f"{path}.configuration: must equal the fixed Z3 setup") + _require_sha256( + record["encoding_summary_sha256"], f"{path}.encoding_summary_sha256" + ) + witness = ( + _validate_cells(record[witness_field], f"{path}.{witness_field}") + if wang + else _validate_assignment(record[witness_field], f"{path}.{witness_field}") + ) + digest = record["witness_sha256"] + if status == "sat": + if witness is None: + raise PipelineSnapshotError(f"{path}.{witness_field}: SAT requires a witness") + _require_sha256(digest, f"{path}.witness_sha256") + if digest != witness_sha256(witness): + raise PipelineSnapshotError(f"{path}.witness_sha256: does not match witness") + elif witness is not None or digest is not None: + raise PipelineSnapshotError(f"{path}: UNSAT forbids witness data") + return status + + +def _validate_native_record(value: object, path: str, solver: str) -> str: + record = _require_object(value, path) + _require_exact_fields( + record, + frozenset( + { + "status", + "configuration", + "trace", + "solution_sha256", + "witness_sha256", + "extracted_assignment", + } + ), + path, + ) + status = _nonempty_string(record["status"], f"{path}.status") + if status not in STATUSES: + raise PipelineSnapshotError(f"{path}.status: must equal sat or unsat") + _load_trace_configuration(record["configuration"], f"{path}.configuration") + trace = _require_object(record["trace"], f"{path}.trace") + _require_exact_fields( + trace, + frozenset( + { + "solver", + "manifest_sha256", + "trace_sha256", + "complete", + "truncated", + "event_capacity", + "observed_event_count", + "checkpoint_interval", + "checkpoint_capacity", + "checkpoint_count", + "selection", + } + ), + f"{path}.trace", + ) + _require_literal(trace["solver"], solver, f"{path}.trace.solver") + _require_sha256(trace["manifest_sha256"], f"{path}.trace.manifest_sha256") + _require_sha256(trace["trace_sha256"], f"{path}.trace.trace_sha256") + if not _boolean(trace["complete"], f"{path}.trace.complete"): + raise PipelineSnapshotError(f"{path}.trace.complete: v2 requires a complete trace") + if _boolean(trace["truncated"], f"{path}.trace.truncated"): + raise PipelineSnapshotError(f"{path}.trace.truncated: must remain false") + event_capacity = _require_integer( + trace["event_capacity"], f"{path}.trace.event_capacity", nonnegative=True + ) + observed = _require_integer( + trace["observed_event_count"], + f"{path}.trace.observed_event_count", + nonnegative=True, + ) + checkpoint_interval = _require_integer( + trace["checkpoint_interval"], + f"{path}.trace.checkpoint_interval", + nonnegative=True, + ) + checkpoint_capacity = _require_integer( + trace["checkpoint_capacity"], + f"{path}.trace.checkpoint_capacity", + nonnegative=True, + ) + checkpoint_count = _require_integer( + trace["checkpoint_count"], + f"{path}.trace.checkpoint_count", + nonnegative=True, + ) + if observed < 2 or observed > event_capacity or checkpoint_count > checkpoint_capacity: + raise PipelineSnapshotError(f"{path}.trace: inconsistent trace counts") + if (checkpoint_interval == 0) != (checkpoint_capacity == 0): + raise PipelineSnapshotError(f"{path}.trace: inconsistent checkpoint setup") + selection = _require_object(trace["selection"], f"{path}.trace.selection") + _require_exact_fields( + selection, + frozenset({"performed", "selected_event_count"}), + f"{path}.trace.selection", + ) + performed = _boolean(selection["performed"], f"{path}.trace.selection.performed") + selected = _nullable_nonnegative( + selection["selected_event_count"], + f"{path}.trace.selection.selected_event_count", + ) + if performed != (selected is not None) or (selected is not None and selected > observed): + raise PipelineSnapshotError(f"{path}.trace.selection: is inconsistent") + configuration = _require_object(record["configuration"], f"{path}.configuration") + for name in _TRACE_FIELDS: + if configuration[name] != trace[name]: + raise PipelineSnapshotError( + f"{path}.trace.{name}: disagrees with configured capture" + ) + solution_digest = record["solution_sha256"] + witness_digest = record["witness_sha256"] + assignment = _validate_assignment( + record["extracted_assignment"], f"{path}.extracted_assignment" + ) + if status == "sat": + _require_sha256(solution_digest, f"{path}.solution_sha256") + _require_sha256(witness_digest, f"{path}.witness_sha256") + if assignment is None: + raise PipelineSnapshotError(f"{path}: SAT requires an extracted assignment") + elif solution_digest is not None or witness_digest is not None or assignment is not None: + raise PipelineSnapshotError(f"{path}: UNSAT forbids witness data") + return status + + +def _validate_check(value: object, path: str, *, performed: bool) -> None: + check = _require_object(value, path) + _require_exact_fields( + check, + frozenset({"checker", "performed", "passed", "witness_sha256"}), + path, + ) + _nonempty_string(check["checker"], f"{path}.checker") + if _boolean(check["performed"], f"{path}.performed") is not performed: + raise PipelineSnapshotError(f"{path}.performed: disagrees with status") + if performed: + if check["passed"] is not True: + raise PipelineSnapshotError(f"{path}.passed: performed checks must pass") + _require_sha256(check["witness_sha256"], f"{path}.witness_sha256") + elif check["passed"] is not None or check["witness_sha256"] is not None: + raise PipelineSnapshotError(f"{path}: unperformed checks require null results") + + +def validate_run_dossier_v2(document: object) -> None: + """Validate the closed transport and all internal named cross-fields.""" + root = _require_object(document, "$") + _require_exact_fields( + root, + frozenset( + { + "schema", + "case", + "source", + "environment", + "boolean_z3", + "reduction", + "reference", + "optimized", + "wang_z3", + "verification", + "agreement", + "presentation", + "timings", + "artifacts", + } + ), + "$", + ) + _require_literal(root["schema"], RUN_SCHEMA, "$.schema") + + case = _require_object(root["case"], "$.case") + _require_exact_fields( + case, frozenset({"id", "title", "purpose", "expected_status"}), "$.case" + ) + identifier = _nonempty_string(case["id"], "$.case.id") + if _CASE_ID.fullmatch(identifier) is None: + raise PipelineSnapshotError("$.case.id: is invalid") + _nonempty_string(case["title"], "$.case.title") + _nonempty_string(case["purpose"], "$.case.purpose") + expected_status = _nonempty_string( + case["expected_status"], "$.case.expected_status" + ) + if expected_status not in STATUSES: + raise PipelineSnapshotError("$.case.expected_status: must equal sat or unsat") + + source = _require_object(root["source"], "$.source") + _require_exact_fields(source, frozenset({"path", "sha256"}), "$.source") + if not _relative_path(source["path"], "$.source.path").endswith(".cm13"): + raise PipelineSnapshotError("$.source.path: must name a .cm13 input") + source_sha256 = _require_sha256(source["sha256"], "$.source.sha256") + + environment = _require_object(root["environment"], "$.environment") + _require_exact_fields( + environment, + frozenset({"captured_at_utc", "platform", "python", "git_commit"}), + "$.environment", + ) + captured = _nonempty_string( + environment["captured_at_utc"], "$.environment.captured_at_utc" + ) + if re.fullmatch(r"\d{4}-\d{2}-\d{2}T\d{2}:\d{2}:\d{2}Z", captured) is None: + raise PipelineSnapshotError( + "$.environment.captured_at_utc: must be UTC seconds" + ) + _nonempty_string(environment["platform"], "$.environment.platform") + _nonempty_string(environment["python"], "$.environment.python") + commit = _nonempty_string(environment["git_commit"], "$.environment.git_commit") + if _GIT_COMMIT.fullmatch(commit) is None: + raise PipelineSnapshotError("$.environment.git_commit: must be a full SHA-1") + + statuses = { + "boolean_z3": _validate_z3_record(root["boolean_z3"], "$.boolean_z3", wang=False), + "reference": _validate_native_record(root["reference"], "$.reference", "reference"), + "optimized": _validate_native_record(root["optimized"], "$.optimized", "optimized"), + "wang_z3": _validate_z3_record(root["wang_z3"], "$.wang_z3", wang=True), + } + if any(status != expected_status for status in statuses.values()): + raise PipelineSnapshotError("engine status mismatch") + + reduction = _require_object(root["reduction"], "$.reduction") + _require_exact_fields( + reduction, + frozenset( + { + "formula_sha256", + "tileset_sha256", + "region_sha256", + "provenance_sha256", + } + ), + "$.reduction", + ) + for name, digest in reduction.items(): + _require_sha256(digest, f"$.reduction.{name}") + + verification = _require_object(root["verification"], "$.verification") + check_names = ( + "boolean_z3_assignment", + "reference_tiling", + "reference_assignment", + "optimized_tiling", + "optimized_assignment", + "wang_z3_tiling", + ) + _require_exact_fields(verification, frozenset(check_names), "$.verification") + for name in check_names: + _validate_check( + verification[name], + f"$.verification.{name}", + performed=expected_status == "sat", + ) + if expected_status == "sat": + expected_check_digests = { + "boolean_z3_assignment": root["boolean_z3"]["witness_sha256"], + "reference_tiling": root["reference"]["witness_sha256"], + "reference_assignment": witness_sha256( + root["reference"]["extracted_assignment"] + ), + "optimized_tiling": root["optimized"]["witness_sha256"], + "optimized_assignment": witness_sha256( + root["optimized"]["extracted_assignment"] + ), + "wang_z3_tiling": root["wang_z3"]["witness_sha256"], + } + for name, digest in expected_check_digests.items(): + if verification[name]["witness_sha256"] != digest: + raise PipelineSnapshotError( + f"$.verification.{name}.witness_sha256: cross-field mismatch" + ) + + agreement = _require_object(root["agreement"], "$.agreement") + _require_exact_fields( + agreement, + frozenset( + { + "expected_status", + "boolean_z3_status", + "reference_status", + "optimized_status", + "wang_z3_status", + "all_status_equal", + "sat_witnesses_valid", + "passed", + } + ), + "$.agreement", + ) + for name in ( + "expected_status", + "boolean_z3_status", + "reference_status", + "optimized_status", + "wang_z3_status", + ): + if agreement[name] != expected_status: + raise PipelineSnapshotError(f"$.agreement.{name}: disagrees with case") + if agreement["all_status_equal"] is not True or agreement["passed"] is not True: + raise PipelineSnapshotError("$.agreement: engine disagreement is a failure") + expected_witness_validity = True if expected_status == "sat" else None + if agreement["sat_witnesses_valid"] is not expected_witness_validity: + raise PipelineSnapshotError("$.agreement.sat_witnesses_valid: is inconsistent") + + presentation = _require_object(root["presentation"], "$.presentation") + presentation_specs = { + "square": "verified-wang-solution", + "generalized": "exact-14-to-23-presentation", + "hex": "checked-square-to-hex-transformation", + } + _require_exact_fields(presentation, frozenset(presentation_specs), "$.presentation") + for name, relationship in presentation_specs.items(): + item = _require_object(presentation[name], f"$.presentation.{name}") + _require_exact_fields( + item, frozenset({"relationship", "applicable", "artifact"}), + f"$.presentation.{name}", + ) + _require_literal( + item["relationship"], relationship, f"$.presentation.{name}.relationship" + ) + if _boolean(item["applicable"], f"$.presentation.{name}.applicable") is not ( + expected_status == "sat" + ): + raise PipelineSnapshotError(f"$.presentation.{name}.applicable: disagrees") + expected_artifact = f"{name}_presentation" + if item["artifact"] not in (None, expected_artifact): + raise PipelineSnapshotError(f"$.presentation.{name}.artifact: is invalid") + + timings = _require_object(root["timings"], "$.timings") + _require_exact_fields(timings, _TIMING_FIELDS, "$.timings") + _require_literal(timings["clock"], "monotonic-perf-counter-ns", "$.timings.clock") + _require_literal( + timings["identity"], "run-specific-observation-not-a-benchmark", + "$.timings.identity", + ) + nullable = { + "boolean_z3_verify_ns", + "reference_verify_ns", + "optimized_verify_ns", + "wang_z3_verify_ns", + } + for name in _TIMING_FIELDS - {"clock", "identity"}: + elapsed = _nullable_nonnegative(timings[name], f"$.timings.{name}") + if name in nullable: + if (elapsed is None) != (expected_status == "unsat"): + raise PipelineSnapshotError( + f"$.timings.{name}: applicability disagrees" + ) + elif elapsed is None: + raise PipelineSnapshotError(f"$.timings.{name}: must be performed") + + artifacts = _require_object(root["artifacts"], "$.artifacts") + _require_exact_fields(artifacts, frozenset(ARTIFACT_NAMES), "$.artifacts") + paths: set[str] = set() + for name in ARTIFACT_NAMES: + raw = artifacts[name] + may_be_null = name in _PRESENTATION_ARTIFACTS or name.endswith("_solution") + if raw is None: + if not may_be_null: + raise PipelineSnapshotError(f"$.artifacts.{name}: is required") + if name.endswith("_solution") and expected_status == "sat": + raise PipelineSnapshotError(f"$.artifacts.{name}: SAT requires a solution") + continue + if name.endswith("_solution") and expected_status == "unsat": + raise PipelineSnapshotError(f"$.artifacts.{name}: UNSAT forbids a solution") + item = _require_object(raw, f"$.artifacts.{name}") + _require_exact_fields(item, _ARTIFACT_FIELDS, f"$.artifacts.{name}") + relative = _relative_path( + item["path"], f"$.artifacts.{name}.path", prefix="assets" + ) + if relative in paths: + raise PipelineSnapshotError(f"$.artifacts.{name}.path: duplicates another artifact") + paths.add(relative) + _require_sha256(item["sha256"], f"$.artifacts.{name}.sha256") + media_type = _nonempty_string( + item["media_type"], f"$.artifacts.{name}.media_type" + ) + if media_type not in _MEDIA_TYPES: + raise PipelineSnapshotError(f"$.artifacts.{name}.media_type: is unsupported") + expected_media_type = ( + "text/plain" + if name == "source_input" + else "application/json" + if name in _JSON_ARTIFACTS + else "image/png" + ) + if media_type != expected_media_type: + raise PipelineSnapshotError( + f"$.artifacts.{name}.media_type: must equal {expected_media_type}" + ) + if item["schema"] is not None: + _nonempty_string(item["schema"], f"$.artifacts.{name}.schema") + _nonempty_string(item["role"], f"$.artifacts.{name}.role") + semantics = _nonempty_string( + item["semantics"], f"$.artifacts.{name}.semantics" + ) + if semantics not in _SEMANTICS: + raise PipelineSnapshotError(f"$.artifacts.{name}.semantics: is unsupported") + form = _nonempty_string(item["form"], f"$.artifacts.{name}.form") + if form not in _FORMS: + raise PipelineSnapshotError(f"$.artifacts.{name}.form: is unsupported") + if item["source_sha256"] != source_sha256: + raise PipelineSnapshotError(f"$.artifacts.{name}.source_sha256: disagrees") + + for name, digest in ( + ("formula_snapshot", reduction["formula_sha256"]), + ("tileset_snapshot", reduction["tileset_sha256"]), + ("region_snapshot", reduction["region_sha256"]), + ("provenance_snapshot", reduction["provenance_sha256"]), + ("boolean_z3_summary", root["boolean_z3"]["encoding_summary_sha256"]), + ("reference_trace_manifest", root["reference"]["trace"]["manifest_sha256"]), + ("reference_trace", root["reference"]["trace"]["trace_sha256"]), + ("optimized_trace_manifest", root["optimized"]["trace"]["manifest_sha256"]), + ("optimized_trace", root["optimized"]["trace"]["trace_sha256"]), + ("wang_z3_summary", root["wang_z3"]["encoding_summary_sha256"]), + ): + if artifacts[name]["sha256"] != digest: + raise PipelineSnapshotError(f"$.artifacts.{name}.sha256: cross-field mismatch") + if artifacts["source_input"]["sha256"] != source_sha256: + raise PipelineSnapshotError( + "$.artifacts.source_input.sha256: must match the source identity" + ) + for solver in ("reference", "optimized"): + solution = artifacts[f"{solver}_solution"] + if expected_status == "sat" and solution["sha256"] != root[solver]["solution_sha256"]: + raise PipelineSnapshotError( + f"$.artifacts.{solver}_solution.sha256: cross-field mismatch" + ) + for name in ("square", "generalized", "hex"): + artifact_name = f"{name}_presentation" + selected = presentation[name]["artifact"] + if (selected is None) != (artifacts[artifact_name] is None): + raise PipelineSnapshotError( + f"$.presentation.{name}.artifact: disagrees with artifacts" + ) diff --git a/python/formats/run_dossier_v2_builder.py b/python/formats/run_dossier_v2_builder.py new file mode 100644 index 0000000..d252f8d --- /dev/null +++ b/python/formats/run_dossier_v2_builder.py @@ -0,0 +1,253 @@ +"""Builder for one successful fixed-engine v2 dossier document.""" + +from __future__ import annotations + +from typing import TYPE_CHECKING + +from formats.pipeline_snapshot import PipelineSnapshotError +from formats.run_case_v2 import MultiEngineRunCase, TraceConfiguration +from formats.run_dossier_v2 import ( + ARTIFACT_NAMES, + RUN_SCHEMA, + STATUSES, + _TIMING_FIELDS, + _validate_assignment, + _validate_cells, + validate_run_dossier_v2, + witness_sha256, +) +from formats.z3_encoding_summary import validate_z3_encoding_summary +from model.tileset import TILESET +from oracles.tiling_check import is_valid_tiling +from oracles.witness_check import is_valid_assignment + +if TYPE_CHECKING: + from native.multi_engine_pipeline import MultiEngineNativeCapture + + +def _trace_record( + capture: object, + configuration: TraceConfiguration, + manifest_sha256: str, + trace_sha256: str, +) -> dict[str, object]: + trace = capture.trace + result = capture.result + return { + "status": result.status.value, + "configuration": { + "event_capacity": configuration.event_capacity, + "checkpoint_interval": configuration.checkpoint_interval, + "checkpoint_capacity": configuration.checkpoint_capacity, + }, + "trace": { + "solver": trace.solver, + "manifest_sha256": manifest_sha256, + "trace_sha256": trace_sha256, + "complete": not trace.truncated, + "truncated": trace.truncated, + "event_capacity": trace.event_capacity, + "observed_event_count": trace.observed_event_count, + "checkpoint_interval": trace.checkpoint_interval, + "checkpoint_capacity": trace.checkpoint_capacity, + "checkpoint_count": len(trace.checkpoints), + "selection": { + "performed": False, + "selected_event_count": None, + }, + }, + "solution_sha256": None, + "witness_sha256": witness_sha256(result.tiling), + "extracted_assignment": ( + None + if capture.extracted_assignment is None + else list(capture.extracted_assignment) + ), + } + + +def _check_record(checker: str, digest: str | None) -> dict[str, object]: + return { + "checker": checker, + "performed": digest is not None, + "passed": True if digest is not None else None, + "witness_sha256": digest, + } + + +def build_run_dossier_v2( + case: MultiEngineRunCase, + capture: "MultiEngineNativeCapture", + *, + source_sha256: str, + captured_at_utc: str, + platform: str, + python_version: str, + git_commit: str, + boolean_summary: dict[str, object], + wang_summary: dict[str, object], + timings_ns: dict[str, int | None], + artifacts: dict[str, dict[str, object] | None], +) -> dict[str, object]: + """Build one successful named-engine capture; mismatches are fatal.""" + if not isinstance(case, MultiEngineRunCase): + raise TypeError("case must be a MultiEngineRunCase") + validate_z3_encoding_summary(boolean_summary) + validate_z3_encoding_summary(wang_summary) + statuses = { + "boolean_z3": boolean_summary["status"], + "reference": capture.reference.result.status.value, + "optimized": capture.optimized.result.status.value, + "wang_z3": wang_summary["status"], + } + if any(status not in STATUSES for status in statuses.values()): + raise PipelineSnapshotError("full-pipeline dossier forbids UNKNOWN results") + if any(status != case.expected_status for status in statuses.values()): + raise PipelineSnapshotError("engine status mismatch") + if capture.reference.trace.truncated or capture.optimized.trace.truncated: + raise PipelineSnapshotError("full-pipeline dossier requires complete traces") + + boolean_assignment = _validate_assignment( + boolean_summary["model"]["assignment"], + "boolean_summary.model.assignment", + ) + wang_cells = _validate_cells( + wang_summary["model"]["cells"], "wang_summary.model.cells" + ) + if case.expected_status == "sat": + if boolean_assignment is None or not is_valid_assignment( + capture.formula, boolean_assignment + ): + raise PipelineSnapshotError( + "Boolean Z3 assignment failed independent check" + ) + if wang_cells is None or not is_valid_tiling( + capture.region, TILESET, wang_cells + ): + raise PipelineSnapshotError("Wang Z3 tiling failed independent check") + + required_timing_names = _TIMING_FIELDS - {"clock", "identity"} + if frozenset(timings_ns) != required_timing_names: + raise PipelineSnapshotError("timings do not match the fixed v2 contract") + if frozenset(artifacts) != frozenset(ARTIFACT_NAMES): + raise PipelineSnapshotError("artifacts do not match the fixed v2 contract") + + reference = _trace_record( + capture.reference, + case.reference_trace, + artifacts["reference_trace_manifest"]["sha256"], + artifacts["reference_trace"]["sha256"], + ) + optimized = _trace_record( + capture.optimized, + case.optimized_trace, + artifacts["optimized_trace_manifest"]["sha256"], + artifacts["optimized_trace"]["sha256"], + ) + if case.expected_status == "sat": + reference["solution_sha256"] = artifacts["reference_solution"]["sha256"] + optimized["solution_sha256"] = artifacts["optimized_solution"]["sha256"] + + boolean_digest = witness_sha256(boolean_assignment) + wang_digest = witness_sha256(wang_cells) + reference_digest = reference["witness_sha256"] + optimized_digest = optimized["witness_sha256"] + document: dict[str, object] = { + "schema": RUN_SCHEMA, + "case": { + "id": case.identifier, + "title": case.title, + "purpose": case.purpose, + "expected_status": case.expected_status, + }, + "source": {"path": case.source, "sha256": source_sha256}, + "environment": { + "captured_at_utc": captured_at_utc, + "platform": platform, + "python": python_version, + "git_commit": git_commit, + }, + "boolean_z3": { + "status": statuses["boolean_z3"], + "configuration": {"random_seed": 0, "threads": 1}, + "encoding_summary_sha256": artifacts["boolean_z3_summary"]["sha256"], + "assignment": ( + None if boolean_assignment is None else list(boolean_assignment) + ), + "witness_sha256": boolean_digest, + }, + "reduction": { + "formula_sha256": artifacts["formula_snapshot"]["sha256"], + "tileset_sha256": artifacts["tileset_snapshot"]["sha256"], + "region_sha256": artifacts["region_snapshot"]["sha256"], + "provenance_sha256": artifacts["provenance_snapshot"]["sha256"], + }, + "reference": reference, + "optimized": optimized, + "wang_z3": { + "status": statuses["wang_z3"], + "configuration": {"random_seed": 0, "threads": 1}, + "encoding_summary_sha256": artifacts["wang_z3_summary"]["sha256"], + "cells": None if wang_cells is None else list(wang_cells), + "witness_sha256": wang_digest, + }, + "verification": { + "boolean_z3_assignment": _check_record( + "oracles.witness_check.is_valid_assignment", boolean_digest + ), + "reference_tiling": _check_record( + "oracles.tiling_check.is_valid_tiling", reference_digest + ), + "reference_assignment": _check_record( + "oracles.witness_check.is_valid_assignment", + witness_sha256(capture.reference.extracted_assignment), + ), + "optimized_tiling": _check_record( + "oracles.tiling_check.is_valid_tiling", optimized_digest + ), + "optimized_assignment": _check_record( + "oracles.witness_check.is_valid_assignment", + witness_sha256(capture.optimized.extracted_assignment), + ), + "wang_z3_tiling": _check_record( + "oracles.tiling_check.is_valid_tiling", wang_digest + ), + }, + "agreement": { + "expected_status": case.expected_status, + "boolean_z3_status": statuses["boolean_z3"], + "reference_status": statuses["reference"], + "optimized_status": statuses["optimized"], + "wang_z3_status": statuses["wang_z3"], + "all_status_equal": True, + "sat_witnesses_valid": ( + True if case.expected_status == "sat" else None + ), + "passed": True, + }, + "presentation": { + "square": { + "relationship": "verified-wang-solution", + "applicable": case.expected_status == "sat", + "artifact": None, + }, + "generalized": { + "relationship": "exact-14-to-23-presentation", + "applicable": case.expected_status == "sat", + "artifact": None, + }, + "hex": { + "relationship": "checked-square-to-hex-transformation", + "applicable": case.expected_status == "sat", + "artifact": None, + }, + }, + "timings": { + "clock": "monotonic-perf-counter-ns", + "identity": "run-specific-observation-not-a-benchmark", + **timings_ns, + }, + "artifacts": artifacts, + } + validate_run_dossier_v2(document) + return document diff --git a/python/formats/run_dossier_v2_bundle.py b/python/formats/run_dossier_v2_bundle.py new file mode 100644 index 0000000..40b090e --- /dev/null +++ b/python/formats/run_dossier_v2_bundle.py @@ -0,0 +1,204 @@ +"""Self-contained loader for an already captured multi-engine v2 dossier.""" + +from __future__ import annotations + +import hashlib +from pathlib import Path + +from formats.pipeline_snapshot import ( + DIRECTIONS, + PipelineSnapshotError, + _load_json_bytes, +) +from formats.run_dossier_v2 import validate_run_dossier_v2, witness_sha256 +from formats.solver_trace_snapshot import load_solver_trace_bundle +from formats.z3_encoding_summary import validate_z3_encoding_summary +from model.formula import Formula +from model.region import Region +from model.tileset import COLOR_NONE, TILESET +from oracles.tiling_check import is_valid_tiling +from oracles.witness_check import is_valid_assignment + + +def _formula_from_snapshot(document: dict[str, object]) -> Formula: + clauses = document["clauses"] + assert isinstance(clauses, list) + return Formula( + variable_count=int(document["variable_count"]), + clauses=tuple(tuple(item["variables"]) for item in clauses), + ) + + +def _region_from_snapshot(document: dict[str, object]) -> Region: + bounds = document["bounds"] + assert isinstance(bounds, dict) + width = int(bounds["max_x_inclusive"]) - int(bounds["min_x_inclusive"]) + 1 + height = int(bounds["max_y_inclusive"]) - int(bounds["min_y_inclusive"]) + 1 + active = tuple(document["active"]) + raw_boundary = document["boundary"] + assert isinstance(raw_boundary, list) + boundary = tuple( + (COLOR_NONE, COLOR_NONE, COLOR_NONE, COLOR_NONE) + if sides is None + else tuple( + COLOR_NONE if sides[direction] is None else sides[direction] + for direction in DIRECTIONS + ) + for sides in raw_boundary + ) + return Region(width=width, height=height, active=active, boundary=boundary) + + +def load_run_dossier_v2(path: str | Path) -> dict[str, object]: + """Verify files, existing bundles, witnesses, and shared identities.""" + run_path = Path(path) + try: + document = _load_json_bytes(run_path.read_bytes(), str(run_path)) + except OSError as error: + raise PipelineSnapshotError( + f"cannot read v2 dossier {run_path!s}: {error}" + ) from error + validate_run_dossier_v2(document) + artifacts = document["artifacts"] + assert isinstance(artifacts, dict) + try: + root = run_path.parent.resolve(strict=True) + except OSError as error: + raise PipelineSnapshotError( + f"cannot resolve v2 dossier root: {error}" + ) from error + artifact_paths: dict[str, Path] = {} + documents: dict[str, dict[str, object]] = {} + for name, raw in artifacts.items(): + if raw is None: + continue + assert isinstance(raw, dict) + try: + candidate = (run_path.parent / str(raw["path"])).resolve(strict=True) + if not candidate.is_relative_to(root) or not candidate.is_file(): + raise PipelineSnapshotError( + f"$.artifacts.{name}.path: escapes dossier" + ) + encoded = candidate.read_bytes() + except PipelineSnapshotError: + raise + except OSError as error: + raise PipelineSnapshotError( + f"$.artifacts.{name}.path: cannot read artifact: {error}" + ) from error + if hashlib.sha256(encoded).hexdigest() != raw["sha256"]: + raise PipelineSnapshotError( + f"$.artifacts.{name}.sha256: does not match file" + ) + artifact_paths[name] = candidate + if raw["media_type"] == "application/json": + documents[name] = _load_json_bytes(encoded, str(candidate)) + + source_bytes = artifact_paths["source_input"].read_bytes() + if hashlib.sha256(source_bytes).hexdigest() != document["source"]["sha256"]: + raise PipelineSnapshotError( + "$.source.sha256: does not match self-contained input" + ) + + reference_manifest, reference_documents = load_solver_trace_bundle( + artifact_paths["reference_trace_manifest"] + ) + optimized_manifest, optimized_documents = load_solver_trace_bundle( + artifact_paths["optimized_trace_manifest"] + ) + for name in ("formula", "tileset", "region", "reduction"): + reference_digest = reference_manifest["artifacts"][name]["sha256"] + optimized_digest = optimized_manifest["artifacts"][name]["sha256"] + if reference_digest != optimized_digest: + raise PipelineSnapshotError( + f"native manifests disagree on shared {name}" + ) + shared_fields = { + "formula": "formula_sha256", + "tileset": "tileset_sha256", + "region": "region_sha256", + "reduction": "provenance_sha256", + } + for manifest_name, run_name in shared_fields.items(): + manifest_digest = reference_manifest["artifacts"][manifest_name]["sha256"] + if manifest_digest != document["reduction"][run_name]: + raise PipelineSnapshotError( + f"native manifest {manifest_name} identity disagrees with run" + ) + for solver, manifest in ( + ("reference", reference_manifest), + ("optimized", optimized_manifest), + ): + trace_digest = manifest["artifacts"]["trace"]["sha256"] + if trace_digest != document[solver]["trace"]["trace_sha256"]: + raise PipelineSnapshotError(f"{solver} manifest trace identity mismatch") + solution_reference = manifest["artifacts"]["solution"] + if document["case"]["expected_status"] == "sat": + if solution_reference["sha256"] != document[solver]["solution_sha256"]: + raise PipelineSnapshotError( + f"{solver} manifest solution identity mismatch" + ) + elif solution_reference is not None: + raise PipelineSnapshotError( + f"{solver} UNSAT manifest contains a solution" + ) + if reference_documents["tileset"] != optimized_documents["tileset"]: + raise PipelineSnapshotError("native manifests disagree on tileset") + tile_documents = reference_documents["tileset"]["tiles"] + canonical_tiles = tuple( + tuple(tile["edges"][direction] for direction in DIRECTIONS) + for tile in tile_documents + ) + if canonical_tiles != TILESET: + raise PipelineSnapshotError( + "native manifests do not bind the canonical tileset" + ) + + boolean_summary = documents["boolean_z3_summary"] + wang_summary = documents["wang_z3_summary"] + validate_z3_encoding_summary(boolean_summary) + validate_z3_encoding_summary(wang_summary) + source_sha256 = document["source"]["sha256"] + region_sha256 = document["reduction"]["region_sha256"] + if boolean_summary["source_formula_sha256"] != source_sha256: + raise PipelineSnapshotError("Boolean Z3 source identity mismatch") + if ( + wang_summary["source_formula_sha256"] != source_sha256 + or wang_summary["region_sha256"] != region_sha256 + ): + raise PipelineSnapshotError("Wang Z3 source or region identity mismatch") + + formula = _formula_from_snapshot(reference_documents["formula"]) + region = _region_from_snapshot(reference_documents["region"]) + if document["case"]["expected_status"] == "sat": + boolean_assignment = tuple(boolean_summary["model"]["assignment"]) + wang_cells = tuple(wang_summary["model"]["cells"]) + if not is_valid_assignment(formula, boolean_assignment): + raise PipelineSnapshotError( + "Boolean Z3 assignment failed independent check" + ) + if not is_valid_tiling(region, TILESET, wang_cells): + raise PipelineSnapshotError("Wang Z3 tiling failed independent check") + for solver, bundle in ( + ("reference", reference_documents), + ("optimized", optimized_documents), + ): + cells = tuple(bundle["solution"]["cells"]) + if not is_valid_tiling(region, TILESET, cells): + raise PipelineSnapshotError( + f"{solver} tiling failed independent check" + ) + if document[solver]["witness_sha256"] != witness_sha256(cells): + raise PipelineSnapshotError(f"{solver} witness digest mismatch") + assignment = tuple(document[solver]["extracted_assignment"]) + if not is_valid_assignment(formula, assignment): + raise PipelineSnapshotError( + f"{solver} assignment failed independent check" + ) + if document["boolean_z3"]["witness_sha256"] != witness_sha256( + boolean_assignment + ): + raise PipelineSnapshotError("Boolean Z3 witness digest mismatch") + if document["wang_z3"]["witness_sha256"] != witness_sha256(wang_cells): + raise PipelineSnapshotError("Wang Z3 witness digest mismatch") + return document diff --git a/python/native/multi_engine_pipeline.py b/python/native/multi_engine_pipeline.py new file mode 100644 index 0000000..858002e --- /dev/null +++ b/python/native/multi_engine_pipeline.py @@ -0,0 +1,217 @@ +"""Fixed one-lifetime native capture for the full-pipeline v2 dossier.""" + +from __future__ import annotations + +from dataclasses import dataclass +from time import perf_counter_ns +from typing import Callable + +from model.formula import Formula +from model.reduction_explanation import ReductionExplanation +from model.region import Region +from model.solver_trace import SolverTrace +from model.tiling import TilingSolveResult, TilingSolveStatus +from model.tileset import TILESET +from native.formula_adapter import PathLike, _copy_formula, _loaded_formula +from native.region_adapter import ( + _built_explained_reduction, + _copy_reduction_explanation, + _copy_region, +) +from native.solver_trace_adapter import _solve_native_traced +from native.witness_adapter import NativeWitnessError, _extract_assignment +from oracles.tiling_check import is_valid_tiling +from oracles.witness_check import is_valid_assignment + + +@dataclass(frozen=True, slots=True) +class TraceCaptureOptions: + """Closed traced-solver options for one named native engine.""" + + event_capacity: int + checkpoint_interval: int + checkpoint_capacity: int + + def __post_init__(self) -> None: + for name in ( + "event_capacity", + "checkpoint_interval", + "checkpoint_capacity", + ): + value = getattr(self, name) + if type(value) is not int or value < 0: + raise ValueError(f"{name} must be a nonnegative integer") + if self.event_capacity < 2: + raise ValueError("event_capacity must be at least two") + if (self.checkpoint_interval == 0) != (self.checkpoint_capacity == 0): + raise ValueError( + "checkpoint_interval and checkpoint_capacity must be jointly set" + ) + + +@dataclass(frozen=True, slots=True) +class NativeEngineCapture: + """Fully copied result, trace, and decoded assignment for one solver.""" + + result: TilingSolveResult + trace: SolverTrace + extracted_assignment: tuple[bool, ...] | None + + +@dataclass(frozen=True, slots=True) +class MultiEngineNativeTimings: + """Run-specific monotonic durations for the fixed native capture.""" + + parse_ns: int + reduction_ns: int + reference_solve_ns: int + reference_verify_ns: int | None + optimized_solve_ns: int + optimized_verify_ns: int | None + + def __post_init__(self) -> None: + for name in ( + "parse_ns", + "reduction_ns", + "reference_solve_ns", + "optimized_solve_ns", + ): + value = getattr(self, name) + if type(value) is not int or value < 0: + raise ValueError(f"{name} must be a nonnegative integer") + for name in ("reference_verify_ns", "optimized_verify_ns"): + value = getattr(self, name) + if value is not None and (type(value) is not int or value < 0): + raise ValueError(f"{name} must be null or a nonnegative integer") + + +@dataclass(frozen=True, slots=True) +class MultiEngineNativeCapture: + """All Python-owned values copied before the shared C lifetime ends.""" + + formula: Formula + region: Region + explanation: ReductionExplanation + reference: NativeEngineCapture + optimized: NativeEngineCapture + timings: MultiEngineNativeTimings + + +def _elapsed_ns(clock_ns: Callable[[], int], started: int) -> int: + finished = clock_ns() + if type(started) is not int or type(finished) is not int or finished < started: + raise RuntimeError("monotonic clock returned an invalid interval") + return finished - started + + +def _verify_and_extract( + native_formula: object, + native_reduction: object, + formula: Formula, + region: Region, + result: TilingSolveResult, +) -> tuple[bool, ...] | None: + if result.status is TilingSolveStatus.UNSAT: + return None + if result.status is not TilingSolveStatus.SAT or result.tiling is None: + raise NativeWitnessError("native dossier solve returned an unsupported result") + if not is_valid_tiling(region, TILESET, result.tiling): + raise NativeWitnessError( + "native dossier SAT tiling was rejected by the Python checker" + ) + assignment = _extract_assignment( + native_formula, + native_reduction, + region, + result.tiling, + ) + if assignment is None or not is_valid_assignment(formula, assignment): + raise NativeWitnessError( + "native dossier SAT tiling did not decode to a valid assignment" + ) + return assignment + + +def capture_multi_engine_native_pipeline( + path: PathLike, + *, + reference_options: TraceCaptureOptions, + optimized_options: TraceCaptureOptions, + clock_ns: Callable[[], int] = perf_counter_ns, +) -> MultiEngineNativeCapture: + """Parse and reduce once, then capture reference and optimized exactly once.""" + if not isinstance(reference_options, TraceCaptureOptions): + raise TypeError("reference_options must be TraceCaptureOptions") + if not isinstance(optimized_options, TraceCaptureOptions): + raise TypeError("optimized_options must be TraceCaptureOptions") + if not callable(clock_ns): + raise TypeError("clock_ns must be callable") + + started = clock_ns() + with _loaded_formula(path) as native_formula: + formula = _copy_formula(native_formula) + parse_ns = _elapsed_ns(clock_ns, started) + + started = clock_ns() + with _built_explained_reduction(native_formula) as native_reduction: + region = _copy_region(native_reduction.reduction.region) + explanation = _copy_reduction_explanation( + native_reduction, + int(native_formula.variable_count), + ) + reduction_ns = _elapsed_ns(clock_ns, started) + + captures: dict[str, NativeEngineCapture] = {} + solve_timings: dict[str, int] = {} + verify_timings: dict[str, int | None] = {} + for name, optimized, options in ( + ("reference", False, reference_options), + ("optimized", True, optimized_options), + ): + started = clock_ns() + result, trace = _solve_native_traced( + native_reduction.reduction, + region, + optimized=optimized, + event_capacity=options.event_capacity, + checkpoint_interval=options.checkpoint_interval, + checkpoint_capacity=options.checkpoint_capacity, + ) + solve_timings[name] = _elapsed_ns(clock_ns, started) + + if result.status is TilingSolveStatus.SAT: + started = clock_ns() + assignment = _verify_and_extract( + native_formula, + native_reduction.reduction, + formula, + region, + result, + ) + verify_timings[name] = _elapsed_ns(clock_ns, started) + else: + assignment = _verify_and_extract( + native_formula, + native_reduction.reduction, + formula, + region, + result, + ) + verify_timings[name] = None + captures[name] = NativeEngineCapture(result, trace, assignment) + + return MultiEngineNativeCapture( + formula=formula, + region=region, + explanation=explanation, + reference=captures["reference"], + optimized=captures["optimized"], + timings=MultiEngineNativeTimings( + parse_ns=parse_ns, + reduction_ns=reduction_ns, + reference_solve_ns=solve_timings["reference"], + reference_verify_ns=verify_timings["reference"], + optimized_solve_ns=solve_timings["optimized"], + optimized_verify_ns=verify_timings["optimized"], + ), + ) diff --git a/schemas/wang-run-case-v2.schema.json b/schemas/wang-run-case-v2.schema.json new file mode 100644 index 0000000..105a20f --- /dev/null +++ b/schemas/wang-run-case-v2.schema.json @@ -0,0 +1,39 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://xtraid.github.io/tiling-foundry/schemas/wang-run-case-v2.schema.json", + "title": "Tiling Foundry full-pipeline multi-engine case v2", + "type": "object", + "additionalProperties": false, + "required": [ + "schema", + "id", + "title", + "purpose", + "source", + "expected_status", + "reference_trace", + "optimized_trace" + ], + "properties": { + "schema": {"const": "wang-run-case-v2"}, + "id": {"type": "string", "pattern": "^[a-z0-9]+(?:-[a-z0-9]+)*$"}, + "title": {"type": "string", "minLength": 1}, + "purpose": {"type": "string", "minLength": 1}, + "source": {"type": "string", "pattern": "^(?!/)(?!.*(?:^|/)\\.\\.?/).+\\.cm13$"}, + "expected_status": {"enum": ["sat", "unsat"]}, + "reference_trace": {"$ref": "#/$defs/trace"}, + "optimized_trace": {"$ref": "#/$defs/trace"} + }, + "$defs": { + "trace": { + "type": "object", + "additionalProperties": false, + "required": ["event_capacity", "checkpoint_interval", "checkpoint_capacity"], + "properties": { + "event_capacity": {"type": "integer", "minimum": 2, "maximum": 100000}, + "checkpoint_interval": {"type": "integer", "minimum": 0}, + "checkpoint_capacity": {"type": "integer", "minimum": 0} + } + } + } +} diff --git a/schemas/wang-run-dossier-v2.schema.json b/schemas/wang-run-dossier-v2.schema.json new file mode 100644 index 0000000..ac4e83b --- /dev/null +++ b/schemas/wang-run-dossier-v2.schema.json @@ -0,0 +1,430 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://xtraid.github.io/tiling-foundry/schemas/wang-run-dossier-v2.schema.json", + "title": "Tiling Foundry full-pipeline multi-engine dossier v2", + "type": "object", + "additionalProperties": false, + "required": [ + "schema", + "case", + "source", + "environment", + "boolean_z3", + "reduction", + "reference", + "optimized", + "wang_z3", + "verification", + "agreement", + "presentation", + "timings", + "artifacts" + ], + "properties": { + "schema": {"const": "wang-run-dossier-v2"}, + "case": { + "type": "object", + "additionalProperties": false, + "required": ["id", "title", "purpose", "expected_status"], + "properties": { + "id": {"type": "string", "pattern": "^[a-z0-9]+(?:-[a-z0-9]+)*$"}, + "title": {"type": "string", "minLength": 1}, + "purpose": {"type": "string", "minLength": 1}, + "expected_status": {"enum": ["sat", "unsat"]} + } + }, + "source": { + "type": "object", + "additionalProperties": false, + "required": ["path", "sha256"], + "properties": { + "path": {"type": "string", "minLength": 1}, + "sha256": {"$ref": "#/$defs/sha256"} + } + }, + "environment": { + "type": "object", + "additionalProperties": false, + "required": ["captured_at_utc", "platform", "python", "git_commit"], + "properties": { + "captured_at_utc": { + "type": "string", + "pattern": "^[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}Z$" + }, + "platform": {"type": "string", "minLength": 1}, + "python": {"type": "string", "minLength": 1}, + "git_commit": {"type": "string", "pattern": "^[0-9a-f]{40}$"} + } + }, + "boolean_z3": {"$ref": "#/$defs/boolean_z3"}, + "reduction": { + "type": "object", + "additionalProperties": false, + "required": [ + "formula_sha256", + "tileset_sha256", + "region_sha256", + "provenance_sha256" + ], + "properties": { + "formula_sha256": {"$ref": "#/$defs/sha256"}, + "tileset_sha256": {"$ref": "#/$defs/sha256"}, + "region_sha256": {"$ref": "#/$defs/sha256"}, + "provenance_sha256": {"$ref": "#/$defs/sha256"} + } + }, + "reference": {"$ref": "#/$defs/native_engine"}, + "optimized": {"$ref": "#/$defs/native_engine"}, + "wang_z3": {"$ref": "#/$defs/wang_z3"}, + "verification": { + "type": "object", + "additionalProperties": false, + "required": [ + "boolean_z3_assignment", + "reference_tiling", + "reference_assignment", + "optimized_tiling", + "optimized_assignment", + "wang_z3_tiling" + ], + "properties": { + "boolean_z3_assignment": {"$ref": "#/$defs/check"}, + "reference_tiling": {"$ref": "#/$defs/check"}, + "reference_assignment": {"$ref": "#/$defs/check"}, + "optimized_tiling": {"$ref": "#/$defs/check"}, + "optimized_assignment": {"$ref": "#/$defs/check"}, + "wang_z3_tiling": {"$ref": "#/$defs/check"} + } + }, + "agreement": { + "type": "object", + "additionalProperties": false, + "required": [ + "expected_status", + "boolean_z3_status", + "reference_status", + "optimized_status", + "wang_z3_status", + "all_status_equal", + "sat_witnesses_valid", + "passed" + ], + "properties": { + "expected_status": {"enum": ["sat", "unsat"]}, + "boolean_z3_status": {"enum": ["sat", "unsat"]}, + "reference_status": {"enum": ["sat", "unsat"]}, + "optimized_status": {"enum": ["sat", "unsat"]}, + "wang_z3_status": {"enum": ["sat", "unsat"]}, + "all_status_equal": {"const": true}, + "sat_witnesses_valid": {"type": ["boolean", "null"]}, + "passed": {"const": true} + } + }, + "presentation": { + "type": "object", + "additionalProperties": false, + "required": ["square", "generalized", "hex"], + "properties": { + "square": { + "$ref": "#/$defs/presentation", + "properties": { + "relationship": {"const": "verified-wang-solution"}, + "artifact": {"enum": ["square_presentation", null]} + } + }, + "generalized": { + "$ref": "#/$defs/presentation", + "properties": { + "relationship": {"const": "exact-14-to-23-presentation"}, + "artifact": {"enum": ["generalized_presentation", null]} + } + }, + "hex": { + "$ref": "#/$defs/presentation", + "properties": { + "relationship": {"const": "checked-square-to-hex-transformation"}, + "artifact": {"enum": ["hex_presentation", null]} + } + } + } + }, + "timings": { + "type": "object", + "additionalProperties": false, + "required": [ + "clock", + "identity", + "parse_ns", + "reduction_ns", + "boolean_z3_ns", + "boolean_z3_verify_ns", + "reference_solve_ns", + "reference_verify_ns", + "optimized_solve_ns", + "optimized_verify_ns", + "wang_z3_ns", + "wang_z3_verify_ns", + "export_ns" + ], + "properties": { + "clock": {"const": "monotonic-perf-counter-ns"}, + "identity": {"const": "run-specific-observation-not-a-benchmark"}, + "parse_ns": {"$ref": "#/$defs/duration"}, + "reduction_ns": {"$ref": "#/$defs/duration"}, + "boolean_z3_ns": {"$ref": "#/$defs/duration"}, + "boolean_z3_verify_ns": {"$ref": "#/$defs/nullable_duration"}, + "reference_solve_ns": {"$ref": "#/$defs/duration"}, + "reference_verify_ns": {"$ref": "#/$defs/nullable_duration"}, + "optimized_solve_ns": {"$ref": "#/$defs/duration"}, + "optimized_verify_ns": {"$ref": "#/$defs/nullable_duration"}, + "wang_z3_ns": {"$ref": "#/$defs/duration"}, + "wang_z3_verify_ns": {"$ref": "#/$defs/nullable_duration"}, + "export_ns": {"$ref": "#/$defs/duration"} + } + }, + "artifacts": { + "type": "object", + "additionalProperties": false, + "required": [ + "source_input", + "formula_snapshot", + "tileset_snapshot", + "region_snapshot", + "provenance_snapshot", + "boolean_z3_summary", + "reference_trace_manifest", + "reference_trace", + "reference_solution", + "optimized_trace_manifest", + "optimized_trace", + "optimized_solution", + "wang_z3_summary", + "square_presentation", + "generalized_presentation", + "hex_presentation" + ], + "properties": { + "source_input": {"$ref": "#/$defs/artifact"}, + "formula_snapshot": {"$ref": "#/$defs/artifact"}, + "tileset_snapshot": {"$ref": "#/$defs/artifact"}, + "region_snapshot": {"$ref": "#/$defs/artifact"}, + "provenance_snapshot": {"$ref": "#/$defs/artifact"}, + "boolean_z3_summary": {"$ref": "#/$defs/artifact"}, + "reference_trace_manifest": {"$ref": "#/$defs/artifact"}, + "reference_trace": {"$ref": "#/$defs/artifact"}, + "reference_solution": {"$ref": "#/$defs/nullable_artifact"}, + "optimized_trace_manifest": {"$ref": "#/$defs/artifact"}, + "optimized_trace": {"$ref": "#/$defs/artifact"}, + "optimized_solution": {"$ref": "#/$defs/nullable_artifact"}, + "wang_z3_summary": {"$ref": "#/$defs/artifact"}, + "square_presentation": {"$ref": "#/$defs/nullable_artifact"}, + "generalized_presentation": {"$ref": "#/$defs/nullable_artifact"}, + "hex_presentation": {"$ref": "#/$defs/nullable_artifact"} + } + } + }, + "$defs": { + "sha256": {"type": "string", "pattern": "^[0-9a-f]{64}$"}, + "nullable_sha256": { + "oneOf": [{"$ref": "#/$defs/sha256"}, {"type": "null"}] + }, + "duration": {"type": "integer", "minimum": 0}, + "nullable_duration": { + "oneOf": [{"$ref": "#/$defs/duration"}, {"type": "null"}] + }, + "z3_configuration": { + "type": "object", + "additionalProperties": false, + "required": ["random_seed", "threads"], + "properties": { + "random_seed": {"const": 0}, + "threads": {"const": 1} + } + }, + "trace_configuration": { + "type": "object", + "additionalProperties": false, + "required": ["event_capacity", "checkpoint_interval", "checkpoint_capacity"], + "properties": { + "event_capacity": {"type": "integer", "minimum": 2, "maximum": 100000}, + "checkpoint_interval": {"type": "integer", "minimum": 0}, + "checkpoint_capacity": {"type": "integer", "minimum": 0} + } + }, + "trace_result": { + "type": "object", + "additionalProperties": false, + "required": [ + "solver", + "manifest_sha256", + "trace_sha256", + "complete", + "truncated", + "event_capacity", + "observed_event_count", + "checkpoint_interval", + "checkpoint_capacity", + "checkpoint_count", + "selection" + ], + "properties": { + "solver": {"enum": ["reference", "optimized"]}, + "manifest_sha256": {"$ref": "#/$defs/sha256"}, + "trace_sha256": {"$ref": "#/$defs/sha256"}, + "complete": {"const": true}, + "truncated": {"const": false}, + "event_capacity": {"type": "integer", "minimum": 2}, + "observed_event_count": {"type": "integer", "minimum": 2}, + "checkpoint_interval": {"type": "integer", "minimum": 0}, + "checkpoint_capacity": {"type": "integer", "minimum": 0}, + "checkpoint_count": {"type": "integer", "minimum": 0}, + "selection": { + "type": "object", + "additionalProperties": false, + "required": ["performed", "selected_event_count"], + "properties": { + "performed": {"type": "boolean"}, + "selected_event_count": { + "oneOf": [ + {"type": "integer", "minimum": 0}, + {"type": "null"} + ] + } + } + } + } + }, + "boolean_z3": { + "type": "object", + "additionalProperties": false, + "required": [ + "status", + "configuration", + "encoding_summary_sha256", + "assignment", + "witness_sha256" + ], + "properties": { + "status": {"enum": ["sat", "unsat"]}, + "configuration": {"$ref": "#/$defs/z3_configuration"}, + "encoding_summary_sha256": {"$ref": "#/$defs/sha256"}, + "assignment": { + "oneOf": [ + {"type": "array", "items": {"type": "boolean"}}, + {"type": "null"} + ] + }, + "witness_sha256": {"$ref": "#/$defs/nullable_sha256"} + } + }, + "wang_z3": { + "type": "object", + "additionalProperties": false, + "required": [ + "status", + "configuration", + "encoding_summary_sha256", + "cells", + "witness_sha256" + ], + "properties": { + "status": {"enum": ["sat", "unsat"]}, + "configuration": {"$ref": "#/$defs/z3_configuration"}, + "encoding_summary_sha256": {"$ref": "#/$defs/sha256"}, + "cells": { + "oneOf": [ + { + "type": "array", + "items": {"type": ["integer", "null"], "minimum": 0, "maximum": 22} + }, + {"type": "null"} + ] + }, + "witness_sha256": {"$ref": "#/$defs/nullable_sha256"} + } + }, + "native_engine": { + "type": "object", + "additionalProperties": false, + "required": [ + "status", + "configuration", + "trace", + "solution_sha256", + "witness_sha256", + "extracted_assignment" + ], + "properties": { + "status": {"enum": ["sat", "unsat"]}, + "configuration": {"$ref": "#/$defs/trace_configuration"}, + "trace": {"$ref": "#/$defs/trace_result"}, + "solution_sha256": {"$ref": "#/$defs/nullable_sha256"}, + "witness_sha256": {"$ref": "#/$defs/nullable_sha256"}, + "extracted_assignment": { + "oneOf": [ + {"type": "array", "items": {"type": "boolean"}}, + {"type": "null"} + ] + } + } + }, + "check": { + "type": "object", + "additionalProperties": false, + "required": ["checker", "performed", "passed", "witness_sha256"], + "properties": { + "checker": {"type": "string", "minLength": 1}, + "performed": {"type": "boolean"}, + "passed": {"type": ["boolean", "null"]}, + "witness_sha256": {"$ref": "#/$defs/nullable_sha256"} + } + }, + "presentation": { + "type": "object", + "additionalProperties": false, + "required": ["relationship", "applicable", "artifact"], + "properties": { + "relationship": {"type": "string", "minLength": 1}, + "applicable": {"type": "boolean"}, + "artifact": {"type": ["string", "null"]} + } + }, + "artifact": { + "type": "object", + "additionalProperties": false, + "required": [ + "path", + "sha256", + "media_type", + "schema", + "role", + "semantics", + "form", + "source_sha256" + ], + "properties": { + "path": {"type": "string", "pattern": "^assets/(?!.*(?:^|/)\\.\\.?/).+"}, + "sha256": {"$ref": "#/$defs/sha256"}, + "media_type": { + "enum": ["application/json", "text/plain", "image/png", "image/gif"] + }, + "schema": {"type": ["string", "null"]}, + "role": {"type": "string", "minLength": 1}, + "semantics": { + "enum": [ + "observed", + "canonical-construction", + "encoding-order", + "verified-transformation", + "didactic" + ] + }, + "form": {"enum": ["data", "static", "animated"]}, + "source_sha256": {"$ref": "#/$defs/sha256"} + } + }, + "nullable_artifact": { + "oneOf": [{"$ref": "#/$defs/artifact"}, {"type": "null"}] + } + } +} diff --git a/tests/python/test_multi_engine_dossier.py b/tests/python/test_multi_engine_dossier.py new file mode 100644 index 0000000..2a2c6b8 --- /dev/null +++ b/tests/python/test_multi_engine_dossier.py @@ -0,0 +1,398 @@ +from __future__ import annotations + +import copy +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +from dossier import multi_engine +from formats.pipeline_snapshot import PipelineSnapshotError +from formats.run_case_v2 import ( + CASE_SCHEMA, + load_run_case_v2, +) +from formats.run_dossier_v2 import ( + RUN_SCHEMA, + validate_run_dossier_v2, +) +from formats.run_dossier_v2_bundle import load_run_dossier_v2 +from native import multi_engine_pipeline +from native.multi_engine_pipeline import ( + TraceCaptureOptions, + capture_multi_engine_native_pipeline, +) +from oracles.witness_check import is_valid_assignment +from tools import generate_run_dossier as public_generator + + +ROOT = Path(__file__).resolve().parents[2] +SAT_CASE = ROOT / "examples/run-cases-v2/pipeline-sat.json" + + +def _unsat_case() -> dict[str, object]: + return { + "schema": CASE_SCHEMA, + "id": "pipeline-unsat-v2", + "title": "Full-pipeline UNSAT capture test", + "purpose": "Exercise the closed v2 UNSAT and not-applicable fields.", + "source": "tests/instances/pipeline_unsat_search.cm13", + "expected_status": "unsat", + "reference_trace": { + "event_capacity": 8192, + "checkpoint_interval": 128, + "checkpoint_capacity": 64, + }, + "optimized_trace": { + "event_capacity": 8192, + "checkpoint_interval": 128, + "checkpoint_capacity": 64, + }, + } + + +class MultiEngineDossierTests(unittest.TestCase): + @classmethod + def setUpClass(cls) -> None: + cls.temporary = tempfile.TemporaryDirectory() + cls.root = Path(cls.temporary.name) + cls.sat_directory = cls.root / "sat" + multi_engine.generate_multi_engine_dossier(SAT_CASE, cls.sat_directory) + cls.sat_document = load_run_dossier_v2(cls.sat_directory / "run.json") + + cls.unsat_case_path = cls.root / "unsat-case.json" + cls.unsat_case_path.write_text( + json.dumps(_unsat_case(), ensure_ascii=False) + "\n", + encoding="utf-8", + ) + cls.unsat_directory = cls.root / "unsat" + multi_engine.generate_multi_engine_dossier( + cls.unsat_case_path, + cls.unsat_directory, + ) + cls.unsat_document = load_run_dossier_v2( + cls.unsat_directory / "run.json" + ) + + @classmethod + def tearDownClass(cls) -> None: + cls.temporary.cleanup() + + def test_native_coordinator_runs_each_solver_once_in_one_capture(self) -> None: + case = load_run_case_v2(SAT_CASE, ROOT) + reference = TraceCaptureOptions( + case.reference_trace.event_capacity, + case.reference_trace.checkpoint_interval, + case.reference_trace.checkpoint_capacity, + ) + optimized = TraceCaptureOptions( + case.optimized_trace.event_capacity, + case.optimized_trace.checkpoint_interval, + case.optimized_trace.checkpoint_capacity, + ) + actual_solve = multi_engine_pipeline._solve_native_traced + actual_load = multi_engine_pipeline._loaded_formula + actual_reduce = multi_engine_pipeline._built_explained_reduction + with patch.object( + multi_engine_pipeline, + "_solve_native_traced", + wraps=actual_solve, + ) as solve, patch.object( + multi_engine_pipeline, + "_loaded_formula", + wraps=actual_load, + ) as load, patch.object( + multi_engine_pipeline, + "_built_explained_reduction", + wraps=actual_reduce, + ) as reduce: + capture = capture_multi_engine_native_pipeline( + ROOT / case.source, + reference_options=reference, + optimized_options=optimized, + ) + + self.assertEqual(load.call_count, 1) + self.assertEqual(reduce.call_count, 1) + self.assertEqual(solve.call_count, 2) + self.assertEqual( + [call.kwargs["optimized"] for call in solve.call_args_list], + [False, True], + ) + self.assertEqual(capture.reference.result.status.value, "sat") + self.assertEqual(capture.optimized.result.status.value, "sat") + self.assertFalse(capture.reference.trace.truncated) + self.assertFalse(capture.optimized.trace.truncated) + self.assertTrue( + is_valid_assignment( + capture.formula, + capture.reference.extracted_assignment or (), + ) + ) + self.assertTrue( + is_valid_assignment( + capture.formula, + capture.optimized.extracted_assignment or (), + ) + ) + + def test_sat_capture_binds_named_engines_and_shared_native_inputs(self) -> None: + document = self.sat_document + self.assertEqual(document["schema"], RUN_SCHEMA) + self.assertTrue(document["agreement"]["passed"]) + self.assertTrue(document["agreement"]["sat_witnesses_valid"]) + self.assertEqual( + { + document[name]["status"] + for name in ("boolean_z3", "reference", "optimized", "wang_z3") + }, + {"sat"}, + ) + self.assertNotEqual( + document["reference"]["trace"]["trace_sha256"], + document["optimized"]["trace"]["trace_sha256"], + ) + self.assertEqual( + document["reduction"]["region_sha256"], + document["artifacts"]["region_snapshot"]["sha256"], + ) + self.assertIsNone(document["presentation"]["square"]["artifact"]) + self.assertFalse((self.sat_directory / "report.tex").exists()) + self.assertFalse((self.sat_directory / "report.pdf").exists()) + + def test_unsat_capture_has_no_witness_or_fabricated_verification(self) -> None: + document = self.unsat_document + self.assertEqual( + { + document[name]["status"] + for name in ("boolean_z3", "reference", "optimized", "wang_z3") + }, + {"unsat"}, + ) + self.assertIsNone(document["agreement"]["sat_witnesses_valid"]) + self.assertIsNone(document["boolean_z3"]["assignment"]) + self.assertIsNone(document["wang_z3"]["cells"]) + self.assertIsNone(document["artifacts"]["reference_solution"]) + self.assertIsNone(document["artifacts"]["optimized_solution"]) + self.assertIsNone(document["timings"]["reference_verify_ns"]) + self.assertIsNone(document["timings"]["wang_z3_verify_ns"]) + for check in document["verification"].values(): + self.assertFalse(check["performed"]) + self.assertIsNone(check["passed"]) + self.assertIsNone(check["witness_sha256"]) + for presentation in document["presentation"].values(): + self.assertFalse(presentation["applicable"]) + self.assertIsNone(presentation["artifact"]) + + def test_case_contract_forbids_initial_domain_overrides(self) -> None: + invalid = json.loads(SAT_CASE.read_text(encoding="utf-8")) + invalid["initial_domain_overrides"] = [] + path = self.root / "invalid-overrides.json" + path.write_text(json.dumps(invalid) + "\n", encoding="utf-8") + with self.assertRaisesRegex(PipelineSnapshotError, "unknown fields"): + load_run_case_v2(path, ROOT) + + schema = json.loads( + (ROOT / "schemas/wang-run-case-v2.schema.json").read_text( + encoding="utf-8" + ) + ) + self.assertFalse(schema["additionalProperties"]) + self.assertNotIn("initial_domain_overrides", schema["properties"]) + + def test_public_generator_dispatch_preserves_the_v1_implementation(self) -> None: + v1_case = ROOT / "examples/run-cases/sat-end-to-end.json" + expected = self.root / "mock-v1" + with patch.object( + public_generator, + "_generate_run_dossier_v1", + return_value=expected, + ) as generate_v1: + actual = public_generator.generate_run_dossier( + v1_case, + expected, + tex_engine="pdflatex", + max_frames=7, + duration_ms=250, + ) + self.assertEqual(actual, expected) + generate_v1.assert_called_once_with( + v1_case, + expected, + tex_engine="pdflatex", + max_frames=7, + duration_ms=250, + ) + + v2_expected = self.root / "mock-v2" + with patch.object( + multi_engine, + "generate_multi_engine_dossier", + return_value=v2_expected, + ) as generate_v2: + v2_actual = public_generator.generate_run_dossier( + SAT_CASE, + v2_expected, + tex_engine="pdflatex", + ) + self.assertEqual(v2_actual, v2_expected) + generate_v2.assert_called_once_with(SAT_CASE, v2_expected) + with self.assertRaisesRegex( + public_generator.DossierGenerationError, + "v1-only", + ): + public_generator.generate_run_dossier( + SAT_CASE, + v2_expected, + tex_engine="xelatex", + ) + + def test_mismatch_and_cross_identity_mutations_are_rejected(self) -> None: + mismatch = copy.deepcopy(self.sat_document) + mismatch["wang_z3"]["status"] = "unsat" + mismatch["wang_z3"]["cells"] = None + mismatch["wang_z3"]["witness_sha256"] = None + with self.assertRaisesRegex(PipelineSnapshotError, "status mismatch"): + validate_run_dossier_v2(mismatch) + + identity = copy.deepcopy(self.sat_document) + identity["reduction"]["region_sha256"] = "0" * 64 + with self.assertRaisesRegex(PipelineSnapshotError, "cross-field mismatch"): + validate_run_dossier_v2(identity) + + unknown = copy.deepcopy(self.sat_document) + unknown["stages"] = [] + with self.assertRaisesRegex(PipelineSnapshotError, "unknown fields"): + validate_run_dossier_v2(unknown) + + def test_loader_rejects_tampering_and_external_symlinks(self) -> None: + tampered = self.root / "tampered" + shutil.copytree(self.sat_directory, tampered) + source = tampered / self.sat_document["artifacts"]["source_input"]["path"] + source.write_bytes(b"tampered\n") + with self.assertRaisesRegex(PipelineSnapshotError, "does not match file"): + load_run_dossier_v2(tampered / "run.json") + + escaped = self.root / "escaped" + shutil.copytree(self.sat_directory, escaped) + run_path = escaped / "run.json" + document = json.loads(run_path.read_text(encoding="utf-8")) + formula = escaped / document["artifacts"]["formula_snapshot"]["path"] + formula.unlink() + outside = self.root / "outside.json" + outside.write_text("{}\n", encoding="utf-8") + formula.symlink_to(outside) + with self.assertRaisesRegex(PipelineSnapshotError, "escapes dossier"): + load_run_dossier_v2(run_path) + + def test_bundle_loader_imports_no_capture_or_native_producer(self) -> None: + completed = subprocess.run( + [ + sys.executable, + "-c", + ( + "import sys; import formats.run_dossier_v2_bundle; " + "assert 'dossier.multi_engine' not in sys.modules; " + "assert 'native.multi_engine_pipeline' not in sys.modules" + ), + ], + cwd=ROOT, + env={**os.environ, "PYTHONPATH": "python"}, + check=False, + capture_output=True, + text=True, + ) + self.assertEqual(completed.returncode, 0, completed.stderr) + + def test_failure_cleanup_and_existing_destination_are_safe(self) -> None: + destination = self.root / "existing" + destination.mkdir() + sentinel = destination / "sentinel" + sentinel.write_text("keep\n", encoding="utf-8") + with self.assertRaisesRegex( + multi_engine.MultiEngineDossierError, + "already exists", + ): + multi_engine.generate_multi_engine_dossier(SAT_CASE, destination) + self.assertEqual(sentinel.read_text(encoding="utf-8"), "keep\n") + + failed = self.root / "failed" + before = set(self.root.glob(".failed.*")) + with patch.object( + multi_engine, + "capture_multi_engine_native_pipeline", + side_effect=RuntimeError("forced capture failure"), + ): + with self.assertRaisesRegex(RuntimeError, "forced capture failure"): + multi_engine.generate_multi_engine_dossier(SAT_CASE, failed) + self.assertFalse(failed.exists()) + self.assertEqual(set(self.root.glob(".failed.*")), before) + + actual_boolean = multi_engine.build_boolean_z3_summary + + def disagree(*args: object, **kwargs: object) -> dict[str, object]: + summary = actual_boolean(*args, **kwargs) + summary["status"] = "unsat" + summary["model"]["assignment"] = None + summary["statistics"][-1]["value"] = 0 + return summary + + mismatch = self.root / "mismatch" + before = set(self.root.glob(".mismatch.*")) + with patch.object( + multi_engine, + "build_boolean_z3_summary", + side_effect=disagree, + ): + with self.assertRaisesRegex(PipelineSnapshotError, "status mismatch"): + multi_engine.generate_multi_engine_dossier(SAT_CASE, mismatch) + self.assertFalse(mismatch.exists()) + self.assertEqual(set(self.root.glob(".mismatch.*")), before) + + def test_final_replace_failure_leaves_no_partial_destination(self) -> None: + destination = self.root / "replace-failed" + before = set(self.root.glob(".replace-failed.*")) + actual_boolean = multi_engine.build_boolean_z3_summary + actual_wang = multi_engine.build_wang_z3_summary + with patch.object( + multi_engine, + "_install_directory", + side_effect=OSError("forced replace failure"), + ), patch.object( + multi_engine, + "build_boolean_z3_summary", + wraps=actual_boolean, + ) as boolean, patch.object( + multi_engine, + "build_wang_z3_summary", + wraps=actual_wang, + ) as wang: + with self.assertRaisesRegex(OSError, "forced replace failure"): + multi_engine.generate_multi_engine_dossier(SAT_CASE, destination) + self.assertEqual(boolean.call_count, 1) + self.assertEqual(wang.call_count, 1) + self.assertFalse(destination.exists()) + self.assertEqual(set(self.root.glob(".replace-failed.*")), before) + + def test_v2_schemas_are_closed_draft_2020_12_documents(self) -> None: + for name, expected in ( + ("wang-run-case-v2.schema.json", CASE_SCHEMA), + ("wang-run-dossier-v2.schema.json", RUN_SCHEMA), + ): + with self.subTest(schema=name): + schema = json.loads((ROOT / "schemas" / name).read_text(encoding="utf-8")) + self.assertEqual( + schema["$schema"], + "https://json-schema.org/draft/2020-12/schema", + ) + self.assertEqual(schema["properties"]["schema"]["const"], expected) + self.assertFalse(schema["additionalProperties"]) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/generate_run_dossier.py b/tools/generate_run_dossier.py index db82355..1ea0226 100644 --- a/tools/generate_run_dossier.py +++ b/tools/generate_run_dossier.py @@ -22,7 +22,11 @@ TEMPLATE = ROOT / "templates/run-report.tex" sys.path.insert(0, str(ROOT / "python")) -from formats.pipeline_snapshot import _encode_document, _write_atomic # noqa: E402 +from formats.pipeline_snapshot import ( # noqa: E402 + _encode_document, + _load_json_bytes, + _write_atomic, +) from formats.run_dossier import ( # noqa: E402 RunCase, build_run_dossier, @@ -45,19 +49,19 @@ class DossierGenerationError(RuntimeError): def _parser() -> argparse.ArgumentParser: parser = argparse.ArgumentParser( description=( - "capture one versioned native run, reuse the offline renderers, and " - "compile a self-contained LaTeX/PDF dossier" + "dispatch one closed v1 or v2 case to its isolated self-contained " + "dossier implementation" ) ) - parser.add_argument("case", type=Path, help="wang-run-case-v1 JSON") + parser.add_argument("case", type=Path, help="wang-run-case-v1/v2 JSON") parser.add_argument("output_directory", type=Path) parser.add_argument( "--tex-engine", default="pdflatex", - help="pdfLaTeX executable (default: pdflatex)", + help="v1 pdfLaTeX executable (default: pdflatex)", ) - parser.add_argument("--max-frames", type=int, default=12) - parser.add_argument("--duration-ms", type=int, default=500) + parser.add_argument("--max-frames", type=int, default=12, help="v1 only") + parser.add_argument("--duration-ms", type=int, default=500, help="v1 only") return parser @@ -330,7 +334,7 @@ def _compile_pdf(dossier_root: Path, tex_engine: str, captured_at: datetime) -> shutil.rmtree(tex_home) -def generate_run_dossier( +def _generate_run_dossier_v1( case_path: str | Path, output_directory: str | Path, *, @@ -425,6 +429,53 @@ def generate_run_dossier( raise +def _case_schema(case_path: str | Path) -> str: + path = Path(case_path) + try: + document = _load_json_bytes(path.read_bytes(), str(path)) + except OSError as error: + raise DossierGenerationError(f"cannot read dossier case {path!s}: {error}") from error + schema = document.get("schema") + if type(schema) is not str: + raise DossierGenerationError("dossier case requires a string schema") + return schema + + +def generate_run_dossier( + case_path: str | Path, + output_directory: str | Path, + *, + tex_engine: str, + max_frames: int = 12, + duration_ms: int = 500, +) -> Path: + """Dispatch the sole public CLI without sharing v1/v2 implementations.""" + schema = _case_schema(case_path) + if schema == "wang-run-case-v1": + return _generate_run_dossier_v1( + case_path, + output_directory, + tex_engine=tex_engine, + max_frames=max_frames, + duration_ms=duration_ms, + ) + if schema == "wang-run-case-v2": + if tex_engine != "pdflatex" or max_frames != 12 or duration_ms != 500: + raise DossierGenerationError( + "renderer and TeX options are v1-only until the v2 asset/PDF passes" + ) + from dossier.multi_engine import ( + MultiEngineDossierError, + generate_multi_engine_dossier, + ) + + try: + return generate_multi_engine_dossier(case_path, output_directory) + except MultiEngineDossierError as error: + raise DossierGenerationError(str(error)) from error + raise DossierGenerationError(f"unsupported dossier case schema: {schema}") + + def main(arguments: list[str] | None = None) -> int: parser = _parser() args = parser.parse_args(arguments)