diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 78699e8..4126b3f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -74,6 +74,14 @@ jobs: working-directory: renderer run: uv run --locked pytest -q + - name: Install isolated report compiler + run: | + sudo apt-get update + sudo apt-get install --yes --no-install-recommends texlive-latex-base + + - name: Compile opt-in run dossier without shell escape + run: make run-dossier-smoke + strict-compilers: runs-on: ubuntu-latest diff --git a/Makefile b/Makefile index 7accdf2..8799b9d 100644 --- a/Makefile +++ b/Makefile @@ -89,7 +89,7 @@ OPENMP_LIBRARY := $(LIB_DIR)/libwang_openmp.a strict-check sanitizer-check analyzer-check valgrind-check \ cachegrind-check benchmark benchmark-smoke benchmark-compare \ benchmark-compare-smoke coverage coverage-c coverage-python \ - parser-fuzz parser-fuzz-smoke parser-fuzz-corpus clean + parser-fuzz parser-fuzz-smoke parser-fuzz-corpus run-dossier-smoke clean all: serial shared @@ -167,6 +167,16 @@ pages-check: generated-pages-check: $(PYTHON) tools/check_generated_pages.py $(PAGES_BUILD_DIR) +run-dossier-smoke: shared + $(RM) -r $(BUILD_DIR)/run-dossier-smoke + $(UV) run --frozen python tools/generate_run_dossier.py \ + examples/run-cases/unsat-root-conflict.json \ + $(BUILD_DIR)/run-dossier-smoke \ + --tex-engine pdflatex --max-frames 8 + test -s $(BUILD_DIR)/run-dossier-smoke/report.tex + test -s $(BUILD_DIR)/run-dossier-smoke/report.pdf + test -s $(BUILD_DIR)/run-dossier-smoke/run.json + c-check: serial $(C_TEST_BINS) @set -e; \ if [ -z "$(strip $(C_TEST_BINS))" ]; then \ diff --git a/README.md b/README.md index e3c0989..c09656f 100644 --- a/README.md +++ b/README.md @@ -76,6 +76,7 @@ solving remains future work. | Reduction construction provenance | Implemented as a separate opt-in native-owned result with exact signal orders, swap-bound gadget spans, manifest v2, and a square overlay view; the compact standard ABI does not allocate it | | 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 | | 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 | @@ -157,10 +158,8 @@ diagram. Planned work remains separated into independently reviewed changes. The new priority is explainability across the deterministic pipeline: -1. publish a compact formula-to-final-image gallery and optional technical - report from versioned examples; -2. resume serial MRV and hard-UNSAT evidence; -3. define `TaskPlan` only after the serial evidence, then implement and measure +1. resume serial MRV and hard-UNSAT evidence; +2. define `TaskPlan` only after the serial evidence, then implement and measure real OpenMP execution. The implementation follows a deliberately small design rule: each datum has one @@ -184,7 +183,7 @@ make check The imported renderer remains a separate locked Python project. Its Pillow and NumPy dependencies are not installed by the root project or exercised by -`make check`. Run its 253-test combined suite independently: +`make check`. Run its 262-test combined suite independently: ```sh cd renderer @@ -227,6 +226,9 @@ invariants, and the square-only construction overlay. The [solver event trace contract](docs/wang_solver_trace.md) defines bounded native capture, manifest v3, semantic replay, checkpoints, truncation, and the presentation-only animation boundary. +The [observed-run dossier contract](docs/run_dossiers.md) defines the four +versioned case classes, authoritative raw metadata, fixed TeX scaffolding, +asset reuse, atomic output, and UNSAT evidence boundary. To export one observed reference run and render selected replay states: @@ -247,6 +249,22 @@ uv run python tools/export_z3_encoding_summaries.py \ tests/instances/pipeline_sat.cm13 build/z3-summaries ``` +To generate one self-contained report outside the ordinary run path, provide +pdfLaTeX and select a versioned case explicitly: + +```sh +make shared +uv run --frozen python tools/generate_run_dossier.py \ + examples/run-cases/sat-end-to-end.json \ + build/run-dossiers/sat-end-to-end \ + --tex-engine pdflatex +``` + +The compiler is invoked without shell escape. `run.json` preserves raw stage +durations and hashes; the PDF reuses the validated trace frames and existing +square/hex renderers. TeX remains an opt-in CI/tooling dependency, not a root +Python dependency. + Useful individual targets: ```sh diff --git a/docs/run_dossiers.md b/docs/run_dossiers.md new file mode 100644 index 0000000..2d4383a --- /dev/null +++ b/docs/run_dossiers.md @@ -0,0 +1,96 @@ +--- +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. +section: Architecture and correctness +document_kind: Reproduction and report contract +status: Current implementation +updated: 2026-08-28 +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. + +`run.json` is the authoritative report input. It records the source and Git +identity, environment, solver options and result, complete trace counters, +initial-domain overrides, raw stage durations, replay scope, and SHA-256 for +every referenced JSON or raster asset. The LaTeX document and PDF are derived +from that one document. They do not recalculate events, witness state, timing, +or provenance. + +## Example index + +Four strict case documents are versioned. Their classification is checked +against the observed trace rather than trusted as prose. + +| Case | Configured result | Required observed shape | Case source | +| --- | --- | --- | --- | +| SAT end to end | SAT | complete trace, independently checked witness, square and checked hex views | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/sat-end-to-end.json) | +| Immediate root conflict | UNSAT | three events: root, initial conflict, result; no propagation or search | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-root-conflict.json) | +| Initial propagation contradiction | UNSAT | domain reductions and propagation reach an initial conflict before any decision | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-propagation.json) | +| Non-superficial search | UNSAT | complete depth-two run with four decisions, three conflicts, and four backtracks | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-search.json) | + +The first three cases use the same small formula so the observed boundary is +easy to compare. The two constrained UNSAT cases deliberately exercise the +public initial-domain option: their UNSAT status describes that configured +Wang solve, not the unconstrained source formula. The search case uses a +separate cubic monotone input whose unconstrained optimized run reaches depth +two before exhausting all branches. + +This page is only an index. The [solver trace contract]({{ '/wang-solver-trace/' | relative_url }}) +remains the canonical explanation of event semantics, truncation, replay, and +the existing animation assets. The [static snapshot contract]({{ '/wang-explainability-snapshots/' | relative_url }}) +defines formula and region views, while the [square-to-hex reference]({{ '/wang-square-to-hex/' | relative_url }}) +defines the presentation-only port. No animation, explanation, or generated +run narrative is copied here. + +## Reproduce one dossier + +Build the shared native library, provide pdfLaTeX, and run the sole generator: + +```sh +make shared +uv run --frozen python tools/generate_run_dossier.py \ + examples/run-cases/sat-end-to-end.json \ + build/run-dossiers/sat-end-to-end \ + --tex-engine pdflatex +``` + +The destination must not exist. Every intermediate is written below a sibling +staging directory, the trace bundle is validated before rendering, and the +completed directory is installed with one rename. A failed render or TeX +compile leaves no partial destination. + +The generator calls the isolated renderer through its locked environment. A +single replay composes the selected frames used for individual PNGs, the +contact sheet, and the optional GIF. The PDF embeds the already-produced +contact sheet and static square/hex PNGs; it never embeds viewer-dependent GIF +or video content. UNSAT reports contain region views rather than inventing a +solution. + +pdfLaTeX is invoked directly, never through a shell, with +`-no-shell-escape`, restricted input/output policy, a private TeX home, UTC, +and `SOURCE_DATE_EPOCH` derived from the recorded run time. The CI smoke +installs TeX only inside its disposable runner. TeX is not a runtime or root +Python dependency. + +## Timing and evidence boundary + +The monotonic durations for parse, region build, solve, export, render, and SAT +witness verification are raw evidence from one environment. They are excluded +from snapshot identity and are not performance gates. The native solver has no +Z3-style encoding stage, so `encoding` is explicitly recorded as not applicable +rather than reported as a fabricated zero-duration operation. Verification is +also explicitly not applicable to UNSAT runs because the trace is diagnostic, +not an independently checked certificate. + +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. diff --git a/docs/wang_solver_trace.md b/docs/wang_solver_trace.md index 5d9fd7c..f24605d 100644 --- a/docs/wang_solver_trace.md +++ b/docs/wang_solver_trace.md @@ -161,3 +161,8 @@ Z3 uses a different boundary. Its versioned summaries are explicitly labeled `encoding-order`, fix version, seed and thread count, and record the project-defined constraint order, returned result/model, and stable project-owned counts. They do not expose or infer Z3's internal search order. + +The [observed-run dossier index]({{ '/run-dossiers/' | relative_url }}) lists +the versioned SAT and UNSAT cases that reuse this trace and rendering chain in +an opt-in LaTeX/PDF report. It adds no second replay path and does not turn +UNSAT diagnostics into a proof certificate. diff --git a/examples/run-cases/sat-end-to-end.json b/examples/run-cases/sat-end-to-end.json new file mode 100644 index 0000000..3d37cc7 --- /dev/null +++ b/examples/run-cases/sat-end-to-end.json @@ -0,0 +1,16 @@ +{ + "schema": "wang-run-case-v1", + "id": "sat-end-to-end", + "title": "SAT formula-to-witness observed run", + "classification": "sat-end-to-end", + "description": "A complete optimized native run from a parsed CM13 formula through reduction, verified square witness, checked hex presentation, and selected replay frames.", + "source": "tests/instances/pipeline_sat.cm13", + "solver": "optimized", + "expected_status": "sat", + "trace": { + "event_capacity": 8192, + "checkpoint_interval": 128, + "checkpoint_capacity": 64 + }, + "initial_domain_overrides": [] +} diff --git a/examples/run-cases/unsat-propagation.json b/examples/run-cases/unsat-propagation.json new file mode 100644 index 0000000..9463351 --- /dev/null +++ b/examples/run-cases/unsat-propagation.json @@ -0,0 +1,21 @@ +{ + "schema": "wang-run-case-v1", + "id": "unsat-propagation", + "title": "UNSAT contradiction during initial propagation", + "classification": "unsat-propagation-contradiction", + "description": "An observed constrained solve whose locally valid singleton on active cell zero propagates to an empty domain before search begins.", + "source": "tests/instances/pipeline_sat.cm13", + "solver": "optimized", + "expected_status": "unsat", + "trace": { + "event_capacity": 8192, + "checkpoint_interval": 128, + "checkpoint_capacity": 64 + }, + "initial_domain_overrides": [ + { + "cell": 0, + "domain": 8 + } + ] +} diff --git a/examples/run-cases/unsat-root-conflict.json b/examples/run-cases/unsat-root-conflict.json new file mode 100644 index 0000000..eff87ff --- /dev/null +++ b/examples/run-cases/unsat-root-conflict.json @@ -0,0 +1,21 @@ +{ + "schema": "wang-run-case-v1", + "id": "unsat-root-conflict", + "title": "UNSAT immediate root conflict", + "classification": "unsat-root-conflict", + "description": "An observed constrained solve whose caller-supplied empty domain on active cell zero is rejected immediately in the initial phase.", + "source": "tests/instances/pipeline_sat.cm13", + "solver": "optimized", + "expected_status": "unsat", + "trace": { + "event_capacity": 8192, + "checkpoint_interval": 128, + "checkpoint_capacity": 64 + }, + "initial_domain_overrides": [ + { + "cell": 0, + "domain": 0 + } + ] +} diff --git a/examples/run-cases/unsat-search.json b/examples/run-cases/unsat-search.json new file mode 100644 index 0000000..8fd8011 --- /dev/null +++ b/examples/run-cases/unsat-search.json @@ -0,0 +1,16 @@ +{ + "schema": "wang-run-case-v1", + "id": "unsat-search", + "title": "UNSAT depth-two search with backtracking", + "classification": "unsat-non-superficial-search", + "description": "A complete optimized native run that survives initial propagation, reaches search depth two, and exhausts alternatives through multiple conflicts and backtracks.", + "source": "tests/instances/pipeline_unsat_search.cm13", + "solver": "optimized", + "expected_status": "unsat", + "trace": { + "event_capacity": 8192, + "checkpoint_interval": 128, + "checkpoint_capacity": 64 + }, + "initial_domain_overrides": [] +} diff --git a/python/formats/run_dossier.py b/python/formats/run_dossier.py new file mode 100644 index 0000000..a3ff085 --- /dev/null +++ b/python/formats/run_dossier.py @@ -0,0 +1,677 @@ +"""Closed case and run documents for opt-in, self-contained run dossiers.""" + +from __future__ import annotations + +from dataclasses import dataclass +import hashlib +from pathlib import Path, PurePosixPath +import re +from typing import Final + +from formats.pipeline_snapshot import ( + PipelineSnapshotError, + _load_json_bytes, + _require_array, + _require_exact_fields, + _require_integer, + _require_literal, + _require_object, + _require_sha256, + _require_string, +) +from model.region import Region +from model.solver_trace import DOMAIN_ALL, SolverTrace + + +CASE_SCHEMA: Final = "wang-run-case-v1" +RUN_SCHEMA: Final = "wang-run-dossier-v1" +CLASS_SAT: Final = "sat-end-to-end" +CLASS_ROOT_CONFLICT: Final = "unsat-root-conflict" +CLASS_PROPAGATION: Final = "unsat-propagation-contradiction" +CLASS_SEARCH: Final = "unsat-non-superficial-search" +CLASSIFICATIONS: Final = frozenset( + {CLASS_SAT, CLASS_ROOT_CONFLICT, CLASS_PROPAGATION, CLASS_SEARCH} +) +SOLVERS: Final = frozenset({"reference", "optimized"}) +STATUSES: Final = frozenset({"sat", "unsat"}) +STAGES: Final = ( + "parse", + "region_build", + "encoding", + "solve", + "verify", + "export", + "render", +) +_CASE_ID = re.compile(r"[a-z0-9]+(?:-[a-z0-9]+)*\Z") +_GIT_COMMIT = re.compile(r"[0-9a-f]{40}\Z") +_MEDIA_TYPES = frozenset({"application/json", "image/png", "image/gif"}) + + +@dataclass(frozen=True, slots=True) +class InitialDomainOverride: + cell: int + domain: int + + +@dataclass(frozen=True, slots=True) +class RunCase: + identifier: str + title: str + classification: str + description: str + source: str + solver: str + expected_status: str + event_capacity: int + checkpoint_interval: int + checkpoint_capacity: int + 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, ...], + path: str, +) -> None: + if classification in (CLASS_SAT, CLASS_SEARCH) and overrides: + raise PipelineSnapshotError(f"{path}: this case class forbids overrides") + if classification == CLASS_ROOT_CONFLICT and not ( + len(overrides) == 1 and overrides[0].domain == 0 + ): + raise PipelineSnapshotError( + f"{path}: root conflict requires one empty active-cell domain" + ) + if classification == CLASS_PROPAGATION and not ( + len(overrides) == 1 + and overrides[0].domain > 0 + and overrides[0].domain & (overrides[0].domain - 1) == 0 + ): + raise PipelineSnapshotError( + f"{path}: propagation contradiction requires one singleton domain" + ) + + +def load_run_case(path: str | Path, repository_root: str | Path) -> RunCase: + """Load one strict, repository-relative dossier case.""" + 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 case {case_path!s}: {error}") from error + _require_exact_fields( + document, + frozenset( + { + "schema", + "id", + "title", + "classification", + "description", + "source", + "solver", + "expected_status", + "trace", + "initial_domain_overrides", + } + ), + "$", + ) + _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") + classification = _nonempty_string(document["classification"], "$.classification") + if classification not in CLASSIFICATIONS: + raise PipelineSnapshotError("$.classification: is not a dossier case class") + description = _nonempty_string(document["description"], "$.description") + source = _relative_path(document["source"], "$.source") + if not source.endswith(".cm13"): + raise PipelineSnapshotError("$.source: must name a .cm13 input") + source_path = Path(repository_root) / source + if not source_path.is_file(): + raise PipelineSnapshotError(f"$.source: repository input does not exist: {source}") + solver = _nonempty_string(document["solver"], "$.solver") + if solver not in SOLVERS: + raise PipelineSnapshotError("$.solver: is not a native traced solver") + expected_status = _nonempty_string(document["expected_status"], "$.expected_status") + if expected_status not in STATUSES: + raise PipelineSnapshotError("$.expected_status: must equal sat or unsat") + if (classification == CLASS_SAT) != (expected_status == "sat"): + raise PipelineSnapshotError("$.expected_status: disagrees with classification") + + trace = _require_object(document["trace"], "$.trace") + _require_exact_fields( + trace, + frozenset({"event_capacity", "checkpoint_interval", "checkpoint_capacity"}), + "$.trace", + ) + event_capacity = _require_integer( + trace["event_capacity"], "$.trace.event_capacity", nonnegative=True + ) + checkpoint_interval = _require_integer( + trace["checkpoint_interval"], + "$.trace.checkpoint_interval", + nonnegative=True, + ) + checkpoint_capacity = _require_integer( + trace["checkpoint_capacity"], + "$.trace.checkpoint_capacity", + nonnegative=True, + ) + if not 2 <= event_capacity <= 100_000: + raise PipelineSnapshotError("$.trace.event_capacity: must be in [2, 100000]") + if (checkpoint_interval == 0) != (checkpoint_capacity == 0): + raise PipelineSnapshotError( + "$.trace: checkpoint interval and capacity must be jointly set" + ) + + overrides: list[InitialDomainOverride] = [] + cells: set[int] = set() + for index, raw in enumerate( + _require_array(document["initial_domain_overrides"], "$.initial_domain_overrides") + ): + item_path = f"$.initial_domain_overrides[{index}]" + item = _require_object(raw, item_path) + _require_exact_fields(item, frozenset({"cell", "domain"}), item_path) + cell = _require_integer(item["cell"], f"{item_path}.cell", nonnegative=True) + domain = _require_integer( + item["domain"], f"{item_path}.domain", nonnegative=True + ) + if domain > DOMAIN_ALL: + raise PipelineSnapshotError(f"{item_path}.domain: is not a Wang domain") + if cell in cells: + raise PipelineSnapshotError(f"{item_path}.cell: duplicates an override") + cells.add(cell) + overrides.append(InitialDomainOverride(cell=cell, domain=domain)) + if tuple(item.cell for item in overrides) != tuple(sorted(cells)): + raise PipelineSnapshotError("$.initial_domain_overrides: must be cell-sorted") + parsed_overrides = tuple(overrides) + _validate_case_override_shape( + classification, + parsed_overrides, + "$.initial_domain_overrides", + ) + + return RunCase( + identifier=identifier, + title=title, + classification=classification, + description=description, + source=source, + solver=solver, + expected_status=expected_status, + event_capacity=event_capacity, + checkpoint_interval=checkpoint_interval, + checkpoint_capacity=checkpoint_capacity, + initial_domain_overrides=parsed_overrides, + ) + + +def initial_domains_for_case(case: RunCase, region: Region) -> tuple[int, ...] | None: + """Expand sparse case overrides to the public dense solver option.""" + if not isinstance(case, RunCase): + raise TypeError("case must be a RunCase") + if not isinstance(region, Region): + raise TypeError("region must be a Region") + if not case.initial_domain_overrides: + return None + domains = [DOMAIN_ALL if active else 0 for active in region.active] + for override in case.initial_domain_overrides: + if override.cell >= len(domains): + raise PipelineSnapshotError("initial domain override lies outside region") + if not region.active[override.cell]: + raise PipelineSnapshotError("initial domain override targets an inactive cell") + domains[override.cell] = override.domain + return tuple(domains) + + +def validate_case_outcome(case: RunCase, trace: SolverTrace) -> None: + """Prove that an observed trace has the case class claimed by its input.""" + if trace.solver != case.solver: + raise PipelineSnapshotError("observed trace solver disagrees with case") + if trace.status.value != case.expected_status: + raise PipelineSnapshotError("observed trace status disagrees with case") + if trace.truncated: + raise PipelineSnapshotError("versioned dossier cases require a complete trace") + events = trace.events + counts = {kind: sum(event.kind == kind for event in events) for kind in ( + "decision", "domain_reduction", "propagation", "conflict", "backtrack" + )} + maximum_depth = max(event.depth for event in events) + conflicts = tuple(event for event in events if event.kind == "conflict") + if case.classification == CLASS_SAT: + if trace.status.value != "sat": + raise PipelineSnapshotError("SAT case did not produce SAT") + return + if not conflicts: + raise PipelineSnapshotError("UNSAT case did not record a conflict") + if case.classification == CLASS_ROOT_CONFLICT: + if not ( + len(events) == 3 + and conflicts[0].phase == "initial" + and counts["domain_reduction"] == 0 + and counts["decision"] == 0 + and counts["backtrack"] == 0 + and maximum_depth == 0 + ): + raise PipelineSnapshotError("trace is not an immediate root conflict") + elif case.classification == CLASS_PROPAGATION: + if not ( + conflicts[-1].phase == "initial" + and counts["domain_reduction"] > 0 + and counts["propagation"] > 0 + and counts["decision"] == 0 + and counts["backtrack"] == 0 + and maximum_depth == 0 + ): + raise PipelineSnapshotError("trace is not an initial propagation contradiction") + elif case.classification == CLASS_SEARCH and not ( + conflicts[-1].phase == "search" + and counts["decision"] >= 4 + and counts["backtrack"] >= 4 + and maximum_depth >= 2 + ): + raise PipelineSnapshotError("trace is not a non-superficial UNSAT search") + + +def validate_run_dossier(document: object) -> None: + """Validate one closed run.json transport document.""" + root = _require_object(document, "$") + _require_exact_fields( + root, + frozenset({"schema", "case", "source", "environment", "solver", "timings", "artifacts"}), + "$", + ) + _require_literal(root["schema"], RUN_SCHEMA, "$.schema") + case = _require_object(root["case"], "$.case") + _require_exact_fields( + case, + frozenset({"id", "title", "classification", "description"}), + "$.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") + classification = _nonempty_string(case["classification"], "$.case.classification") + if classification not in CLASSIFICATIONS: + raise PipelineSnapshotError("$.case.classification: is invalid") + _nonempty_string(case["description"], "$.case.description") + + source = _require_object(root["source"], "$.source") + _require_exact_fields(source, frozenset({"path", "sha256"}), "$.source") + source_path = _relative_path(source["path"], "$.source.path") + if not source_path.endswith(".cm13"): + raise PipelineSnapshotError("$.source.path: must name a .cm13 input") + _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") + + solver = _require_object(root["solver"], "$.solver") + _require_exact_fields( + solver, + frozenset( + { + "engine", + "semantics", + "status", + "expected_status", + "initial_domain_overrides", + "trace", + "replay", + } + ), + "$.solver", + ) + engine = _nonempty_string(solver["engine"], "$.solver.engine") + if engine not in SOLVERS: + raise PipelineSnapshotError("$.solver.engine: is invalid") + _require_literal(solver["semantics"], "observed", "$.solver.semantics") + status = _nonempty_string(solver["status"], "$.solver.status") + expected_status = _nonempty_string(solver["expected_status"], "$.solver.expected_status") + if status not in STATUSES or status != expected_status: + raise PipelineSnapshotError("$.solver.status: must match the expected status") + if (classification == CLASS_SAT) != (status == "sat"): + raise PipelineSnapshotError("$.solver.status: disagrees with case classification") + overrides = _require_array( + solver["initial_domain_overrides"], "$.solver.initial_domain_overrides" + ) + parsed_overrides: list[InitialDomainOverride] = [] + previous_cell = -1 + for index, raw in enumerate(overrides): + item_path = f"$.solver.initial_domain_overrides[{index}]" + item = _require_object(raw, item_path) + _require_exact_fields(item, frozenset({"cell", "domain"}), item_path) + cell = _require_integer(item["cell"], f"{item_path}.cell", nonnegative=True) + domain = _require_integer(item["domain"], f"{item_path}.domain", nonnegative=True) + if cell <= previous_cell or domain > DOMAIN_ALL: + raise PipelineSnapshotError(f"{item_path}: overrides must be sorted and canonical") + parsed_overrides.append(InitialDomainOverride(cell=cell, domain=domain)) + previous_cell = cell + _validate_case_override_shape( + classification, + tuple(parsed_overrides), + "$.solver.initial_domain_overrides", + ) + + trace = _require_object(solver["trace"], "$.solver.trace") + _require_exact_fields( + trace, + frozenset( + { + "event_capacity", + "observed_event_count", + "truncated", + "checkpoint_interval", + "checkpoint_capacity", + "checkpoint_count", + "event_counts", + "max_depth", + } + ), + "$.solver.trace", + ) + event_capacity = _require_integer( + trace["event_capacity"], "$.solver.trace.event_capacity", nonnegative=True + ) + observed = _require_integer( + trace["observed_event_count"], + "$.solver.trace.observed_event_count", + nonnegative=True, + ) + truncated = _boolean(trace["truncated"], "$.solver.trace.truncated") + if truncated: + raise PipelineSnapshotError("$.solver.trace.truncated: dossier v1 requires a complete trace") + if event_capacity < 2 or observed < 2 or observed > event_capacity: + raise PipelineSnapshotError("$.solver.trace: event capacity is inconsistent") + checkpoint_interval = _require_integer( + trace["checkpoint_interval"], + "$.solver.trace.checkpoint_interval", + nonnegative=True, + ) + checkpoint_capacity = _require_integer( + trace["checkpoint_capacity"], + "$.solver.trace.checkpoint_capacity", + nonnegative=True, + ) + checkpoint_count = _require_integer( + trace["checkpoint_count"], + "$.solver.trace.checkpoint_count", + nonnegative=True, + ) + if (checkpoint_interval == 0) != (checkpoint_capacity == 0) or checkpoint_count > checkpoint_capacity: + raise PipelineSnapshotError("$.solver.trace: checkpoint metadata is inconsistent") + event_counts = _require_object(trace["event_counts"], "$.solver.trace.event_counts") + _require_exact_fields( + event_counts, + frozenset({"root", "propagation", "decision", "domain_reduction", "conflict", "backtrack", "result"}), + "$.solver.trace.event_counts", + ) + parsed_counts = { + name: _require_integer(value, f"$.solver.trace.event_counts.{name}", nonnegative=True) + for name, value in event_counts.items() + } + if parsed_counts["root"] != 1 or parsed_counts["result"] != 1: + raise PipelineSnapshotError("$.solver.trace.event_counts: requires one root and result") + if not truncated and sum(parsed_counts.values()) != observed: + raise PipelineSnapshotError("$.solver.trace.event_counts: does not total observed events") + maximum_depth = _require_integer(trace["max_depth"], "$.solver.trace.max_depth", nonnegative=True) + + replay = _require_object(solver["replay"], "$.solver.replay") + _require_exact_fields( + replay, + frozenset({"trace_scope", "frame_scope", "unsat_certificate"}), + "$.solver.replay", + ) + _require_literal(replay["trace_scope"], "complete", "$.solver.replay.trace_scope") + _require_literal(replay["frame_scope"], "selected", "$.solver.replay.frame_scope") + if _boolean(replay["unsat_certificate"], "$.solver.replay.unsat_certificate"): + raise PipelineSnapshotError("$.solver.replay.unsat_certificate: must remain false") + if classification == CLASS_ROOT_CONFLICT and not ( + maximum_depth == 0 + and observed == 3 + and parsed_counts["conflict"] == 1 + and parsed_counts["propagation"] == 0 + and parsed_counts["domain_reduction"] == 0 + and parsed_counts["decision"] == 0 + and parsed_counts["backtrack"] == 0 + ): + raise PipelineSnapshotError("$.solver.trace: does not describe a root conflict") + if classification == CLASS_PROPAGATION and not ( + maximum_depth == 0 + and parsed_counts["conflict"] >= 1 + and parsed_counts["domain_reduction"] > 0 + and parsed_counts["propagation"] > 0 + and parsed_counts["decision"] == 0 + and parsed_counts["backtrack"] == 0 + ): + raise PipelineSnapshotError("$.solver.trace: does not describe propagation UNSAT") + if classification == CLASS_SEARCH and not ( + maximum_depth >= 2 + and parsed_counts["conflict"] >= 1 + and parsed_counts["decision"] >= 4 + and parsed_counts["backtrack"] >= 4 + ): + raise PipelineSnapshotError("$.solver.trace: does not describe non-superficial search") + + timings = _require_object(root["timings"], "$.timings") + _require_exact_fields( + timings, + frozenset({"clock", "identity", "stages"}), + "$.timings", + ) + _require_literal(timings["clock"], "monotonic-perf-counter-ns", "$.timings.clock") + _require_literal( + timings["identity"], + "environment-specific-observation", + "$.timings.identity", + ) + stages = _require_array(timings["stages"], "$.timings.stages") + names: list[str] = [] + for index, raw in enumerate(stages): + item_path = f"$.timings.stages[{index}]" + stage = _require_object(raw, item_path) + _require_exact_fields(stage, frozenset({"name", "performed", "elapsed_ns"}), item_path) + name = _nonempty_string(stage["name"], f"{item_path}.name") + performed = _boolean(stage["performed"], f"{item_path}.performed") + elapsed = _nullable_integer(stage["elapsed_ns"], f"{item_path}.elapsed_ns") + if performed != (elapsed is not None): + raise PipelineSnapshotError(f"{item_path}: performed must match elapsed_ns") + names.append(name) + if tuple(names) != STAGES: + raise PipelineSnapshotError("$.timings.stages: order does not match the run contract") + if stages[2]["performed"] is not False: + raise PipelineSnapshotError("$.timings.stages[2]: native encoding must be not applicable") + expected_verify = status == "sat" + if stages[4]["performed"] is not expected_verify: + expectation = "performed for SAT" if expected_verify else "not applicable for UNSAT" + raise PipelineSnapshotError(f"$.timings.stages[4]: verify must be {expectation}") + + artifacts = _require_object(root["artifacts"], "$.artifacts") + required = {"trace_manifest", "formula_view", "region_square", "region_hex", "reduction_view", "trace_contact_sheet", "trace_fallback", "trace_animation"} + if not required.issubset(artifacts): + missing = ", ".join(sorted(required - artifacts.keys())) + raise PipelineSnapshotError(f"$.artifacts: missing required artifacts: {missing}") + if status == "sat" and not {"solution_square", "solution_hex"}.issubset(artifacts): + raise PipelineSnapshotError("$.artifacts: SAT dossier requires square and hex solutions") + if status == "unsat" and ({"solution_square", "solution_hex"} & artifacts.keys()): + raise PipelineSnapshotError("$.artifacts: UNSAT dossier forbids solution images") + referenced_paths: set[str] = set() + for name, raw in artifacts.items(): + if _CASE_ID.fullmatch(name.replace("_", "-")) is None: + raise PipelineSnapshotError(f"$.artifacts.{name}: invalid artifact key") + item_path = f"$.artifacts.{name}" + item = _require_object(raw, item_path) + _require_exact_fields(item, frozenset({"path", "sha256", "media_type", "role"}), item_path) + artifact_path = _relative_path(item["path"], f"{item_path}.path", prefix="assets") + if artifact_path in referenced_paths: + raise PipelineSnapshotError(f"{item_path}.path: duplicates another artifact") + referenced_paths.add(artifact_path) + _require_sha256(item["sha256"], f"{item_path}.sha256") + media_type = _nonempty_string(item["media_type"], f"{item_path}.media_type") + if media_type not in _MEDIA_TYPES: + raise PipelineSnapshotError(f"{item_path}.media_type: is unsupported") + _nonempty_string(item["role"], f"{item_path}.role") + + +def load_run_dossier(path: str | Path) -> dict[str, object]: + """Load run.json and verify every referenced asset without producer imports.""" + 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 run dossier {run_path!s}: {error}") from error + validate_run_dossier(document) + artifacts = _require_object(document["artifacts"], "$.artifacts") + try: + dossier_root = run_path.parent.resolve(strict=True) + except OSError as error: + raise PipelineSnapshotError(f"cannot resolve dossier root: {error}") from error + for name, raw in artifacts.items(): + item = _require_object(raw, f"$.artifacts.{name}") + relative = _relative_path( + item["path"], f"$.artifacts.{name}.path", prefix="assets" + ) + artifact_path = run_path.parent / relative + try: + resolved = artifact_path.resolve(strict=True) + if not resolved.is_relative_to(dossier_root) or not resolved.is_file(): + raise PipelineSnapshotError( + f"$.artifacts.{name}.path: escapes the self-contained dossier" + ) + encoded = resolved.read_bytes() + except OSError as error: + raise PipelineSnapshotError( + f"$.artifacts.{name}.path: cannot read {relative}: {error}" + ) from error + if hashlib.sha256(encoded).hexdigest() != item["sha256"]: + raise PipelineSnapshotError( + f"$.artifacts.{name}.sha256: does not match {relative}" + ) + return document + + +def build_run_dossier( + case: RunCase, + trace: SolverTrace, + *, + source_sha256: str, + captured_at_utc: str, + platform: str, + python_version: str, + git_commit: str, + timings_ns: dict[str, int | None], + artifacts: dict[str, dict[str, str]], +) -> dict[str, object]: + """Build and validate the raw authoritative run.json document.""" + validate_case_outcome(case, trace) + event_counts = { + kind: sum(event.kind == kind for event in trace.events) + for kind in ("root", "propagation", "decision", "domain_reduction", "conflict", "backtrack", "result") + } + document: dict[str, object] = { + "schema": RUN_SCHEMA, + "case": { + "id": case.identifier, + "title": case.title, + "classification": case.classification, + "description": case.description, + }, + "source": {"path": case.source, "sha256": source_sha256}, + "environment": { + "captured_at_utc": captured_at_utc, + "platform": platform, + "python": python_version, + "git_commit": git_commit, + }, + "solver": { + "engine": trace.solver, + "semantics": "observed", + "status": trace.status.value, + "expected_status": case.expected_status, + "initial_domain_overrides": [ + {"cell": item.cell, "domain": item.domain} + for item in case.initial_domain_overrides + ], + "trace": { + "event_capacity": trace.event_capacity, + "observed_event_count": trace.observed_event_count, + "truncated": trace.truncated, + "checkpoint_interval": trace.checkpoint_interval, + "checkpoint_capacity": trace.checkpoint_capacity, + "checkpoint_count": len(trace.checkpoints), + "event_counts": event_counts, + "max_depth": max(event.depth for event in trace.events), + }, + "replay": { + "trace_scope": "truncated-prefix" if trace.truncated else "complete", + "frame_scope": "selected", + "unsat_certificate": False, + }, + }, + "timings": { + "clock": "monotonic-perf-counter-ns", + "identity": "environment-specific-observation", + "stages": [ + { + "name": name, + "performed": timings_ns[name] is not None, + "elapsed_ns": timings_ns[name], + } + for name in STAGES + ], + }, + "artifacts": artifacts, + } + validate_run_dossier(document) + return document diff --git a/python/formats/run_report_tex.py b/python/formats/run_report_tex.py new file mode 100644 index 0000000..c2a7691 --- /dev/null +++ b/python/formats/run_report_tex.py @@ -0,0 +1,235 @@ +"""Fixed LaTeX scaffolding for a validated run dossier.""" + +from __future__ import annotations + +from typing import Final + +from formats.run_dossier import ( + CLASS_PROPAGATION, + CLASS_ROOT_CONFLICT, + CLASS_SAT, + CLASS_SEARCH, + validate_run_dossier, +) + + +_DIAGNOSIS: Final = { + CLASS_SAT: ( + "The native solver returned SAT, the independent Python checker accepted " + "the copied witness, and the square and hex images derive from that same " + "hash-bound solution." + ), + CLASS_ROOT_CONFLICT: ( + "A caller-supplied empty domain on an active cell was observed as an " + "immediate initial-phase conflict. No propagation, decision, or " + "backtracking step was needed." + ), + CLASS_PROPAGATION: ( + "A caller-supplied singleton was locally well formed but incompatible with " + "the region. Initial arc propagation reduced domains until it observed an " + "empty active-cell domain, before search began." + ), + CLASS_SEARCH: ( + "Initial propagation did not decide the instance. The observed solver run " + "entered depth-two search and exhausted alternatives through multiple " + "decisions, conflicts, and backtracks before returning UNSAT." + ), +} + + +def _tex(value: object) -> str: + text = str(value).replace("\u00a0", " ") + text = text.replace("–", "--").replace("—", "---").replace("→", " to ") + replacements = { + "\\": r"\textbackslash{}", + "{": r"\{", + "}": r"\}", + "$": r"\$", + "&": r"\&", + "#": r"\#", + "_": r"\_", + "%": r"\%", + "~": r"\textasciitilde{}", + "^": r"\textasciicircum{}", + } + return "".join(replacements.get(character, character) for character in text) + + +def _image(path: str, caption: str) -> str: + return "\n".join( + ( + r"\begin{figure}[htbp]", + r"\centering", + rf"\includegraphics[width=\textwidth,height=0.42\textheight,keepaspectratio]{{{path}}}", + rf"\caption{{{_tex(caption)}}}", + r"\end{figure}", + ) + ) + + +def render_run_report_tex(document: dict[str, object], template: str) -> str: + """Render the sole fixed report representation from validated run.json data.""" + validate_run_dossier(document) + if template.count("@@TITLE@@") != 1 or template.count("@@BODY@@") != 1: + raise ValueError("report template must contain one title and one body marker") + + case = document["case"] + source = document["source"] + environment = document["environment"] + solver = document["solver"] + timings = document["timings"] + artifacts = document["artifacts"] + assert isinstance(case, dict) + assert isinstance(source, dict) + assert isinstance(environment, dict) + assert isinstance(solver, dict) + assert isinstance(timings, dict) + assert isinstance(artifacts, dict) + trace = solver["trace"] + replay = solver["replay"] + assert isinstance(trace, dict) + assert isinstance(replay, dict) + counts = trace["event_counts"] + assert isinstance(counts, dict) + + timing_rows: list[str] = [] + for stage in timings["stages"]: + assert isinstance(stage, dict) + elapsed = stage["elapsed_ns"] + value = "not applicable" if elapsed is None else f"{elapsed / 1_000_000:.3f} ms ({elapsed} ns)" + timing_rows.append(rf"{_tex(stage['name'])} & {_tex(value)} \\") + + event_rows = [ + rf"{_tex(name)} & {value} \\" + for name, value in counts.items() + ] + override_rows = [ + rf"cell {_tex(item['cell'])}: domain {_tex(item['domain'])}" + for item in solver["initial_domain_overrides"] + ] + override_text = ", ".join(override_rows) if override_rows else "none" + + artifact_rows = [ + rf"{_tex(name)} & \texttt{{{_tex(item['sha256'])}}} \\" + for name, item in artifacts.items() + if str(item["media_type"]) == "application/json" + ] + + figures = [ + _image( + artifacts["formula_view"]["path"], + "Parsed formula snapshot used by this run.", + ), + _image( + artifacts["region_square"]["path"], + "Unassigned square region and boundary constraints.", + ), + _image( + artifacts["region_hex"]["path"], + "Presentation-only Basire/Culik hex port of the same square region.", + ), + _image( + artifacts["reduction_view"]["path"], + "Native Yang--Zhang reduction provenance for the constructed region.", + ), + _image( + artifacts["trace_contact_sheet"]["path"], + "Selected states from one replay of the observed semantic trace.", + ), + ] + if solver["status"] == "sat": + figures.extend( + ( + _image( + artifacts["solution_square"]["path"], + "Verified square witness with explainability overlays.", + ), + _image( + artifacts["solution_hex"]["path"], + "Checked presentation-only hex port of the same witness.", + ), + ) + ) + + body = "\n".join( + ( + r"\section{Run identity}", + _tex(case["description"]), + "", + r"\begin{tabular}{@{}>{\bfseries}p{0.28\textwidth}p{0.64\textwidth}@{}}", + rf"Case & {_tex(case['id'])} \\", + rf"Classification & {_tex(case['classification'])} \\", + rf"Source & {_tex(source['path'])} \\", + rf"Source SHA-256 & {{\scriptsize\texttt{{{_tex(source['sha256'])}}}}} \\", + rf"Git commit & \texttt{{{_tex(environment['git_commit'])}}} \\", + rf"Captured & {_tex(environment['captured_at_utc'])} \\", + rf"Platform & {{\small {_tex(environment['platform'])}}} \\", + rf"Python & {_tex(environment['python'])} \\", + r"\end{tabular}", + "", + r"\section{Pipeline and result}", + r"\begin{tabular}{@{}>{\bfseries}p{0.28\textwidth}p{0.64\textwidth}@{}}", + rf"Native solver & {_tex(solver['engine'])} \\", + rf"Semantics & {_tex(solver['semantics'])} \\", + rf"Status & {_tex(solver['status'])} \\", + rf"Initial-domain overrides & {_tex(override_text)} \\", + rf"Event capacity & {_tex(trace['event_capacity'])} \\", + rf"Trace truncated & {_tex(trace['truncated'])} \\", + rf"Checkpoint interval & {_tex(trace['checkpoint_interval'])} \\", + rf"Checkpoint capacity & {_tex(trace['checkpoint_capacity'])} \\", + rf"Observed checkpoints & {_tex(trace['checkpoint_count'])} \\", + rf"Trace scope & {_tex(replay['trace_scope'])} \\", + rf"Frame scope & {_tex(replay['frame_scope'])} \\", + rf"UNSAT certificate & {_tex(replay['unsat_certificate'])} \\", + r"\end{tabular}", + "", + _tex(_DIAGNOSIS[str(case["classification"])]), + "", + ( + "For UNSAT runs, the trail and conflicts are diagnostics from this " + "observed execution; they are not a mathematical UNSAT certificate." + if solver["status"] == "unsat" + else "The renderer is presentation only; witness correctness remains upstream." + ), + "", + r"\subsection{Observed trace counts}", + r"\begin{tabular}{lr}", + *event_rows, + rf"maximum depth & {_tex(trace['max_depth'])} \\", + rf"observed events & {_tex(trace['observed_event_count'])} \\", + r"\end{tabular}", + "", + r"\section{Stage timings}", + ( + "Durations are raw measurements of this environment and execution. " + "They are excluded from deterministic snapshot identity. Native Wang " + "solving has no separate Z3-style encoding phase, so encoding is " + "reported as not applicable rather than fabricated as zero." + ), + "", + r"\begin{tabular}{ll}", + *timing_rows, + r"\end{tabular}", + "", + r"\section{Hash-bound JSON inputs}", + r"\scriptsize", + r"\begin{tabular}{p{0.25\textwidth}p{0.68\textwidth}}", + *artifact_rows, + r"\end{tabular}", + r"\normalsize", + "", + r"\section{Visual evidence}", + *figures, + r"\clearpage", + r"\section{Reproduction boundary}", + ( + "run.json is the authoritative record for this dossier. The trace " + "manifest and content-addressed JSON documents are validated before " + "rendering. Frames are composed once by the existing replay renderer; " + "this PDF reuses selected PNGs and embeds neither GIF nor video. The " + "LaTeX compiler is invoked without shell escape." + ), + ) + ) + title = _tex(case["title"]) + return template.replace("@@TITLE@@", title).replace("@@BODY@@", body) diff --git a/python/native/solver_trace_adapter.py b/python/native/solver_trace_adapter.py index 3a50646..ac8c136 100644 --- a/python/native/solver_trace_adapter.py +++ b/python/native/solver_trace_adapter.py @@ -2,6 +2,7 @@ from __future__ import annotations +from collections.abc import Sequence from ctypes import ( CDLL, POINTER, @@ -17,6 +18,7 @@ from model.region import Region from model.solver_trace import ( + DOMAIN_ALL, SOLVER_OPTIMIZED, SOLVER_REFERENCE, TRACE_BACKTRACK, @@ -243,6 +245,7 @@ def _solve_native_traced( event_capacity: int, checkpoint_interval: int, checkpoint_capacity: int, + initial_domains: Sequence[int] | None = None, ) -> tuple[TilingSolveResult, SolverTrace]: """Run one traced solve and copy all caller-owned native storage.""" for name, value in ( @@ -259,6 +262,36 @@ def _solve_native_traced( "checkpoint_interval and checkpoint_capacity must be jointly set" ) + copied_domains: tuple[int, ...] | None = None + native_domains: object | None = None + solver_options: _WangSolverOptions | None = None + if initial_domains is not None: + try: + copied_domains = tuple(initial_domains) + except TypeError as error: + raise ValueError("initial_domains must be a finite integer sequence") from error + if len(copied_domains) != len(region.active): + raise ValueError("initial_domains length must match the region area") + for index, (active, domain) in enumerate( + zip(region.active, copied_domains, strict=True) + ): + if type(domain) is not int or not 0 <= domain <= DOMAIN_ALL: + raise ValueError( + f"initial_domains[{index}] is not a canonical Wang domain" + ) + if not active and domain != 0: + raise ValueError( + f"initial_domains[{index}] must be zero for an inactive cell" + ) + native_domains = (c_uint32 * len(copied_domains))(*copied_domains) + solver_options = _WangSolverOptions( + flags=0, + failed_leaf_path=None, + failed_leaf_capacity=0, + initial_domains=native_domains, + initial_domain_count=len(copied_domains), + ) + native_options = _WangSolveTraceOptions( event_capacity=event_capacity, checkpoint_interval=checkpoint_interval, @@ -275,7 +308,7 @@ def _solve_native_traced( try: status_code = solve( byref(native_reduction.region), - None, + None if solver_options is None else byref(solver_options), byref(native_options), byref(native_result), ) diff --git a/python/native/trace_pipeline.py b/python/native/trace_pipeline.py index 656b711..b6cd69c 100644 --- a/python/native/trace_pipeline.py +++ b/python/native/trace_pipeline.py @@ -1,9 +1,14 @@ """One-lifetime native formula, reduction, solve, and trace orchestration.""" +from collections.abc import Sequence +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.solver_trace import DOMAIN_ALL, SolverTrace from model.tiling import TilingSolveResult, TilingSolveStatus from model.tileset import TILESET from native.formula_adapter import PathLike, _copy_formula, _loaded_formula @@ -17,32 +22,99 @@ from oracles.tiling_check import is_valid_tiling -def solve_native_pipeline_trace( +@dataclass(frozen=True, slots=True) +class NativeTraceTimings: + """Raw monotonic durations for the native stages of one observed run.""" + + parse_ns: int + region_build_ns: int + solve_ns: int + verify_ns: int + + def __post_init__(self) -> None: + for name in ("parse_ns", "region_build_ns", "solve_ns", "verify_ns"): + value = getattr(self, name) + if type(value) is not int or value < 0: + raise ValueError(f"{name} must be a nonnegative integer") + + +NativeTraceValues = tuple[ + Formula, + Region, + ReductionExplanation, + TilingSolveResult, + SolverTrace, +] + + +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 capture_native_pipeline_trace( path: PathLike, *, optimized: bool = False, event_capacity: int = 20_000, checkpoint_interval: int = 64, checkpoint_capacity: int = 64, -) -> tuple[ - Formula, - Region, - ReductionExplanation, - TilingSolveResult, - SolverTrace, -]: - """Copy one observed native run before every C lifetime is released.""" + initial_domains: Sequence[int] | None = None, + initial_domain_overrides: Sequence[tuple[int, int]] | None = None, + clock_ns: Callable[[], int] = perf_counter_ns, +) -> tuple[NativeTraceValues, NativeTraceTimings]: + """Capture one traced run plus raw stage durations from a monotonic clock.""" if type(optimized) is not bool: raise TypeError("optimized must be a boolean") + if not callable(clock_ns): + raise TypeError("clock_ns must be callable") + if initial_domains is not None and initial_domain_overrides is not None: + raise ValueError( + "initial_domains and initial_domain_overrides are mutually exclusive" + ) + 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), ) + region_build_ns = _elapsed_ns(clock_ns, started) + + started = clock_ns() + configured_domains = initial_domains + if initial_domain_overrides is not None: + configured = [DOMAIN_ALL if active else 0 for active in region.active] + previous_cell = -1 + for index, override in enumerate(initial_domain_overrides): + if type(override) is not tuple or len(override) != 2: + raise ValueError( + f"initial_domain_overrides[{index}] must be a cell/domain pair" + ) + cell, domain = override + if type(cell) is not int or cell <= previous_cell: + raise ValueError( + "initial_domain_overrides must use unique sorted cells" + ) + if cell >= len(configured) or not region.active[cell]: + raise ValueError( + f"initial_domain_overrides[{index}] targets no active cell" + ) + if type(domain) is not int or not 0 <= domain <= DOMAIN_ALL: + raise ValueError( + f"initial_domain_overrides[{index}] is not a Wang domain" + ) + configured[cell] = domain + previous_cell = cell + configured_domains = tuple(configured) result, trace = _solve_native_traced( native_reduction.reduction, region, @@ -50,7 +122,11 @@ def solve_native_pipeline_trace( event_capacity=event_capacity, checkpoint_interval=checkpoint_interval, checkpoint_capacity=checkpoint_capacity, + initial_domains=configured_domains, ) + solve_ns = _elapsed_ns(clock_ns, started) + + started = clock_ns() if result.status is TilingSolveStatus.SAT: if result.tiling is None or not is_valid_tiling( region, @@ -60,4 +136,36 @@ def solve_native_pipeline_trace( raise NativeWitnessError( "traced native SAT tiling was rejected by the Python checker" ) - return formula, region, explanation, result, trace + verify_ns = _elapsed_ns(clock_ns, started) + + values: NativeTraceValues = (formula, region, explanation, result, trace) + timings = NativeTraceTimings( + parse_ns=parse_ns, + region_build_ns=region_build_ns, + solve_ns=solve_ns, + verify_ns=verify_ns, + ) + return values, timings + + +def solve_native_pipeline_trace( + path: PathLike, + *, + optimized: bool = False, + event_capacity: int = 20_000, + checkpoint_interval: int = 64, + checkpoint_capacity: int = 64, + initial_domains: Sequence[int] | None = None, + initial_domain_overrides: Sequence[tuple[int, int]] | None = None, +) -> NativeTraceValues: + """Copy one observed native run before every C lifetime is released.""" + values, _ = capture_native_pipeline_trace( + path, + optimized=optimized, + event_capacity=event_capacity, + checkpoint_interval=checkpoint_interval, + checkpoint_capacity=checkpoint_capacity, + initial_domains=initial_domains, + initial_domain_overrides=initial_domain_overrides, + ) + return values diff --git a/renderer/README.md b/renderer/README.md index f5da873..88f1e98 100644 --- a/renderer/README.md +++ b/renderer/README.md @@ -149,6 +149,14 @@ uv run --locked python wang_trace_render.py \ output/solver-trace ``` +The static projection of the same v3 manifest can also drive the existing +formula, tileset, region, and reduction views. It verifies every reference by +schema and hash but deliberately does not replay trace or solution content; +the trace consumer remains their semantic validator. This lets the root opt-in +dossier generator reuse one trace bundle without synthesizing a second v1/v2 +manifest. The renderer still imports neither native code nor Z3, and it does +not own LaTeX or report metadata. + Z3 uses a separate `encoding-order` summary. The renderer shows the explicit project-owned row-major constraint construction and returned model, never an internal Z3 search or debug trace: @@ -360,9 +368,9 @@ Raises `RenderingException` on pipeline errors. uv run --locked pytest -q ``` -The complete isolated suite has 253 tests: the 144 preserved legacy tests -below, 45 Wang square tests, 24 square-to-hex/hex-raster tests, 25 static -snapshot/explainability tests, and 15 trace/Z3/algorithm-animation tests. +The complete isolated suite has 262 tests: the 144 preserved legacy tests +below, 45 Wang square tests, 24 square-to-hex/hex-raster tests, 29 static +snapshot/explainability tests, and 20 trace/Z3/algorithm-animation tests. To run only the original upstream suite: ```bash diff --git a/renderer/test_wang_snapshot.py b/renderer/test_wang_snapshot.py index 75a2ba5..1e43fd3 100644 --- a/renderer/test_wang_snapshot.py +++ b/renderer/test_wang_snapshot.py @@ -50,6 +50,7 @@ ROOT / "tests/fixtures/pipeline_sat_reduction_explain" ) REDUCTION_MANIFEST = REDUCTION_SNAPSHOT_DIRECTORY / "manifest.json" +TRACE_MANIFEST = ROOT / "tests/fixtures/pipeline_sat_solver_trace/manifest.json" REDUCTION_GOLDEN = RENDERER_DIR / "test_data/pipeline_sat_reduction.png" GOLDENS = { ("formula", False): RENDERER_DIR / "test_data/pipeline_sat_formula.png", @@ -246,6 +247,32 @@ def test_reduction_view_matches_native_provenance_golden(tmp_path): assert image.mode == "RGB" +@pytest.mark.parametrize( + ("view", "golden"), + ( + ("formula", GOLDENS[("formula", False)]), + ("region", GOLDENS[("region", False)]), + ("reduction", REDUCTION_GOLDEN), + ), +) +def test_v3_trace_manifest_reuses_static_snapshot_views(tmp_path, view, golden): + output = tmp_path / f"{view}.png" + + render_pipeline_snapshot(TRACE_MANIFEST, output, view=view) + + assert output.read_bytes() == golden.read_bytes() + assert "native._lib" not in sys.modules + + +def test_v3_static_projection_does_not_import_or_replay_trace_consumer(): + sys.modules.pop("wang_trace", None) + + bundle = load_explainability_bundle(TRACE_MANIFEST) + + assert bundle.reduction is not None + assert "wang_trace" not in sys.modules + + @pytest.mark.parametrize("hex_mode", (False, True)) def test_solution_explain_views_match_separate_goldens(tmp_path, hex_mode): output = tmp_path / "render.png" diff --git a/renderer/wang_snapshot.py b/renderer/wang_snapshot.py index 7130258..42f21e7 100644 --- a/renderer/wang_snapshot.py +++ b/renderer/wang_snapshot.py @@ -736,7 +736,7 @@ def _parse_reduction(document: dict[str, object]) -> ReductionExplanationSnapsho def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: - """Load a v1/v2 manifest and independently verify every referenced stage.""" + """Load static v1/v2/v3 stages, hash-binding non-static v3 artifacts.""" manifest_path = Path(path) manifest = _load_json_bytes( _read_bytes(manifest_path, "manifest"), @@ -763,6 +763,16 @@ def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: "region": REGION_SCHEMA, "reduction": REDUCTION_SCHEMA, } + elif manifest_schema == "wang-explain-manifest-v3": + _literal(manifest["stage"], "solver-trace", "$.stage") + expected_schemas = { + "formula": FORMULA_SCHEMA, + "tileset": TILESET_SCHEMA, + "region": REGION_SCHEMA, + "reduction": REDUCTION_SCHEMA, + "trace": "wang-solver-trace-v1", + "solution": "wang-solution-v1", + } else: _fail("$.schema", "must be a supported explainability manifest") source_digest = _sha256( @@ -775,6 +785,10 @@ def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: artifact_digests: dict[str, str] = {} for name, expected_schema in expected_schemas.items(): reference_path = f"$.artifacts.{name}" + if artifacts[name] is None: + if name != "solution": + _fail(reference_path, "must not be null") + continue reference = _object(artifacts[name], reference_path) _fields(reference, frozenset({"path", "sha256", "schema"}), reference_path) artifact_name = _basename(reference["path"], f"{reference_path}.path") @@ -787,7 +801,10 @@ def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: encoded = _read_bytes(artifact_path, f"{name} artifact") if hashlib.sha256(encoded).hexdigest() != expected_digest: _fail(f"{reference_path}.sha256", f"does not match {artifact_name}") - documents[name] = _load_json_bytes(encoded, str(artifact_path)) + document = _load_json_bytes(encoded, str(artifact_path)) + if document.get("schema") != expected_schema: + _fail(f"{reference_path}.schema", "does not match artifact") + documents[name] = document artifact_digests[name] = expected_digest formula = _parse_formula(documents["formula"]) diff --git a/schemas/wang-run-case-v1.schema.json b/schemas/wang-run-case-v1.schema.json new file mode 100644 index 0000000..f105b77 --- /dev/null +++ b/schemas/wang-run-case-v1.schema.json @@ -0,0 +1,58 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://xtraid.github.io/tiling-foundry/schemas/wang-run-case-v1.schema.json", + "title": "Tiling Foundry observed-run dossier case v1", + "type": "object", + "additionalProperties": false, + "required": [ + "schema", + "id", + "title", + "classification", + "description", + "source", + "solver", + "expected_status", + "trace", + "initial_domain_overrides" + ], + "properties": { + "schema": {"const": "wang-run-case-v1"}, + "id": {"type": "string", "pattern": "^[a-z0-9]+(?:-[a-z0-9]+)*$"}, + "title": {"type": "string", "minLength": 1}, + "classification": { + "enum": [ + "sat-end-to-end", + "unsat-root-conflict", + "unsat-propagation-contradiction", + "unsat-non-superficial-search" + ] + }, + "description": {"type": "string", "minLength": 1}, + "source": {"type": "string", "pattern": "^(?!/)(?!.*(?:^|/)\\.\\.?/).+\\.cm13$"}, + "solver": {"enum": ["reference", "optimized"]}, + "expected_status": {"enum": ["sat", "unsat"]}, + "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} + } + }, + "initial_domain_overrides": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["cell", "domain"], + "properties": { + "cell": {"type": "integer", "minimum": 0}, + "domain": {"type": "integer", "minimum": 0, "maximum": 8388607} + } + } + } + } +} diff --git a/schemas/wang-run-dossier-v1.schema.json b/schemas/wang-run-dossier-v1.schema.json new file mode 100644 index 0000000..00e9149 --- /dev/null +++ b/schemas/wang-run-dossier-v1.schema.json @@ -0,0 +1,171 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://xtraid.github.io/tiling-foundry/schemas/wang-run-dossier-v1.schema.json", + "title": "Tiling Foundry observed-run dossier v1", + "type": "object", + "additionalProperties": false, + "required": ["schema", "case", "source", "environment", "solver", "timings", "artifacts"], + "properties": { + "schema": {"const": "wang-run-dossier-v1"}, + "case": { + "type": "object", + "additionalProperties": false, + "required": ["id", "title", "classification", "description"], + "properties": { + "id": {"type": "string", "pattern": "^[a-z0-9]+(?:-[a-z0-9]+)*$"}, + "title": {"type": "string", "minLength": 1}, + "classification": { + "enum": [ + "sat-end-to-end", + "unsat-root-conflict", + "unsat-propagation-contradiction", + "unsat-non-superficial-search" + ] + }, + "description": {"type": "string", "minLength": 1} + } + }, + "source": { + "type": "object", + "additionalProperties": false, + "required": ["path", "sha256"], + "properties": { + "path": {"type": "string", "minLength": 1}, + "sha256": {"type": "string", "pattern": "^[0-9a-f]{64}$"} + } + }, + "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}$"} + } + }, + "solver": { + "type": "object", + "additionalProperties": false, + "required": [ + "engine", + "semantics", + "status", + "expected_status", + "initial_domain_overrides", + "trace", + "replay" + ], + "properties": { + "engine": {"enum": ["reference", "optimized"]}, + "semantics": {"const": "observed"}, + "status": {"enum": ["sat", "unsat"]}, + "expected_status": {"enum": ["sat", "unsat"]}, + "initial_domain_overrides": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["cell", "domain"], + "properties": { + "cell": {"type": "integer", "minimum": 0}, + "domain": {"type": "integer", "minimum": 0, "maximum": 8388607} + } + } + }, + "trace": { + "type": "object", + "additionalProperties": false, + "required": [ + "event_capacity", + "observed_event_count", + "truncated", + "checkpoint_interval", + "checkpoint_capacity", + "checkpoint_count", + "event_counts", + "max_depth" + ], + "properties": { + "event_capacity": {"type": "integer", "minimum": 2}, + "observed_event_count": {"type": "integer", "minimum": 2}, + "truncated": {"const": false}, + "checkpoint_interval": {"type": "integer", "minimum": 0}, + "checkpoint_capacity": {"type": "integer", "minimum": 0}, + "checkpoint_count": {"type": "integer", "minimum": 0}, + "event_counts": { + "type": "object", + "additionalProperties": false, + "required": ["root", "propagation", "decision", "domain_reduction", "conflict", "backtrack", "result"], + "properties": { + "root": {"type": "integer", "minimum": 0}, + "propagation": {"type": "integer", "minimum": 0}, + "decision": {"type": "integer", "minimum": 0}, + "domain_reduction": {"type": "integer", "minimum": 0}, + "conflict": {"type": "integer", "minimum": 0}, + "backtrack": {"type": "integer", "minimum": 0}, + "result": {"type": "integer", "minimum": 0} + } + }, + "max_depth": {"type": "integer", "minimum": 0} + } + }, + "replay": { + "type": "object", + "additionalProperties": false, + "required": ["trace_scope", "frame_scope", "unsat_certificate"], + "properties": { + "trace_scope": {"const": "complete"}, + "frame_scope": {"const": "selected"}, + "unsat_certificate": {"const": false} + } + } + } + }, + "timings": { + "type": "object", + "additionalProperties": false, + "required": ["clock", "identity", "stages"], + "properties": { + "clock": {"const": "monotonic-perf-counter-ns"}, + "identity": {"const": "environment-specific-observation"}, + "stages": { + "type": "array", + "minItems": 7, + "maxItems": 7, + "items": { + "type": "object", + "additionalProperties": false, + "required": ["name", "performed", "elapsed_ns"], + "properties": { + "name": { + "enum": ["parse", "region_build", "encoding", "solve", "verify", "export", "render"] + }, + "performed": {"type": "boolean"}, + "elapsed_ns": {"type": ["integer", "null"], "minimum": 0} + } + } + } + } + }, + "artifacts": { + "type": "object", + "minProperties": 8, + "additionalProperties": { + "type": "object", + "additionalProperties": false, + "required": ["path", "sha256", "media_type", "role"], + "properties": { + "path": {"type": "string", "pattern": "^assets/(?!.*(?:^|/)\\.\\.?/).+"}, + "sha256": {"type": "string", "pattern": "^[0-9a-f]{64}$"}, + "media_type": {"enum": ["application/json", "image/png", "image/gif"]}, + "role": {"type": "string", "minLength": 1} + } + } + } + } +} diff --git a/templates/run-report.tex b/templates/run-report.tex new file mode 100644 index 0000000..14d413c --- /dev/null +++ b/templates/run-report.tex @@ -0,0 +1,25 @@ +\documentclass[11pt]{article} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage[a4paper,margin=20mm]{geometry} +\usepackage{array} +\usepackage{graphicx} + +\ifdefined\pdfinfoomitdate + \pdfinfoomitdate=1 +\fi +\ifdefined\pdftrailerid + \pdftrailerid{} +\fi +\ifdefined\pdfsuppressptexinfo + \pdfsuppressptexinfo=15 +\fi + +\title{@@TITLE@@} +\author{Tiling Foundry observed-run dossier} +\date{} + +\begin{document} +\maketitle +@@BODY@@ +\end{document} diff --git a/tests/instances/pipeline_unsat_search.cm13 b/tests/instances/pipeline_unsat_search.cm13 new file mode 100644 index 0000000..a257a53 --- /dev/null +++ b/tests/instances/pipeline_unsat_search.cm13 @@ -0,0 +1,6 @@ +c UNSAT dossier case requiring depth-two native search and backtracking +p cm13 4 4 +1 1 2 0 +1 2 3 0 +2 3 3 0 +4 4 4 0 diff --git a/tests/python/test_native_solver_trace.py b/tests/python/test_native_solver_trace.py index 1828ef8..7f9eda0 100644 --- a/tests/python/test_native_solver_trace.py +++ b/tests/python/test_native_solver_trace.py @@ -5,9 +5,11 @@ from pathlib import Path from model.solver_trace import ( + DOMAIN_ALL, SOLVER_OPTIMIZED, SOLVER_REFERENCE, TRACE_DECISION, + TRACE_CONFLICT, TRACE_DOMAIN_REDUCTION, TRACE_PROPAGATION, TRACE_RESULT, @@ -104,6 +106,55 @@ def test_rejects_invalid_trace_capacity_before_native_call(self) -> None: checkpoint_capacity=0, ) + def test_initial_domain_overrides_distinguish_root_and_propagation_conflicts(self) -> None: + _, region, *_ = solve_native_pipeline_trace(INSTANCE, optimized=True) + base = tuple(DOMAIN_ALL if active else 0 for active in region.active) + + empty = tuple(0 if index == 0 else domain for index, domain in enumerate(base)) + *_, root_trace = solve_native_pipeline_trace( + INSTANCE, + optimized=True, + initial_domains=empty, + checkpoint_interval=0, + checkpoint_capacity=0, + ) + self.assertEqual( + tuple(event.kind for event in root_trace.events), + (TRACE_ROOT, TRACE_CONFLICT, TRACE_RESULT), + ) + self.assertEqual(root_trace.events[1].phase, "initial") + + singleton = tuple(8 if index == 0 else domain for index, domain in enumerate(base)) + *_, propagation_trace = solve_native_pipeline_trace( + INSTANCE, + optimized=True, + initial_domains=singleton, + checkpoint_interval=0, + checkpoint_capacity=0, + ) + kinds = tuple(event.kind for event in propagation_trace.events) + self.assertIn(TRACE_DOMAIN_REDUCTION, kinds) + self.assertIn(TRACE_PROPAGATION, kinds) + self.assertIn(TRACE_CONFLICT, kinds) + self.assertNotIn(TRACE_DECISION, kinds) + self.assertEqual( + next(event for event in propagation_trace.events if event.kind == TRACE_CONFLICT).phase, + "initial", + ) + + def test_initial_domain_validation_is_type_strict(self) -> None: + _, region, *_ = solve_native_pipeline_trace(INSTANCE, optimized=True) + domains = [DOMAIN_ALL if active else 0 for active in region.active] + domains[0] = True + with self.assertRaisesRegex(ValueError, "canonical Wang domain"): + solve_native_pipeline_trace(INSTANCE, initial_domains=domains) + + with self.assertRaisesRegex(ValueError, "unique sorted cells"): + solve_native_pipeline_trace( + INSTANCE, + initial_domain_overrides=((1, DOMAIN_ALL), (0, DOMAIN_ALL)), + ) + if __name__ == "__main__": unittest.main() diff --git a/tests/python/test_run_dossier.py b/tests/python/test_run_dossier.py new file mode 100644 index 0000000..b7a536a --- /dev/null +++ b/tests/python/test_run_dossier.py @@ -0,0 +1,198 @@ +from __future__ import annotations + +import copy +from dataclasses import replace +import hashlib +import json +from pathlib import Path +import tempfile +import unittest + +from formats.pipeline_snapshot import PipelineSnapshotError +from formats.run_dossier import ( + CLASS_ROOT_CONFLICT, + build_run_dossier, + load_run_case, + load_run_dossier, + validate_case_outcome, + validate_run_dossier, +) +from formats.run_report_tex import render_run_report_tex +from native.trace_pipeline import capture_native_pipeline_trace + + +ROOT = Path(__file__).resolve().parents[2] +CASES = ROOT / "examples/run-cases" +TEMPLATE = ROOT / "templates/run-report.tex" + + +def _artifacts() -> dict[str, dict[str, str]]: + specs = { + "trace_manifest": ("assets/data/manifest.json", "application/json"), + "formula_view": ("assets/images/formula.png", "image/png"), + "region_square": ("assets/images/region-square.png", "image/png"), + "region_hex": ("assets/images/region-hex.png", "image/png"), + "reduction_view": ("assets/images/reduction.png", "image/png"), + "trace_contact_sheet": ("assets/images/trace/contact-sheet.png", "image/png"), + "trace_fallback": ("assets/images/trace/frame-000001.png", "image/png"), + "trace_animation": ("assets/images/trace/trace.gif", "image/gif"), + } + return { + name: { + "path": path, + "sha256": f"{index + 1:064x}", + "media_type": media_type, + "role": f"test {name}", + } + for index, (name, (path, media_type)) in enumerate(specs.items()) + } + + +class RunDossierTests(unittest.TestCase): + def test_versioned_cases_match_distinct_complete_observed_runs(self) -> None: + summaries: dict[str, tuple[str, int, int]] = {} + for case_path in sorted(CASES.glob("*.json")): + with self.subTest(case=case_path.name): + case = load_run_case(case_path, ROOT) + overrides = tuple( + (item.cell, item.domain) + for item in case.initial_domain_overrides + ) + values, timings = capture_native_pipeline_trace( + ROOT / case.source, + optimized=case.solver == "optimized", + event_capacity=case.event_capacity, + checkpoint_interval=case.checkpoint_interval, + checkpoint_capacity=case.checkpoint_capacity, + initial_domain_overrides=overrides or None, + ) + trace = values[-1] + validate_case_outcome(case, trace) + self.assertFalse(trace.truncated) + self.assertGreaterEqual(timings.solve_ns, 0) + summaries[case.identifier] = ( + trace.status.value, + trace.observed_event_count, + max(event.depth for event in trace.events), + ) + + self.assertEqual(summaries["unsat-root-conflict"], ("unsat", 3, 0)) + self.assertEqual(summaries["unsat-search"][0], "unsat") + self.assertGreaterEqual(summaries["unsat-search"][2], 2) + self.assertEqual(len(summaries), 4) + + def test_builds_closed_raw_run_and_fixed_latex_from_the_same_data(self) -> None: + case = load_run_case(CASES / "unsat-root-conflict.json", ROOT) + self.assertEqual(case.classification, CLASS_ROOT_CONFLICT) + overrides = tuple( + (item.cell, item.domain) for item in case.initial_domain_overrides + ) + values, _ = capture_native_pipeline_trace( + ROOT / case.source, + optimized=True, + event_capacity=case.event_capacity, + checkpoint_interval=case.checkpoint_interval, + checkpoint_capacity=case.checkpoint_capacity, + initial_domain_overrides=overrides, + ) + trace = values[-1] + timings = { + "parse": 10, + "region_build": 20, + "encoding": None, + "solve": 30, + "verify": None, + "export": 50, + "render": 60, + } + source_digest = hashlib.sha256((ROOT / case.source).read_bytes()).hexdigest() + document = build_run_dossier( + case, + trace, + source_sha256=source_digest, + captured_at_utc="2026-08-27T20:00:00Z", + platform="test-platform", + python_version="3.14.0", + git_commit="0" * 40, + timings_ns=timings, + artifacts=_artifacts(), + ) + + validate_run_dossier(document) + tex = render_run_report_tex(document, TEMPLATE.read_text(encoding="utf-8")) + self.assertIn("UNSAT immediate root conflict", tex) + self.assertIn("not applicable", tex) + self.assertIn("not a mathematical UNSAT certificate", tex) + self.assertNotIn("@@TITLE@@", tex) + self.assertNotIn("@@BODY@@", tex) + self.assertNotIn("\\write18", tex) + + with tempfile.TemporaryDirectory() as directory: + dossier = Path(directory) + for name, item in document["artifacts"].items(): + asset = dossier / item["path"] + asset.parent.mkdir(parents=True, exist_ok=True) + encoded = f"artifact:{name}".encode("ascii") + asset.write_bytes(encoded) + item["sha256"] = hashlib.sha256(encoded).hexdigest() + run_path = dossier / "run.json" + run_path.write_text( + json.dumps(document, ensure_ascii=False, separators=(",", ":")) + "\n", + encoding="utf-8", + ) + self.assertEqual(load_run_dossier(run_path), document) + (dossier / document["artifacts"]["formula_view"]["path"]).write_bytes( + b"tampered" + ) + with self.assertRaisesRegex(PipelineSnapshotError, "does not match"): + load_run_dossier(run_path) + + with tempfile.TemporaryDirectory() as outside_directory: + external = Path(outside_directory) / "formula.png" + external.write_bytes(b"external artifact") + formula = dossier / document["artifacts"]["formula_view"]["path"] + formula.unlink() + formula.symlink_to(external) + document["artifacts"]["formula_view"]["sha256"] = hashlib.sha256( + external.read_bytes() + ).hexdigest() + run_path.write_text( + json.dumps(document, ensure_ascii=False, separators=(",", ":")) + "\n", + encoding="utf-8", + ) + with self.assertRaisesRegex(PipelineSnapshotError, "self-contained"): + load_run_dossier(run_path) + + invalid = copy.deepcopy(document) + invalid["artifacts"]["formula_view"]["path"] = "../escape.png" + with self.assertRaisesRegex(PipelineSnapshotError, "normalized relative"): + validate_run_dossier(invalid) + + invalid = copy.deepcopy(document) + invalid["solver"]["trace"]["truncated"] = True + invalid["solver"]["replay"]["trace_scope"] = "truncated-prefix" + with self.assertRaisesRegex(PipelineSnapshotError, "complete trace"): + validate_run_dossier(invalid) + + with self.assertRaisesRegex(PipelineSnapshotError, "solver disagrees"): + validate_case_outcome(replace(case, solver="reference"), trace) + + def test_case_loader_rejects_duplicate_members_and_wrong_status(self) -> None: + with self.subTest("status"): + case_path = CASES / "sat-end-to-end.json" + encoded = case_path.read_text(encoding="utf-8").replace( + '"expected_status": "sat"', + '"expected_status": "unsat"', + ) + temporary = ROOT / "build/test-invalid-run-case.json" + temporary.parent.mkdir(exist_ok=True) + temporary.write_text(encoded, encoding="utf-8") + try: + with self.assertRaisesRegex(PipelineSnapshotError, "disagrees"): + load_run_case(temporary, ROOT) + finally: + temporary.unlink(missing_ok=True) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/generate_run_dossier.py b/tools/generate_run_dossier.py new file mode 100644 index 0000000..db82355 --- /dev/null +++ b/tools/generate_run_dossier.py @@ -0,0 +1,446 @@ +#!/usr/bin/env python3 +"""Generate one opt-in, self-contained observed-run dossier.""" + +from __future__ import annotations + +import argparse +import calendar +from datetime import datetime, timezone +import hashlib +import os +from pathlib import Path +import platform as platform_module +import shutil +import subprocess +import sys +import tempfile +from time import perf_counter_ns + + +ROOT = Path(__file__).resolve().parents[1] +RENDERER = ROOT / "renderer" +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.run_dossier import ( # noqa: E402 + RunCase, + build_run_dossier, + load_run_case, + load_run_dossier, + validate_case_outcome, +) +from formats.run_report_tex import render_run_report_tex # noqa: E402 +from formats.solver_trace_snapshot import ( # noqa: E402 + dump_solver_trace_bundle, + load_solver_trace_bundle, +) +from native.trace_pipeline import capture_native_pipeline_trace # noqa: E402 + + +class DossierGenerationError(RuntimeError): + """The opt-in report pipeline could not complete atomically.""" + + +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" + ) + ) + parser.add_argument("case", type=Path, help="wang-run-case-v1 JSON") + parser.add_argument("output_directory", type=Path) + parser.add_argument( + "--tex-engine", + default="pdflatex", + help="pdfLaTeX executable (default: pdflatex)", + ) + parser.add_argument("--max-frames", type=int, default=12) + parser.add_argument("--duration-ms", type=int, default=500) + return parser + + +def _run_renderer(arguments: list[str]) -> str: + uv = shutil.which("uv") + if uv is None: + raise DossierGenerationError("uv is required to run the isolated renderer") + command = [uv, "run", "--locked", "python", *arguments] + try: + completed = subprocess.run( + command, + cwd=RENDERER, + check=True, + capture_output=True, + text=True, + timeout=180, + ) + except (OSError, subprocess.SubprocessError) as error: + detail = getattr(error, "stderr", "") or str(error) + raise DossierGenerationError(f"renderer failed: {detail.strip()}") from error + return completed.stdout + + +def _render_assets( + manifest_path: Path, + manifest: dict[str, object], + images: Path, + *, + max_frames: int, + duration_ms: int, +) -> Path: + images.mkdir(parents=True, exist_ok=True) + trace_directory = images / "trace" + stdout = _run_renderer( + [ + "wang_trace_render.py", + str(manifest_path), + str(trace_directory), + "--max-frames", + str(max_frames), + "--duration-ms", + str(duration_ms), + ] + ) + fallback: Path | None = None + for line in stdout.splitlines(): + if line.startswith("fallback="): + fallback = Path(line.removeprefix("fallback=")) + if fallback is None or not fallback.is_file() or fallback.parent != trace_directory: + raise DossierGenerationError("trace renderer did not publish a local fallback") + + views = ( + ("formula", "formula.png", False), + ("region", "region-square.png", False), + ("region", "region-hex.png", True), + ("reduction", "reduction.png", False), + ) + for view, name, hex_mode in views: + arguments = [ + "wang_square.py", + str(manifest_path), + str(images / name), + "--view", + view, + ] + if hex_mode: + arguments.append("--hex") + _run_renderer(arguments) + + artifacts = manifest["artifacts"] + assert isinstance(artifacts, dict) + solution_reference = artifacts["solution"] + if solution_reference is not None: + assert isinstance(solution_reference, dict) + solution_path = manifest_path.parent / str(solution_reference["path"]) + _run_renderer( + [ + "wang_square.py", + str(solution_path), + str(images / "solution-square.png"), + "--explain", + ] + ) + _run_renderer( + [ + "wang_square.py", + str(solution_path), + str(images / "solution-hex.png"), + "--explain", + "--hex", + ] + ) + return fallback + + +def _artifact( + dossier_root: Path, + path: Path, + *, + media_type: str, + role: str, +) -> dict[str, str]: + try: + encoded = path.read_bytes() + relative = path.relative_to(dossier_root).as_posix() + except (OSError, ValueError) as error: + raise DossierGenerationError(f"cannot bind artifact {path!s}: {error}") from error + return { + "path": relative, + "sha256": hashlib.sha256(encoded).hexdigest(), + "media_type": media_type, + "role": role, + } + + +def _collect_artifacts( + dossier_root: Path, + manifest_path: Path, + manifest: dict[str, object], + fallback: Path, +) -> dict[str, dict[str, str]]: + artifacts: dict[str, dict[str, str]] = { + "trace_manifest": _artifact( + dossier_root, + manifest_path, + media_type="application/json", + role="hash-bound solver trace manifest", + ), + } + references = manifest["artifacts"] + assert isinstance(references, dict) + for name, reference in references.items(): + if reference is None: + continue + assert isinstance(reference, dict) + artifacts[f"{name}_snapshot"] = _artifact( + dossier_root, + manifest_path.parent / str(reference["path"]), + media_type="application/json", + role=f"authoritative {name} document", + ) + + images = dossier_root / "assets/images" + image_specs = { + "formula_view": (images / "formula.png", "parsed formula view"), + "region_square": (images / "region-square.png", "square region view"), + "region_hex": (images / "region-hex.png", "checked hex region view"), + "reduction_view": (images / "reduction.png", "native reduction provenance view"), + "trace_contact_sheet": ( + images / "trace/contact-sheet.png", + "selected observed trace states", + ), + "trace_fallback": (fallback, "accessible static trace fallback"), + "trace_animation": ( + images / "trace/trace.gif", + "presentation-only trace animation", + ), + } + if references["solution"] is not None: + image_specs.update( + { + "solution_square": ( + images / "solution-square.png", + "verified square witness view", + ), + "solution_hex": ( + images / "solution-hex.png", + "checked hex witness view", + ), + } + ) + for name, (image_path, role) in image_specs.items(): + media_type = "image/gif" if image_path.suffix == ".gif" else "image/png" + artifacts[name] = _artifact( + dossier_root, + image_path, + media_type=media_type, + role=role, + ) + remaining_frames = tuple( + frame + for frame in sorted((images / "trace").glob("frame-*.png")) + if frame != fallback + ) + for index, frame in enumerate(remaining_frames): + artifacts[f"trace_frame_{index:03d}"] = _artifact( + dossier_root, + frame, + media_type="image/png", + role="selected observed trace frame", + ) + return artifacts + + +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 DossierGenerationError(f"cannot identify repository commit: {error}") from error + return completed.stdout.strip() + + +def _compile_pdf(dossier_root: Path, tex_engine: str, captured_at: datetime) -> None: + executable = shutil.which(tex_engine) + if executable is None: + raise DossierGenerationError(f"TeX engine not found: {tex_engine}") + tex_home = dossier_root / ".tex-home" + tex_home.mkdir() + tex_var = tex_home / "var" + tex_config = tex_home / "config" + tex_fonts = tex_var / "fonts" + tex_var.mkdir() + tex_config.mkdir() + tex_fonts.mkdir() + environment = { + "PATH": os.environ.get("PATH", "/usr/bin:/bin"), + "HOME": str(tex_home), + "TEXMFHOME": str(tex_home / "texmf"), + "TEXMFVAR": str(tex_var), + "TEXMFCONFIG": str(tex_config), + "VARTEXFONTS": str(tex_fonts), + "SOURCE_DATE_EPOCH": str(calendar.timegm(captured_at.utctimetuple())), + "TZ": "UTC", + "openin_any": "p", + "openout_any": "p", + } + command = [ + executable, + "-interaction=nonstopmode", + "-halt-on-error", + "-file-line-error", + "-no-shell-escape", + "report.tex", + ] + for _ in range(2): + try: + subprocess.run( + command, + cwd=dossier_root, + env=environment, + check=True, + capture_output=True, + text=True, + timeout=120, + ) + except (OSError, subprocess.SubprocessError) as error: + detail = getattr(error, "stdout", "") or getattr(error, "stderr", "") + raise DossierGenerationError( + f"LaTeX compilation failed without shell escape: {detail.strip()}" + ) from error + pdf = dossier_root / "report.pdf" + try: + if pdf.stat().st_size < 100 or not pdf.read_bytes().startswith(b"%PDF-"): + raise DossierGenerationError("TeX engine did not produce a valid PDF header") + except OSError as error: + raise DossierGenerationError(f"cannot inspect report.pdf: {error}") from error + for suffix in ("aux", "log", "out", "toc"): + auxiliary = dossier_root / f"report.{suffix}" + try: + auxiliary.unlink() + except FileNotFoundError: + pass + shutil.rmtree(tex_home) + + +def generate_run_dossier( + case_path: str | Path, + output_directory: str | Path, + *, + tex_engine: str, + max_frames: int = 12, + duration_ms: int = 500, +) -> Path: + """Generate all dossier outputs in staging and install the directory once.""" + case: RunCase = load_run_case(case_path, ROOT) + destination = Path(output_directory).resolve() + if destination.exists(): + raise DossierGenerationError(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_digest = hashlib.sha256(source_path.read_bytes()).hexdigest() + overrides = tuple( + (item.cell, item.domain) for item in case.initial_domain_overrides + ) + values, native_timings = capture_native_pipeline_trace( + source_path, + optimized=case.solver == "optimized", + event_capacity=case.event_capacity, + checkpoint_interval=case.checkpoint_interval, + checkpoint_capacity=case.checkpoint_capacity, + initial_domain_overrides=overrides or None, + ) + formula, region, explanation, result, trace = values + validate_case_outcome(case, trace) + + data_directory = staging / "assets/data" + data_directory.mkdir(parents=True) + manifest_path = data_directory / "manifest.json" + started = perf_counter_ns() + dump_solver_trace_bundle( + manifest_path, + source_path, + formula, + region, + explanation, + result, + trace, + ) + export_ns = perf_counter_ns() - started + manifest, _ = load_solver_trace_bundle(manifest_path) + + started = perf_counter_ns() + fallback = _render_assets( + manifest_path, + manifest, + staging / "assets/images", + max_frames=max_frames, + duration_ms=duration_ms, + ) + render_ns = perf_counter_ns() - started + artifacts = _collect_artifacts(staging, manifest_path, manifest, fallback) + + captured_at = datetime.now(timezone.utc).replace(microsecond=0) + timings_ns = { + "parse": native_timings.parse_ns, + "region_build": native_timings.region_build_ns, + "encoding": None, + "solve": native_timings.solve_ns, + "verify": native_timings.verify_ns if result.status.value == "sat" else None, + "export": export_ns, + "render": render_ns, + } + run_document = build_run_dossier( + case, + trace, + source_sha256=source_digest, + 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(), + timings_ns=timings_ns, + artifacts=artifacts, + ) + _write_atomic(staging / "run.json", _encode_document(run_document)) + load_run_dossier(staging / "run.json") + template = TEMPLATE.read_text(encoding="utf-8") + report_tex = render_run_report_tex(run_document, template) + _write_atomic(staging / "report.tex", report_tex.encode("utf-8")) + _compile_pdf(staging, tex_engine, captured_at) + os.replace(staging, destination) + return destination + except Exception: + shutil.rmtree(staging, ignore_errors=True) + raise + + +def main(arguments: list[str] | None = None) -> int: + parser = _parser() + args = parser.parse_args(arguments) + try: + destination = generate_run_dossier( + args.case, + args.output_directory, + tex_engine=args.tex_engine, + max_frames=args.max_frames, + duration_ms=args.duration_ms, + ) + except (DossierGenerationError, OSError, ValueError) as error: + parser.error(str(error)) + print(f"dossier={destination}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())