diff --git a/README.md b/README.md index 54c9fdd..273168d 100644 --- a/README.md +++ b/README.md @@ -72,6 +72,7 @@ solving remains future work. | Verified square solution export | Implemented as the closed `wang-solution-v1` contract and deterministic exporter | | Wang diagnostic renderer | Implemented as one presentation-only CLI with byte-stable square default and explicit `--hex` mode in the isolated `renderer/` project | | Square-to-hex presentation port | Implemented as a pure in-memory Basire/Culik mapping with a raster-independent checker; no hex solver, schema, or core model | +| Static explainability snapshots | Implemented for parsed formula, canonical tile sheet, and unassigned region, with hash-bound JSON contracts and square/hex diagnostic views | | 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 | @@ -89,29 +90,32 @@ The implemented paths are: ```text .cm13 --> C parser --> native Formula - | \ - | +--> copied Formula --> Boolean Z3 - | | - | v - | Boolean witness checker + | |\ + | | +--> formula snapshot --> formula view + | +----> copied Formula ----> Boolean Z3 + | | + | v + | Boolean witness checker v Yang–Zhang builder --> Region - | \ - | +--> copied Region + TILESET - | | - | v - native reference/ Wang Z3 - optimized solver | - | v - v Python tiling checker - native verifier - | - copied tiling + Python checker - | - v - wang-solution-v1 --> square PNG (default) - \ - +--> pure hex port/check --> hex PNG (--hex) + | |\ + | | +--> static manifest --> region view + | | + tile sheet + | +----> copied Region + TILESET + | | + | v + native reference/ Wang Z3 + optimized solver | + | v + v Python tiling checker + native verifier + | + copied tiling + Python checker + | + v + wang-solution-v1 --> square PNG (default/explain) + \ + +--> pure hex port/check --> hex PNG (--hex) ``` The witness bridge relates exact Boolean assignments to the variable cells of @@ -144,12 +148,15 @@ diagram. ## Next milestones -Planned work remains separated into independently reviewed changes: +Planned work remains separated into independently reviewed changes. The new +priority is explainability across the deterministic pipeline: -1. evaluate MRV indexing on weakly constrained search and build a separate - hard-UNSAT corpus before making parallelism claims; -2. harden allocation and cleanup failure paths before concurrent execution; -3. define and validate a minimal serial `TaskPlan` before implementing OpenMP. +1. add provenance overlays from formula positions to region structures without + changing the generic `Region` model; +2. define bounded, deterministic event traces for native DFS and explicit + encoding summaries for Z3, then render partial states by replay; +3. publish a compact formula-to-final-image gallery from versioned examples; +4. resume serial MRV and hard-UNSAT evidence before `TaskPlan` and OpenMP work. The implementation follows a deliberately small design rule: each datum has one owner, derived state is computed when needed, and future metadata is not added to @@ -172,7 +179,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 213-test combined suite independently: +`make check`. Run its 234-test combined suite independently: ```sh cd renderer @@ -206,6 +213,9 @@ The [square solution contract](docs/wang_solution_v1.md) includes the producer API for exporting a verified native result before rendering it. The [square-to-hex reference](docs/wang_square_to_hex.md) defines the mapping, inverse proof, checker boundary, and integer axial raster convention. +The [static snapshot contract](docs/wang_explainability_snapshots.md) documents +the real formula-to-region export and the formula, tile-sheet, region, and +opt-in final explainability views. Useful individual targets: @@ -285,11 +295,11 @@ src/verify/ independent tiling verification src/io/ formula parsing and native JSON placeholder python/model/ pure Python data contracts python/native/ C ABI adapters and ownership boundaries -python/formats/ versioned solution validation and deterministic export +python/formats/ versioned solution and static-snapshot validation/export python/crosscheck/ scoped native/Z3 witness orchestration python/oracles/ independent Z3 oracles and witness checks python/hex/ deliberately unused empty hex-core placeholders -renderer/ isolated legacy and square/default, hex/explicit Wang rendering +renderer/ isolated legacy and explainable square/hex Wang rendering tests/ C, Python, and instance regressions benchmarks/ fixed reference corpus and profiling runner docs/ theory and architecture references diff --git a/docs/development_principles.md b/docs/development_principles.md index f19821c..3f34ea6 100644 --- a/docs/development_principles.md +++ b/docs/development_principles.md @@ -95,9 +95,10 @@ A module is implemented when it has: | `python/native` | C ABI adaptation, scoped native lifetimes, and complete copy-out | Solver logic and escaping native pointers | | `python/crosscheck` | Scoped composition of adapters, Z3, and independent checkers | Persistent native state and duplicated reduction semantics | | `python/oracles` | Independent solvers and checkers over pure models | Parsing, filesystem I/O, and reduction construction | -| `python/formats` | Square solution validation and deterministic export | Native lifetimes, solving, and presentation | +| `python/formats` | Solution and static pipeline snapshot validation and deterministic export | Native lifetimes, solving, and presentation | | `renderer/wang_hex_port.py` | Pure square-to-hex mapping, inverse checks, and matching-equivalence checks | Raster geometry, semantic verification, and solver access | -| `renderer/wang_square.py` | Structural presentation projection and square/default or hex/explicit rasterization | Semantic verification and solver access | +| `renderer/wang_snapshot.py` | Strict hash-bound snapshot consumption and static formula, tile-sheet, and region composition | Native access, solving, and semantic verification | +| `renderer/wang_square.py` | One CLI for solution and static views, with square/default or hex/explicit rasterization | Semantic verification and solver access | `include/wang/task_plan.h`, `src/parallel/solver_openmp.c`, and the two modules under `python/hex/` are placeholders. `src/io/json.c` is also a placeholder; @@ -201,6 +202,15 @@ instances, and its tests verify that construction. ### Downstream solution and renderer boundary +Before solving, `python/formats/pipeline_snapshot.py` can project copied +`Formula`, canonical `TILESET`, and unassigned `Region` values into three +closed, versioned documents referenced by a hash-bound manifest. These are +presentation-neutral snapshots: they preserve source identity, ordered formula +positions, positional tile IDs, active cells, bounds, and exposed boundary +constraints without adding fields to the core models. The +[static snapshot contract]({{ '/wang-explainability-snapshots/' | relative_url }}) +defines their failure and rendering behavior. + The native-only solve coordinator copies a verified SAT tiling out of native storage and applies the independent Python Wang checker. The exporter then produces the closed square-only `wang-solution-v1` document. The diff --git a/docs/wang_explainability_snapshots.md b/docs/wang_explainability_snapshots.md new file mode 100644 index 0000000..f43047f --- /dev/null +++ b/docs/wang_explainability_snapshots.md @@ -0,0 +1,136 @@ +--- +layout: page +title: Static pipeline snapshots and explainable Wang views +permalink: /wang-explainability-snapshots/ +description: Versioned formula, tileset, and unassigned-region snapshots consumed by the isolated Wang renderer. +section: Architecture and correctness +document_kind: Data and rendering contract +status: Current implementation +updated: 2026-08-26 +nav_order: 33 +--- + +# Static pipeline snapshots and explainable Wang views + +The pipeline can export its state after parsing and region construction without +running a solver. The isolated renderer turns that state into three diagnostic +views: the parsed formula, the canonical tile sheet, and the unassigned region +with the formula beside it. A verified solution can additionally be rendered +with colored edge bands, tile IDs, emphasized boundary constraints, and a +palette legend. + +These views explain data that already exists at a module boundary. They do not +add presentation fields to `Formula` or `Region`, expose native pointers, or +make a PNG part of the correctness argument. + +## Contracts and identity + +The exporter writes four closed JSON documents: + +| Schema | Meaning | +| --- | --- | +| `cm13-formula-snapshot-v1` | Source basename and digest, ordered clauses, and all three variable positions, including repeats | +| `wang-tileset-snapshot-v1` | Canonical positional tile IDs and their square `N,E,S,W` colors | +| `wang-region-snapshot-v1` | Inclusive bounds, dense active mask, exposed boundary constraints, and no assignment | +| `wang-explain-manifest-v1` | Stage identity plus a basename, schema, and full SHA-256 digest for each artifact | + +The manifest is installed atomically only after its content-addressed artifacts +have been installed. Both the producer and the renderer reject duplicate JSON +members, non-finite numbers, unknown fields, invalid types, path traversal, +hash drift, mismatched formula identity, and region colors absent from the +referenced tileset. + +The committed example was produced from `tests/instances/pipeline_sat.cm13` and +lives in `tests/fixtures/pipeline_sat_explain/`. It is data, not a hand-edited +diagram. + +## Export from the real construction pipeline + +Build the shared native library, then parse and reduce one formula: + +```sh +make shared +uv run --frozen python tools/export_pipeline_snapshots.py \ + tests/instances/pipeline_sat.cm13 \ + /tmp/pipeline-sat-explain/manifest.json +``` + +The command loads the formula and constructs the real Yang–Zhang `Region` +through the scoped native adapter. It prints the manifest and three generated +artifact paths. It performs no solving. + +## Render each static stage + +From `renderer/`, pass the manifest to the existing Wang command and select a +view: + +```sh +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_explain/manifest.json \ + output/formula.png --view formula + +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_explain/manifest.json \ + output/tileset-square.png --view tileset + +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_explain/manifest.json \ + output/region-square.png --view region +``` + +The tile sheet and region also accept the explicit `--hex` flag. Their hex +data is not stored in JSON: the renderer applies the same pure Basire/Culik +port and raster-independent checker used for verified solutions. + +```sh +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_explain/manifest.json \ + output/tileset-hex.png --view tileset --hex + +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_explain/manifest.json \ + output/region-hex.png --view region --hex +``` + +The region view deliberately contains no tiles: pale cells are active +positions, crossed cells are outside the region, and colored bands are exposed +boundary constraints. The adjacent formula panel states exactly which parsed +formula the region simulates. + +## Render the final verified witness + +The default solution image remains byte-for-byte compatible. Explainability is +opt-in: + +```sh +uv run --locked python wang_square.py \ + ../tests/fixtures/wang_solution_v1_square_sat.json \ + output/solution-explain.png --explain + +uv run --locked python wang_square.py \ + ../tests/fixtures/wang_solution_v1_square_sat.json \ + output/solution-explain-hex.png --explain --hex +``` + +Every tile shows its positional ID. Each logical edge color has a deterministic +RGB band, exposed constraints receive a heavier outer stroke, and the legend +retains the numeric color identity. The hex view also labels the fresh +presentation color `kappa = max(C) + 1`. + +## Correctness and current scope + +The static contracts stop at the constructed region. They contain neither +solver events nor a partial assignment. Deterministic event traces, replayed +partial states, and algorithm-specific ordering require a separate trace +contract because native DFS and Z3 do not expose the same kind of step. + +The producer is standard-library-only and depends on copied immutable models. +The renderer independently consumes the JSON without importing `libwang.so`, +native adapters, or Z3. Golden PNGs cover all five static geometry/view pairs +and both explainable final-solution modes. The old square and hex solution +goldens remain unchanged when `--explain` is absent. + +Rendering still does not prove SAT, region validity, or witness validity. Those +obligations remain with construction tests, the independent verifier, the +solution exporter, and the square-to-hex checker described by their respective +contracts. diff --git a/python/formats/pipeline_snapshot.py b/python/formats/pipeline_snapshot.py new file mode 100644 index 0000000..b4e1f28 --- /dev/null +++ b/python/formats/pipeline_snapshot.py @@ -0,0 +1,780 @@ +"""Versioned static snapshots for explainable Wang pipeline stages. + +The producer is standard-library-only. It converts the immutable Python +formula, tileset, and region models into closed JSON documents and installs a +manifest only after all content-addressed artifacts have been written. The +snapshots carry presentation-neutral semantics; raster layout remains the +isolated renderer's responsibility. +""" + +from __future__ import annotations + +import hashlib +import json +import os +from pathlib import Path +import re +import tempfile +from typing import Final + +from model.formula import Formula +from model.region import Region +from model.tileset import COLOR_NONE, TILESET, Tileset + + +FORMULA_SCHEMA: Final = "cm13-formula-snapshot-v1" +TILESET_SCHEMA: Final = "wang-tileset-snapshot-v1" +REGION_SCHEMA: Final = "wang-region-snapshot-v1" +MANIFEST_SCHEMA: Final = "wang-explain-manifest-v1" +GEOMETRY: Final = "square" +STAGE: Final = "region" +DIRECTIONS: Final = ("N", "E", "S", "W") +_OFFSETS: Final = ((0, -1), (1, 0), (0, 1), (-1, 0)) +_SHA256_PATTERN: Final = re.compile(r"[0-9a-f]{64}") + + +class PipelineSnapshotError(ValueError): + """Raised when a static snapshot is malformed or cannot be installed.""" + + +def _fail(path: str, message: str) -> None: + raise PipelineSnapshotError(f"{path}: {message}") + + +def _require_object(value: object, path: str) -> dict[str, object]: + if type(value) is not dict: + _fail(path, "must be an object") + return value + + +def _require_array(value: object, path: str) -> list[object]: + if type(value) is not list: + _fail(path, "must be an array") + return value + + +def _require_string(value: object, path: str) -> str: + if type(value) is not str: + _fail(path, "must be a string") + try: + value.encode("utf-8") + except UnicodeEncodeError as error: + raise PipelineSnapshotError( + f"{path}: must contain valid UTF-8 text" + ) from error + return value + + +def _require_integer( + value: object, + path: str, + *, + nonnegative: bool, +) -> int: + if type(value) is not int: + _fail(path, "must be an integer") + if nonnegative and value < 0: + _fail(path, "must be nonnegative") + return value + + +def _require_exact_fields( + value: dict[str, object], + expected: frozenset[str], + path: str, +) -> None: + if any(type(key) is not str for key in value): + _fail(path, "object member names must be strings") + actual = frozenset(value) + missing = sorted(expected - actual) + extra = sorted(actual - expected) + if missing: + _fail(path, f"missing fields: {', '.join(missing)}") + if extra: + _fail(path, f"unknown fields: {', '.join(extra)}") + + +def _require_literal( + value: object, + expected: str, + path: str, +) -> None: + if _require_string(value, path) != expected: + _fail(path, f"must equal {expected!r}") + + +def _require_sha256(value: object, path: str) -> str: + digest = _require_string(value, path) + if _SHA256_PATTERN.fullmatch(digest) is None: + _fail(path, "must be a lowercase SHA-256 digest") + return digest + + +def _require_artifact_name(value: object, path: str) -> str: + name = _require_string(value, path) + if ( + not name + or name in {".", ".."} + or Path(name).name != name + or "/" in name + or "\\" in name + ): + _fail(path, "must be a nonempty artifact basename") + return name + + +def _validate_edges( + value: object, + path: str, + *, + optional: bool, +) -> tuple[int | None, int | None, int | None, int | None]: + edges = _require_object(value, path) + _require_exact_fields(edges, frozenset(DIRECTIONS), path) + checked: list[int | None] = [] + for direction in DIRECTIONS: + color = edges[direction] + if optional and color is None: + checked.append(None) + else: + checked.append( + _require_integer( + color, + f"{path}.{direction}", + nonnegative=True, + ) + ) + return tuple(checked) + + +def validate_formula_snapshot(document: object) -> None: + """Validate one closed parsed-formula snapshot.""" + root = _require_object(document, "$") + _require_exact_fields( + root, + frozenset({"schema", "source", "variable_count", "clauses"}), + "$", + ) + _require_literal(root["schema"], FORMULA_SCHEMA, "$.schema") + + source = _require_object(root["source"], "$.source") + _require_exact_fields(source, frozenset({"name", "sha256"}), "$.source") + _require_artifact_name(source["name"], "$.source.name") + _require_sha256(source["sha256"], "$.source.sha256") + + variable_count = _require_integer( + root["variable_count"], + "$.variable_count", + nonnegative=True, + ) + if variable_count == 0: + _fail("$.variable_count", "must be positive") + + clauses = _require_array(root["clauses"], "$.clauses") + if len(clauses) != variable_count: + _fail( + "$.clauses", + "length must equal variable_count for a cubic CM1-in-3 formula", + ) + occurrences = [0] * variable_count + for clause_id, raw_clause in enumerate(clauses): + path = f"$.clauses[{clause_id}]" + clause = _require_object(raw_clause, path) + _require_exact_fields( + clause, + frozenset({"clause_id", "variables"}), + path, + ) + actual_id = _require_integer( + clause["clause_id"], + f"{path}.clause_id", + nonnegative=True, + ) + if actual_id != clause_id: + _fail( + f"{path}.clause_id", + f"must equal canonical position {clause_id}", + ) + variables = _require_array(clause["variables"], f"{path}.variables") + if len(variables) != 3: + _fail(f"{path}.variables", "must preserve exactly three positions") + for position, raw_variable in enumerate(variables): + variable = _require_integer( + raw_variable, + f"{path}.variables[{position}]", + nonnegative=True, + ) + if variable >= variable_count: + _fail( + f"{path}.variables[{position}]", + "is outside the canonical variable domain", + ) + occurrences[variable] += 1 + if any(count != 3 for count in occurrences): + _fail("$.clauses", "every variable must occur exactly three times") + + +def validate_tileset_snapshot(document: object) -> None: + """Validate one canonical square-tileset snapshot.""" + root = _require_object(document, "$") + _require_exact_fields( + root, + frozenset({"schema", "geometry", "directions", "colors", "tiles"}), + "$", + ) + _require_literal(root["schema"], TILESET_SCHEMA, "$.schema") + _require_literal(root["geometry"], GEOMETRY, "$.geometry") + + directions = _require_array(root["directions"], "$.directions") + if directions != list(DIRECTIONS): + _fail("$.directions", f"must equal {list(DIRECTIONS)!r}") + + colors = _require_array(root["colors"], "$.colors") + checked_colors = [ + _require_integer(color, f"$.colors[{index}]", nonnegative=True) + for index, color in enumerate(colors) + ] + if not checked_colors: + _fail("$.colors", "must not be empty") + if checked_colors != sorted(set(checked_colors)): + _fail("$.colors", "must be strictly increasing and unique") + + tiles = _require_array(root["tiles"], "$.tiles") + if not tiles: + _fail("$.tiles", "must not be empty") + used_colors: set[int] = set() + for expected_id, raw_tile in enumerate(tiles): + path = f"$.tiles[{expected_id}]" + tile = _require_object(raw_tile, path) + _require_exact_fields(tile, frozenset({"tile_id", "edges"}), path) + tile_id = _require_integer( + tile["tile_id"], + f"{path}.tile_id", + nonnegative=True, + ) + if tile_id != expected_id: + _fail( + f"{path}.tile_id", + f"must equal canonical table position {expected_id}", + ) + used_colors.update( + _validate_edges( + tile["edges"], + f"{path}.edges", + optional=False, + ) + ) + if checked_colors != sorted(used_colors): + _fail("$.colors", "must equal exactly the colors used by the tile table") + + +def validate_region_snapshot(document: object) -> None: + """Validate square-region geometry and exposed boundary constraints.""" + root = _require_object(document, "$") + _require_exact_fields( + root, + frozenset( + { + "schema", + "geometry", + "source_formula_sha256", + "bounds", + "active", + "boundary", + } + ), + "$", + ) + _require_literal(root["schema"], REGION_SCHEMA, "$.schema") + _require_literal(root["geometry"], GEOMETRY, "$.geometry") + _require_sha256(root["source_formula_sha256"], "$.source_formula_sha256") + + bounds = _require_object(root["bounds"], "$.bounds") + bound_fields = frozenset( + { + "min_x_inclusive", + "min_y_inclusive", + "max_x_inclusive", + "max_y_inclusive", + } + ) + _require_exact_fields(bounds, bound_fields, "$.bounds") + min_x = _require_integer( + bounds["min_x_inclusive"], + "$.bounds.min_x_inclusive", + nonnegative=False, + ) + min_y = _require_integer( + bounds["min_y_inclusive"], + "$.bounds.min_y_inclusive", + nonnegative=False, + ) + max_x = _require_integer( + bounds["max_x_inclusive"], + "$.bounds.max_x_inclusive", + nonnegative=False, + ) + max_y = _require_integer( + bounds["max_y_inclusive"], + "$.bounds.max_y_inclusive", + nonnegative=False, + ) + if max_x < min_x or max_y < min_y: + _fail("$.bounds", "inclusive maxima must not precede minima") + width = max_x - min_x + 1 + height = max_y - min_y + 1 + area = width * height + + active = _require_array(root["active"], "$.active") + boundary = _require_array(root["boundary"], "$.boundary") + if len(active) != area: + _fail("$.active", f"length must equal inclusive bounds area {area}") + if len(boundary) != area: + _fail("$.boundary", f"length must equal inclusive bounds area {area}") + if any(type(value) is not bool for value in active): + _fail("$.active", "must contain only booleans") + if not any(active): + _fail("$.active", "must contain at least one active cell") + + checked_boundary: list[ + tuple[int | None, int | None, int | None, int | None] | None + ] = [] + for index, raw_sides in enumerate(boundary): + if not active[index]: + if raw_sides is not None: + _fail( + f"$.boundary[{index}]", + "must be null for an inactive position", + ) + checked_boundary.append(None) + continue + if raw_sides is None: + _fail( + f"$.boundary[{index}]", + "must contain N/E/S/W entries for an active cell", + ) + checked_boundary.append( + _validate_edges( + raw_sides, + f"$.boundary[{index}]", + optional=True, + ) + ) + + for index, is_active in enumerate(active): + if not is_active: + continue + sides = checked_boundary[index] + assert sides is not None + x = index % width + y = index // width + for direction, (dx, dy) in enumerate(_OFFSETS): + neighbor_x = x + dx + neighbor_y = y + dy + neighbor_active = False + if 0 <= neighbor_x < width and 0 <= neighbor_y < height: + neighbor_active = active[neighbor_y * width + neighbor_x] + if neighbor_active and sides[direction] is not None: + _fail( + f"$.boundary[{index}].{DIRECTIONS[direction]}", + "must be null on an edge shared by active cells", + ) + + +def _validate_reference( + value: object, + path: str, + *, + expected_schema: str, +) -> tuple[str, str]: + reference = _require_object(value, path) + _require_exact_fields( + reference, + frozenset({"path", "sha256", "schema"}), + path, + ) + name = _require_artifact_name(reference["path"], f"{path}.path") + digest = _require_sha256(reference["sha256"], f"{path}.sha256") + _require_literal(reference["schema"], expected_schema, f"{path}.schema") + return name, digest + + +def validate_explain_manifest(document: object) -> None: + """Validate the closed manifest structure without loading artifacts.""" + root = _require_object(document, "$") + _require_exact_fields( + root, + frozenset({"schema", "stage", "source_formula_sha256", "artifacts"}), + "$", + ) + _require_literal(root["schema"], MANIFEST_SCHEMA, "$.schema") + _require_literal(root["stage"], STAGE, "$.stage") + _require_sha256(root["source_formula_sha256"], "$.source_formula_sha256") + artifacts = _require_object(root["artifacts"], "$.artifacts") + _require_exact_fields( + artifacts, + frozenset({"formula", "tileset", "region"}), + "$.artifacts", + ) + for name, schema in ( + ("formula", FORMULA_SCHEMA), + ("tileset", TILESET_SCHEMA), + ("region", REGION_SCHEMA), + ): + _validate_reference( + artifacts[name], + f"$.artifacts.{name}", + expected_schema=schema, + ) + + +def _reject_duplicate_members( + pairs: list[tuple[str, object]], +) -> dict[str, object]: + result: dict[str, object] = {} + for key, value in pairs: + if key in result: + raise PipelineSnapshotError( + f"JSON object contains duplicate member {key!r}" + ) + result[key] = value + return result + + +def _reject_nonfinite_constant(value: str) -> None: + raise PipelineSnapshotError( + f"JSON document contains non-finite number {value}" + ) + + +def _load_json_bytes(encoded: bytes, label: str) -> dict[str, object]: + try: + decoded = encoded.decode("utf-8") + except UnicodeDecodeError as error: + raise PipelineSnapshotError(f"{label}: is not valid UTF-8") from error + try: + document = json.loads( + decoded, + object_pairs_hook=_reject_duplicate_members, + parse_constant=_reject_nonfinite_constant, + ) + except json.JSONDecodeError as error: + raise PipelineSnapshotError( + f"{label}: invalid JSON at line {error.lineno}, " + f"column {error.colno}: {error.msg}" + ) from error + except (ValueError, RecursionError) as error: + if isinstance(error, PipelineSnapshotError): + raise + raise PipelineSnapshotError(f"{label}: invalid JSON value: {error}") from error + return _require_object(document, label) + + +def load_pipeline_snapshot(path: str | Path) -> dict[str, object]: + """Strictly load and validate any static snapshot document.""" + source = Path(path) + try: + encoded = source.read_bytes() + except OSError as error: + raise PipelineSnapshotError( + f"cannot read snapshot {source!s}: {error}" + ) from error + document = _load_json_bytes(encoded, str(source)) + schema = document.get("schema") + if type(schema) is not str: + _fail("$.schema", "must be a string") + validators = { + FORMULA_SCHEMA: validate_formula_snapshot, + TILESET_SCHEMA: validate_tileset_snapshot, + REGION_SCHEMA: validate_region_snapshot, + MANIFEST_SCHEMA: validate_explain_manifest, + } + validator = validators.get(schema) + if validator is None: + _fail("$.schema", "is not a supported static snapshot schema") + validator(document) + return document + + +def load_explainability_bundle( + manifest_path: str | Path, +) -> tuple[ + dict[str, object], + dict[str, object], + dict[str, object], + dict[str, object], +]: + """Load a manifest and its three hash-bound artifacts.""" + path = Path(manifest_path) + manifest = load_pipeline_snapshot(path) + if manifest["schema"] != MANIFEST_SCHEMA: + _fail("$.schema", f"must equal {MANIFEST_SCHEMA!r}") + artifacts = _require_object(manifest["artifacts"], "$.artifacts") + loaded: dict[str, dict[str, object]] = {} + for name, schema in ( + ("formula", FORMULA_SCHEMA), + ("tileset", TILESET_SCHEMA), + ("region", REGION_SCHEMA), + ): + reference = _require_object(artifacts[name], f"$.artifacts.{name}") + artifact_name, expected_digest = _validate_reference( + reference, + f"$.artifacts.{name}", + expected_schema=schema, + ) + artifact_path = path.parent / artifact_name + try: + encoded = artifact_path.read_bytes() + except OSError as error: + raise PipelineSnapshotError( + f"cannot read {name} artifact {artifact_path!s}: {error}" + ) from error + actual_digest = hashlib.sha256(encoded).hexdigest() + if actual_digest != expected_digest: + _fail( + f"$.artifacts.{name}.sha256", + f"does not match {artifact_name}", + ) + document = _load_json_bytes(encoded, str(artifact_path)) + if document.get("schema") != schema: + _fail(f"$.artifacts.{name}.schema", "does not match artifact") + { + FORMULA_SCHEMA: validate_formula_snapshot, + TILESET_SCHEMA: validate_tileset_snapshot, + REGION_SCHEMA: validate_region_snapshot, + }[schema](document) + loaded[name] = document + + formula = loaded["formula"] + region = loaded["region"] + tileset = loaded["tileset"] + formula_source = _require_object(formula["source"], "formula.source") + source_digest = _require_sha256( + manifest["source_formula_sha256"], + "$.source_formula_sha256", + ) + if formula_source["sha256"] != source_digest: + _fail("$.source_formula_sha256", "does not match formula artifact") + if region["source_formula_sha256"] != source_digest: + _fail("$.source_formula_sha256", "does not match region artifact") + + colors = set(_require_array(tileset["colors"], "tileset.colors")) + for index, raw_sides in enumerate( + _require_array(region["boundary"], "region.boundary") + ): + if raw_sides is None: + continue + sides = _require_object(raw_sides, f"region.boundary[{index}]") + for direction in DIRECTIONS: + color = sides[direction] + if color is not None and color not in colors: + _fail( + f"region.boundary[{index}].{direction}", + "is absent from the referenced tileset color set", + ) + return manifest, formula, tileset, region + + +def build_formula_snapshot( + formula: Formula, + *, + source_name: str, + source_sha256: str, +) -> dict[str, object]: + """Build one parsed-formula snapshot from an immutable model.""" + if not isinstance(formula, Formula): + raise TypeError("formula must be a Formula") + _require_artifact_name(source_name, "source_name") + _require_sha256(source_sha256, "source_sha256") + document: dict[str, object] = { + "schema": FORMULA_SCHEMA, + "source": {"name": source_name, "sha256": source_sha256}, + "variable_count": formula.variable_count, + "clauses": [ + {"clause_id": clause_id, "variables": list(clause)} + for clause_id, clause in enumerate(formula.clauses) + ], + } + validate_formula_snapshot(document) + return document + + +def build_tileset_snapshot( + tileset: Tileset = TILESET, +) -> dict[str, object]: + """Build one positional square-tileset snapshot.""" + if type(tileset) is not tuple or not tileset: + raise TypeError("tileset must be a nonempty tuple") + if any( + type(tile) is not tuple + or len(tile) != len(DIRECTIONS) + or any(type(color) is not int or color < 0 for color in tile) + for tile in tileset + ): + raise TypeError( + "every tile must be an immutable N/E/S/W tuple of " + "nonnegative integer colors" + ) + document: dict[str, object] = { + "schema": TILESET_SCHEMA, + "geometry": GEOMETRY, + "directions": list(DIRECTIONS), + "colors": sorted({color for tile in tileset for color in tile}), + "tiles": [ + { + "tile_id": tile_id, + "edges": { + direction: tile[direction_index] + for direction_index, direction in enumerate(DIRECTIONS) + }, + } + for tile_id, tile in enumerate(tileset) + ], + } + validate_tileset_snapshot(document) + return document + + +def build_region_snapshot( + region: Region, + *, + source_formula_sha256: str, + origin: tuple[int, int] = (0, 0), +) -> dict[str, object]: + """Build one unassigned square-region snapshot.""" + if not isinstance(region, Region): + raise TypeError("region must be a Region") + _require_sha256(source_formula_sha256, "source_formula_sha256") + if ( + type(origin) is not tuple + or len(origin) != 2 + or any(type(coordinate) is not int for coordinate in origin) + ): + raise PipelineSnapshotError( + "origin must be an immutable pair of integer coordinates" + ) + min_x, min_y = origin + boundary = [ + None + if not active + else { + direction: None if color == COLOR_NONE else color + for direction, color in zip(DIRECTIONS, sides, strict=True) + } + for active, sides in zip(region.active, region.boundary, strict=True) + ] + document: dict[str, object] = { + "schema": REGION_SCHEMA, + "geometry": GEOMETRY, + "source_formula_sha256": source_formula_sha256, + "bounds": { + "min_x_inclusive": min_x, + "min_y_inclusive": min_y, + "max_x_inclusive": min_x + region.width - 1, + "max_y_inclusive": min_y + region.height - 1, + }, + "active": list(region.active), + "boundary": boundary, + } + validate_region_snapshot(document) + return document + + +def _encode_document(document: dict[str, object]) -> bytes: + serialized = json.dumps( + document, + ensure_ascii=False, + allow_nan=False, + indent=2, + ) + return f"{serialized}\n".encode("utf-8") + + +def _write_atomic(path: Path, encoded: bytes) -> None: + temporary: Path | None = None + try: + with tempfile.NamedTemporaryFile( + mode="wb", + dir=path.parent, + prefix=f".{path.name}.", + suffix=".tmp", + delete=False, + ) as stream: + temporary = Path(stream.name) + stream.write(encoded) + os.replace(temporary, path) + temporary = None + except OSError as error: + raise PipelineSnapshotError( + f"cannot install snapshot {path!s}: {error}" + ) from error + finally: + if temporary is not None: + try: + temporary.unlink() + except FileNotFoundError: + pass + + +def dump_pipeline_snapshots( + manifest_path: str | Path, + source_path: str | Path, + formula: Formula, + region: Region, + *, + origin: tuple[int, int] = (0, 0), +) -> Path: + """Write content-addressed artifacts, then atomically install a manifest.""" + destination = Path(manifest_path) + source = Path(source_path) + try: + source_bytes = source.read_bytes() + except OSError as error: + raise PipelineSnapshotError( + f"cannot read formula source {source!s}: {error}" + ) from error + source_digest = hashlib.sha256(source_bytes).hexdigest() + formula_document = build_formula_snapshot( + formula, + source_name=source.name, + source_sha256=source_digest, + ) + tileset_document = build_tileset_snapshot() + region_document = build_region_snapshot( + region, + source_formula_sha256=source_digest, + origin=origin, + ) + documents = { + "formula": (FORMULA_SCHEMA, formula_document), + "tileset": (TILESET_SCHEMA, tileset_document), + "region": (REGION_SCHEMA, region_document), + } + references: dict[str, object] = {} + for name, (schema, document) in documents.items(): + encoded = _encode_document(document) + digest = hashlib.sha256(encoded).hexdigest() + artifact_name = f"{name}-{digest}.json" + if artifact_name == destination.name: + raise PipelineSnapshotError( + "manifest filename must not collide with a generated " + f"artifact: {artifact_name}" + ) + artifact_path = destination.parent / artifact_name + _write_atomic(artifact_path, encoded) + references[name] = { + "path": artifact_name, + "sha256": digest, + "schema": schema, + } + + manifest: dict[str, object] = { + "schema": MANIFEST_SCHEMA, + "stage": STAGE, + "source_formula_sha256": source_digest, + "artifacts": references, + } + validate_explain_manifest(manifest) + _write_atomic(destination, _encode_document(manifest)) + load_explainability_bundle(destination) + return destination diff --git a/renderer/README.md b/renderer/README.md index 97b2978..92edf95 100644 --- a/renderer/README.md +++ b/renderer/README.md @@ -82,6 +82,42 @@ byte-for-byte unchanged. A successful PNG is presentation, not a proof; correctness remains the responsibility of the independent Tiling Foundry verifier before export. +Add `--explain` to a verified solution to show a neutral tile center, its +positional tile ID, colored `N,E,S,W` (or six hex) edge bands, emphasized +exposed boundary constraints, and the numeric palette legend: + +```bash +uv run --locked python wang_square.py \ + ../tests/fixtures/wang_solution_v1_square_sat.json \ + output/wang-square-explain.png \ + --explain +``` + +Static pre-solver views consume a `wang-explain-manifest-v1` instead of a +solution. They are inherently explanatory, so they do not use `--explain`: + +```bash +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_explain/manifest.json \ + output/formula.png \ + --view formula + +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_explain/manifest.json \ + output/tileset.png \ + --view tileset + +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_explain/manifest.json \ + output/region.png \ + --view region +``` + +`--view tileset` and `--view region` also accept `--hex`. Both invoke the pure +square-to-hex reducer and checker before rasterization. Formula view rejects +`--hex`; region view intentionally contains no assignment or partial solver +state. + ## Input Format ### palette.json @@ -228,8 +264,11 @@ Raises `RenderingException` on pipeline errors. ├── tests.py # Test suite (144 tests, all passing) ├── wang_square.py # One Wang CLI: square default, explicit hex raster ├── wang_hex_port.py # Pure square-to-hex reducer and independent checker +├── wang_snapshot.py # Strict static-snapshot consumer and view compositor +├── wang_explain.py # Shared colored-edge and legend drawing primitives ├── test_wang_square.py # Square loader, raster, isolation, CLI, and failures ├── test_wang_hex.py # Port proof obligations, hex raster, golden, and CLI +├── test_wang_snapshot.py # Snapshot contracts, views, isolation, and goldens ├── input/ # Example input files (palette, scene, tiles, sprites) ├── output/ # Rendered PNG output goes here ├── test_data/ @@ -250,9 +289,10 @@ Raises `RenderingException` on pipeline errors. uv run --locked pytest -q ``` -The complete isolated suite has 213 tests: the 144 preserved legacy tests -below, 45 Wang square tests, and 24 square-to-hex/hex-raster tests. To run only -the original upstream suite: +The complete isolated suite has 234 tests: the 144 preserved legacy tests +below, 45 Wang square tests, 24 square-to-hex/hex-raster tests, and 21 static +snapshot/explainability tests. +To run only the original upstream suite: ```bash uv run --locked pytest tests.py -v diff --git a/renderer/UPSTREAM.md b/renderer/UPSTREAM.md index ebacbd5..c488675 100644 --- a/renderer/UPSTREAM.md +++ b/renderer/UPSTREAM.md @@ -21,10 +21,11 @@ tests. The overall and affected section totals now say 144, 18 Palette, 33 SceneParser, and 49 Blitter tests. This `UPSTREAM.md` file is local provenance, not an upstream file. -Tiling Foundry later added `wang_square.py`, `wang_hex_port.py`, their two test -modules, and square/hex goldens under `test_data/`, plus clearly separated -usage notes in `README.md`. These additions consume `wang-solution-v1` as -presentation data and do not modify or import the legacy PAP modules. They +Tiling Foundry later added its isolated Wang modules, tests, and goldens under +`test_data/`, plus clearly separated usage notes in `README.md`. The default +and explainable solution paths consume `wang-solution-v1`; the static formula, +tile-sheet, and unassigned-region views consume a hash-bound explainability +manifest. These additions do not modify or import the legacy PAP modules. They also leave `pyproject.toml`, `uv.lock`, and the pinned dependencies unchanged. ## Verification @@ -42,9 +43,10 @@ uv run --locked pytest -q ``` The import baseline remains 144 collected tests and 144 passing tests. The -combined local suite is 213 tests: 144 preserved legacy tests, 45 Wang square -tests, and 24 square-to-hex/hex-raster tests. Keep the renderer environment -under `renderer/.venv`; its local `.gitignore` excludes that environment and +combined local suite is 234 tests: 144 preserved legacy tests, 45 Wang square +tests, 24 square-to-hex/hex-raster tests, and 21 static +snapshot/explainability tests. Keep the renderer environment under +`renderer/.venv`; its local `.gitignore` excludes that environment and generated Python/build files. The preserved `renderer/.github/workflows/ci.yml` is nested upstream evidence; diff --git a/renderer/test_data/pipeline_sat_formula.png b/renderer/test_data/pipeline_sat_formula.png new file mode 100644 index 0000000..b7592ad Binary files /dev/null and b/renderer/test_data/pipeline_sat_formula.png differ diff --git a/renderer/test_data/pipeline_sat_region_hex.png b/renderer/test_data/pipeline_sat_region_hex.png new file mode 100644 index 0000000..9ecfedc Binary files /dev/null and b/renderer/test_data/pipeline_sat_region_hex.png differ diff --git a/renderer/test_data/pipeline_sat_region_square.png b/renderer/test_data/pipeline_sat_region_square.png new file mode 100644 index 0000000..7568104 Binary files /dev/null and b/renderer/test_data/pipeline_sat_region_square.png differ diff --git a/renderer/test_data/pipeline_sat_tileset_hex.png b/renderer/test_data/pipeline_sat_tileset_hex.png new file mode 100644 index 0000000..734b545 Binary files /dev/null and b/renderer/test_data/pipeline_sat_tileset_hex.png differ diff --git a/renderer/test_data/pipeline_sat_tileset_square.png b/renderer/test_data/pipeline_sat_tileset_square.png new file mode 100644 index 0000000..5b2ab4f Binary files /dev/null and b/renderer/test_data/pipeline_sat_tileset_square.png differ diff --git a/renderer/test_data/wang_solution_v1_hex_explain.png b/renderer/test_data/wang_solution_v1_hex_explain.png new file mode 100644 index 0000000..0c69d56 Binary files /dev/null and b/renderer/test_data/wang_solution_v1_hex_explain.png differ diff --git a/renderer/test_data/wang_solution_v1_square_explain.png b/renderer/test_data/wang_solution_v1_square_explain.png new file mode 100644 index 0000000..11fab85 Binary files /dev/null and b/renderer/test_data/wang_solution_v1_square_explain.png differ diff --git a/renderer/test_wang_snapshot.py b/renderer/test_wang_snapshot.py new file mode 100644 index 0000000..3bcd880 --- /dev/null +++ b/renderer/test_wang_snapshot.py @@ -0,0 +1,309 @@ +"""Tests for static snapshots and opt-in explainability raster modes.""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys + +import numpy as np +from PIL import Image, ImageDraw +import pytest + +import wang_square +import wang_snapshot +from wang_explain import ( + EXPLAIN_ACTIVE_RGB, + EXPLAIN_OUTLINE_RGB, + draw_boundary_side, + hex_explain_tile, + square_explain_tile, + square_region_tile, +) +from wang_hex_port import WangSquareRenderError +from wang_snapshot import ( + FORMULA_SCHEMA, + MANIFEST_SCHEMA, + REGION_SCHEMA, + TILESET_SCHEMA, + load_explainability_bundle, + render_pipeline_snapshot, +) +from wang_square import ( + _build_palette_from_edges, + _hex_vertices, + render_wang_square, +) + + +RENDERER_DIR = Path(__file__).resolve().parent +ROOT = RENDERER_DIR.parent +SOLUTION = ROOT / "tests/fixtures/wang_solution_v1_square_sat.json" +SNAPSHOT_DIRECTORY = ROOT / "tests/fixtures/pipeline_sat_explain" +MANIFEST = SNAPSHOT_DIRECTORY / "manifest.json" +GOLDENS = { + ("formula", False): RENDERER_DIR / "test_data/pipeline_sat_formula.png", + ("tileset", False): RENDERER_DIR / "test_data/pipeline_sat_tileset_square.png", + ("tileset", True): RENDERER_DIR / "test_data/pipeline_sat_tileset_hex.png", + ("region", False): RENDERER_DIR / "test_data/pipeline_sat_region_square.png", + ("region", True): RENDERER_DIR / "test_data/pipeline_sat_region_hex.png", +} +SOLUTION_GOLDENS = { + False: RENDERER_DIR / "test_data/wang_solution_v1_square_explain.png", + True: RENDERER_DIR / "test_data/wang_solution_v1_hex_explain.png", +} + + +def test_loads_hash_bound_bundle_without_native_or_solver_imports(): + bundle = load_explainability_bundle(MANIFEST) + + assert bundle.formula.source_name == "pipeline_sat.cm13" + assert bundle.formula.variable_count == 3 + assert bundle.formula.clauses == ((0, 0, 1), (0, 1, 2), (1, 2, 2)) + assert len(bundle.tileset.tile_edges) == 23 + assert bundle.tileset.colors == tuple(range(16)) + assert (bundle.region.width, bundle.region.height) == (41, 11) + assert sum(bundle.region.active) == 444 + assert bundle.region.active.count(False) == 7 + assert "z3" not in sys.modules + assert "native._lib" not in sys.modules + + +def test_versioned_fixture_manifest_references_expected_closed_contracts(): + manifest = json.loads(MANIFEST.read_text(encoding="utf-8")) + + assert manifest["schema"] == MANIFEST_SCHEMA + assert manifest["stage"] == "region" + assert manifest["artifacts"]["formula"]["schema"] == FORMULA_SCHEMA + assert manifest["artifacts"]["tileset"]["schema"] == TILESET_SCHEMA + assert manifest["artifacts"]["region"]["schema"] == REGION_SCHEMA + for reference in manifest["artifacts"].values(): + encoded = (SNAPSHOT_DIRECTORY / reference["path"]).read_bytes() + assert hashlib.sha256(encoded).hexdigest() == reference["sha256"] + + +@pytest.mark.parametrize("view", ["tileset", "region"]) +def test_hex_snapshot_views_require_the_independent_port_checker( + tmp_path, + monkeypatch, + view, +): + def reject_port(_square, _candidate): + raise WangSquareRenderError("independent checker rejected candidate") + + monkeypatch.setattr(wang_snapshot, "check_square_to_hex", reject_port) + + with pytest.raises( + WangSquareRenderError, + match="independent checker rejected candidate", + ): + render_pipeline_snapshot( + MANIFEST, + tmp_path / f"{view}.png", + view=view, + hex_mode=True, + ) + + +def test_square_explain_asset_puts_each_logical_color_on_its_edge(): + edges = (10, 20, 30, 40) + palette = _build_palette_from_edges((edges,)) + asset = np.asarray( + square_explain_tile( + edges, + palette, + 64, + tile_id=3, + edge_labels=False, + ) + ) + + assert tuple(asset[1, 32]) == palette[10] + assert tuple(asset[32, 62]) == palette[20] + assert tuple(asset[62, 32]) == palette[30] + assert tuple(asset[32, 1]) == palette[40] + + +def test_hex_explain_asset_puts_eswwnwne_colors_on_sides(): + edges = (10, 20, 30, 40, 50, 60) + palette = _build_palette_from_edges((edges,)) + radius = 32 + vertices = _hex_vertices(radius, radius // 2) + asset = np.asarray( + hex_explain_tile( + edges, + palette, + radius, + vertices, + tile_id=4, + edge_labels=False, + ) + ) + midpoints = tuple( + ( + (vertices[(direction + 1) % 6][0] + vertices[(direction + 2) % 6][0]) + // 2, + (vertices[(direction + 1) % 6][1] + vertices[(direction + 2) % 6][1]) + // 2, + ) + for direction in range(6) + ) + + for direction, (x, y) in enumerate(midpoints): + assert tuple(asset[y, x]) == palette[edges[direction]] + + +def test_unassigned_region_asset_colors_only_constrained_edges(): + palette = _build_palette_from_edges(((10, 20, 30, 40),)) + asset = np.asarray( + square_region_tile(32, (10, None, 30, None), palette) + ) + + assert tuple(asset[1, 16]) == palette[10] + assert tuple(asset[30, 16]) == palette[30] + assert tuple(asset[16, 16]) == EXPLAIN_ACTIVE_RGB + + +def test_boundary_emphasis_keeps_a_colored_core_and_dark_backing(): + image = Image.new("RGB", (24, 24), (255, 255, 255)) + color = (10, 80, 190) + draw_boundary_side( + ImageDraw.Draw(image), + (3, 12), + (20, 12), + color, + width=2, + ) + pixels = np.asarray(image) + + assert tuple(pixels[12, 12]) == color + assert tuple(pixels[10, 12]) == EXPLAIN_OUTLINE_RGB + + +@pytest.mark.parametrize(("view", "hex_mode"), GOLDENS) +def test_snapshot_views_match_pixel_stable_goldens(tmp_path, view, hex_mode): + output = tmp_path / "render.png" + + render_pipeline_snapshot( + MANIFEST, + output, + view=view, + hex_mode=hex_mode, + ) + + assert output.read_bytes() == GOLDENS[(view, hex_mode)].read_bytes() + + +@pytest.mark.parametrize("hex_mode", (False, True)) +def test_solution_explain_views_match_separate_goldens(tmp_path, hex_mode): + output = tmp_path / "render.png" + + render_wang_square(SOLUTION, output, explain=True, hex_mode=hex_mode) + + assert output.read_bytes() == SOLUTION_GOLDENS[hex_mode].read_bytes() + with Image.open(output) as image: + assert image.mode == "RGB" + + +def test_default_solution_paths_remain_byte_identical_to_legacy_goldens(tmp_path): + expected = { + False: RENDERER_DIR / "test_data/wang_solution_v1_square_sat.png", + True: RENDERER_DIR / "test_data/wang_solution_v1_hex_sat.png", + } + for hex_mode in (False, True): + output = tmp_path / f"render-{hex_mode}.png" + render_wang_square(SOLUTION, output, hex_mode=hex_mode) + assert output.read_bytes() == expected[hex_mode].read_bytes() + + +def test_manifest_hash_failure_preserves_existing_output(tmp_path): + copied = tmp_path / "bundle" + shutil.copytree(SNAPSHOT_DIRECTORY, copied) + manifest = copied / "manifest.json" + document = json.loads(manifest.read_text(encoding="utf-8")) + formula = copied / document["artifacts"]["formula"]["path"] + formula.write_bytes(formula.read_bytes() + b" ") + output = tmp_path / "render.png" + output.write_bytes(b"previous output") + + with pytest.raises(WangSquareRenderError, match="does not match"): + render_pipeline_snapshot(manifest, output, view="formula") + + assert output.read_bytes() == b"previous output" + assert not list(tmp_path.glob(".render.png.*.png")) + + +def test_manifest_rejects_parent_path_and_duplicate_json_members(tmp_path): + document = json.loads(MANIFEST.read_text(encoding="utf-8")) + document["artifacts"]["formula"]["path"] = "../formula.json" + traversal = tmp_path / "traversal.json" + traversal.write_text(json.dumps(document), encoding="utf-8") + with pytest.raises(WangSquareRenderError, match="artifact basename"): + load_explainability_bundle(traversal) + + duplicate = tmp_path / "duplicate.json" + duplicate.write_text( + '{"schema":"wang-explain-manifest-v1","schema":"duplicate"}', + encoding="utf-8", + ) + with pytest.raises(WangSquareRenderError, match="duplicate member"): + load_explainability_bundle(duplicate) + + +def test_formula_view_rejects_hex_and_unknown_snapshot_view(tmp_path): + with pytest.raises(WangSquareRenderError, match="not meaningful"): + render_pipeline_snapshot( + MANIFEST, + tmp_path / "formula.png", + view="formula", + hex_mode=True, + ) + with pytest.raises(WangSquareRenderError, match="must be one of"): + render_pipeline_snapshot( + MANIFEST, + tmp_path / "unknown.png", + view="unknown", + ) + + +def test_cli_dispatches_snapshot_view_and_explain_solution(tmp_path): + snapshot_output = tmp_path / "snapshot.png" + wang_square.main( + [str(MANIFEST), str(snapshot_output), "--view", "tileset", "--hex"] + ) + assert snapshot_output.read_bytes() == GOLDENS[("tileset", True)].read_bytes() + + solution_output = tmp_path / "solution.png" + wang_square.main([str(SOLUTION), str(solution_output), "--explain"]) + assert solution_output.read_bytes() == SOLUTION_GOLDENS[False].read_bytes() + + +def test_snapshot_consumer_imports_in_isolated_renderer_process(): + script = f""" +import importlib.util +import sys +from pathlib import Path + +renderer = Path({str(RENDERER_DIR)!r}) +sys.path.insert(0, str(renderer)) +module_path = renderer / 'wang_snapshot.py' +spec = importlib.util.spec_from_file_location('isolated_wang_snapshot', module_path) +module = importlib.util.module_from_spec(spec) +sys.modules[spec.name] = module +spec.loader.exec_module(module) +bundle = module.load_explainability_bundle(Path({str(MANIFEST)!r})) +assert len(bundle.tileset.tile_edges) == 23 +assert 'z3' not in sys.modules +assert 'native._lib' not in sys.modules +""" + completed = subprocess.run( + [sys.executable, "-I", "-B", "-c", script], + cwd=RENDERER_DIR, + capture_output=True, + text=True, + check=False, + ) + assert completed.returncode == 0, completed.stderr diff --git a/renderer/wang_explain.py b/renderer/wang_explain.py new file mode 100644 index 0000000..0d9d2bf --- /dev/null +++ b/renderer/wang_explain.py @@ -0,0 +1,355 @@ +"""Shared drawing primitives for opt-in explainability views.""" + +from __future__ import annotations + +from collections.abc import Mapping, Sequence +from typing import Final + +import numpy as np +from PIL import Image, ImageDraw, ImageFont + + +EXPLAIN_FACE_RGB: Final = (244, 246, 249) +EXPLAIN_PANEL_RGB: Final = (255, 255, 255) +EXPLAIN_TEXT_RGB: Final = (24, 28, 36) +EXPLAIN_MUTED_RGB: Final = (88, 96, 112) +EXPLAIN_OUTLINE_RGB: Final = (28, 32, 40) +EXPLAIN_INACTIVE_LIGHT_RGB: Final = (226, 230, 236) +EXPLAIN_INACTIVE_DARK_RGB: Final = (190, 197, 207) +EXPLAIN_ACTIVE_RGB: Final = (238, 241, 246) + + +def explain_font(size: int) -> ImageFont.FreeTypeFont | ImageFont.ImageFont: + """Return Pillow's bundled deterministic font at an explicit size.""" + return ImageFont.load_default(size=max(8, size)) + + +def contrasting_text(rgb: tuple[int, int, int]) -> tuple[int, int, int]: + """Choose black or white text from integer relative luminance.""" + red, green, blue = rgb + luminance = 299 * red + 587 * green + 114 * blue + return (20, 22, 28) if luminance >= 145_000 else (250, 250, 250) + + +def centered_text( + draw: ImageDraw.ImageDraw, + box: tuple[int, int, int, int], + text: str, + *, + font: ImageFont.FreeTypeFont | ImageFont.ImageFont, + fill: tuple[int, int, int] = EXPLAIN_TEXT_RGB, +) -> None: + """Draw text centered in an inclusive integer box.""" + left, top, right, bottom = box + text_box = draw.textbbox((0, 0), text, font=font) + width = text_box[2] - text_box[0] + height = text_box[3] - text_box[1] + x = left + (right - left + 1 - width) // 2 - text_box[0] + y = top + (bottom - top + 1 - height) // 2 - text_box[1] + draw.text((x, y), text, font=font, fill=fill) + + +def draw_explain_heading( + draw: ImageDraw.ImageDraw, + origin: tuple[int, int], + *, + title: str, + subtitle: str, +) -> None: + """Draw the common two-line heading used by explainability views.""" + x, y = origin + draw.text((x, y), title, font=explain_font(20), fill=EXPLAIN_TEXT_RGB) + draw.text( + (x, y + 28), + subtitle, + font=explain_font(12), + fill=EXPLAIN_MUTED_RGB, + ) + + +def draw_inactive_key( + draw: ImageDraw.ImageDraw, + origin: tuple[int, int], +) -> None: + """Draw the shared legend key for an inactive bounding-box position.""" + x, y = origin + size = 20 + draw.rectangle( + (x, y, x + size, y + size), + fill=EXPLAIN_INACTIVE_LIGHT_RGB, + outline=EXPLAIN_INACTIVE_DARK_RGB, + ) + draw.line( + (x + 2, y + 2, x + size - 2, y + size - 2), + fill=EXPLAIN_TEXT_RGB, + ) + draw.line( + (x + size - 2, y + 2, x + 2, y + size - 2), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (x + size + 8, y + 1), + "inactive / outside region", + font=explain_font(12), + fill=EXPLAIN_TEXT_RGB, + ) + + +def square_explain_tile( + edges: tuple[int, int, int, int], + palette: Mapping[int, tuple[int, int, int]], + size: int, + *, + tile_id: int | None, + edge_labels: bool, +) -> Image.Image: + """Draw a neutral square face surrounded by four logical-color bands.""" + last = size - 1 + band = max(3, size // 9) + inner = band + asset = Image.new("RGB", (size, size), EXPLAIN_FACE_RGB) + draw = ImageDraw.Draw(asset) + polygons = ( + ((0, 0), (last, 0), (last - inner, inner), (inner, inner)), + ((last, 0), (last, last), (last - inner, last - inner), (last - inner, inner)), + ((last, last), (0, last), (inner, last - inner), (last - inner, last - inner)), + ((0, last), (0, 0), (inner, inner), (inner, last - inner)), + ) + for direction, color in enumerate(edges): + draw.polygon(polygons[direction], fill=palette[color]) + draw.rectangle( + (inner, inner, last - inner, last - inner), + outline=EXPLAIN_OUTLINE_RGB, + width=1, + ) + + if tile_id is not None: + centered_text( + draw, + (inner + 1, inner + 1, last - inner - 1, last - inner - 1), + str(tile_id), + font=explain_font(max(9, size // 4)), + ) + if edge_labels and size >= 56: + font = explain_font(max(8, size // 9)) + labels = ( + (str(edges[0]), (size // 2, band // 2)), + (str(edges[1]), (last - band // 2, size // 2)), + (str(edges[2]), (size // 2, last - band // 2)), + (str(edges[3]), (band // 2, size // 2)), + ) + for direction, (label, center) in enumerate(labels): + text_box = draw.textbbox((0, 0), label, font=font) + width = text_box[2] - text_box[0] + height = text_box[3] - text_box[1] + draw.text( + ( + center[0] - width // 2 - text_box[0], + center[1] - height // 2 - text_box[1], + ), + label, + font=font, + fill=contrasting_text(palette[edges[direction]]), + ) + return asset + + +def square_inactive_tile(size: int) -> Image.Image: + """Draw an explicitly inactive bounding-box position.""" + coordinates = np.arange(size, dtype=np.int32) + x = np.broadcast_to(coordinates, (size, size)) + y = x.T + checker_size = max(2, size // 6) + checker = ((x // checker_size) + (y // checker_size)) % 2 + colors = np.asarray( + (EXPLAIN_INACTIVE_LIGHT_RGB, EXPLAIN_INACTIVE_DARK_RGB), + dtype=np.uint8, + ) + asset = Image.fromarray(colors[checker], mode="RGB") + draw = ImageDraw.Draw(asset) + draw.rectangle((0, 0, size - 1, size - 1), outline=EXPLAIN_OUTLINE_RGB) + draw.line((2, 2, size - 3, size - 3), fill=EXPLAIN_OUTLINE_RGB, width=1) + draw.line((size - 3, 2, 2, size - 3), fill=EXPLAIN_OUTLINE_RGB, width=1) + return asset + + +def square_region_tile( + size: int, + boundary: tuple[int | None, int | None, int | None, int | None], + palette: Mapping[int, tuple[int, int, int]], +) -> Image.Image: + """Draw one unassigned active cell and its exposed boundary constraints.""" + asset = Image.new("RGB", (size, size), EXPLAIN_ACTIVE_RGB) + draw = ImageDraw.Draw(asset) + draw.rectangle((0, 0, size - 1, size - 1), outline=(174, 181, 193)) + band = max(3, size // 8) + sides = ( + (0, 0, size - 1, band - 1), + (size - band, 0, size - 1, size - 1), + (0, size - band, size - 1, size - 1), + (0, 0, band - 1, size - 1), + ) + for direction, color in enumerate(boundary): + if color is None: + continue + draw.rectangle(sides[direction], fill=palette[color]) + if direction == 0: + line = (0, 0, size - 1, 0) + elif direction == 1: + line = (size - 1, 0, size - 1, size - 1) + elif direction == 2: + line = (0, size - 1, size - 1, size - 1) + else: + line = (0, 0, 0, size - 1) + draw.line(line, fill=EXPLAIN_OUTLINE_RGB, width=1) + return asset + + +def hex_explain_tile( + edges: tuple[int, int, int, int, int, int], + palette: Mapping[int, tuple[int, int, int]], + radius: int, + vertices: tuple[tuple[int, int], ...], + *, + tile_id: int | None, + edge_labels: bool, +) -> Image.Image: + """Draw a pointy-top hex with explicit six-side logical-color bands.""" + size = 2 * radius + 1 + asset = Image.new("RGB", (size, size), EXPLAIN_FACE_RGB) + draw = ImageDraw.Draw(asset) + draw.polygon(vertices, fill=EXPLAIN_FACE_RGB) + width = max(3, radius // 5) + for direction, color in enumerate(edges): + first = vertices[(direction + 1) % 6] + second = vertices[(direction + 2) % 6] + draw.line((first, second), fill=EXPLAIN_OUTLINE_RGB, width=width + 2) + draw.line((first, second), fill=palette[color], width=width) + if tile_id is not None: + centered_text( + draw, + (radius // 2, radius // 2, radius + radius // 2, radius + radius // 2), + str(tile_id), + font=explain_font(max(9, radius // 2)), + ) + if edge_labels and radius >= 28: + font = explain_font(max(8, radius // 4)) + center = (radius, radius) + for direction, color in enumerate(edges): + first = vertices[(direction + 1) % 6] + second = vertices[(direction + 2) % 6] + midpoint = ((first[0] + second[0]) // 2, (first[1] + second[1]) // 2) + label_center = ( + (2 * midpoint[0] + center[0]) // 3, + (2 * midpoint[1] + center[1]) // 3, + ) + label = str(color) + text_box = draw.textbbox((0, 0), label, font=font) + draw.text( + ( + label_center[0] - (text_box[2] - text_box[0]) // 2, + label_center[1] - (text_box[3] - text_box[1]) // 2, + ), + label, + font=font, + fill=EXPLAIN_TEXT_RGB, + ) + return asset + + +def draw_boundary_side( + draw: ImageDraw.ImageDraw, + first: tuple[int, int], + second: tuple[int, int], + color: tuple[int, int, int], + *, + width: int, +) -> None: + """Highlight one exposed constraint with a black-backed colored stroke.""" + draw.line((first, second), fill=EXPLAIN_OUTLINE_RGB, width=width + 4) + draw.line((first, second), fill=color, width=width) + + +def draw_palette_legend( + draw: ImageDraw.ImageDraw, + palette: Mapping[int, tuple[int, int, int]], + origin: tuple[int, int], + *, + title: str = "Logical edge colors", + columns: int = 2, + font_size: int = 14, +) -> tuple[int, int]: + """Draw a numeric palette legend and return its occupied width/height.""" + font = explain_font(font_size) + title_font = explain_font(font_size + 2) + swatch = font_size + 2 + row_height = swatch + 6 + column_width = 82 + colors = sorted(palette) + rows = (len(colors) + columns - 1) // columns + x0, y0 = origin + draw.text((x0, y0), title, font=title_font, fill=EXPLAIN_TEXT_RGB) + title_box = draw.textbbox((x0, y0), title, font=title_font) + content_y = title_box[3] + 8 + for index, logical_color in enumerate(colors): + column = index // rows + row = index % rows + x = x0 + column * column_width + y = content_y + row * row_height + rgb = palette[logical_color] + draw.rectangle( + (x, y, x + swatch, y + swatch), + fill=rgb, + outline=EXPLAIN_OUTLINE_RGB, + ) + draw.text( + (x + swatch + 6, y), + str(logical_color), + font=font, + fill=EXPLAIN_TEXT_RGB, + ) + height = content_y - y0 + rows * row_height + return columns * column_width, height + + +def wrap_text( + draw: ImageDraw.ImageDraw, + text: str, + font: ImageFont.FreeTypeFont | ImageFont.ImageFont, + max_width: int, +) -> list[str]: + """Wrap words using measured Pillow widths without locale dependence.""" + words = text.split() + if not words: + return [""] + lines: list[str] = [] + current = words[0] + for word in words[1:]: + candidate = f"{current} {word}" + box = draw.textbbox((0, 0), candidate, font=font) + if box[2] - box[0] <= max_width: + current = candidate + else: + lines.append(current) + current = word + lines.append(current) + return lines + + +def draw_lines( + draw: ImageDraw.ImageDraw, + lines: Sequence[str], + origin: tuple[int, int], + *, + font: ImageFont.FreeTypeFont | ImageFont.ImageFont, + fill: tuple[int, int, int] = EXPLAIN_TEXT_RGB, + spacing: int = 5, +) -> int: + """Draw lines and return the first unused y coordinate.""" + x, y = origin + sample = draw.textbbox((0, 0), "Ag", font=font) + line_height = sample[3] - sample[1] + spacing + for line in lines: + draw.text((x, y), line, font=font, fill=fill) + y += line_height + return y diff --git a/renderer/wang_snapshot.py b/renderer/wang_snapshot.py new file mode 100644 index 0000000..d88cab1 --- /dev/null +++ b/renderer/wang_snapshot.py @@ -0,0 +1,984 @@ +"""Strict consumer and raster views for static explainability snapshots.""" + +from __future__ import annotations + +from dataclasses import dataclass +import hashlib +import json +from pathlib import Path +import re +from typing import Final + +import numpy as np +from PIL import Image, ImageDraw + +from wang_explain import ( + EXPLAIN_ACTIVE_RGB, + EXPLAIN_MUTED_RGB, + EXPLAIN_OUTLINE_RGB, + EXPLAIN_PANEL_RGB, + EXPLAIN_TEXT_RGB, + draw_boundary_side, + draw_explain_heading, + draw_inactive_key, + draw_lines, + draw_palette_legend, + explain_font, + hex_explain_tile, + square_explain_tile, + square_inactive_tile, + square_region_tile, + wrap_text, +) +from wang_hex_port import ( + WangHexPort, + WangPresentation, + WangSquareRenderError, + check_square_to_hex, + reduce_square_to_hex, +) +from wang_square import ( + DEFAULT_MARGIN, + DEFAULT_PIXELS_PER_CELL, + MAX_MARGIN, + MAX_PIXELS_PER_CELL, + MIN_PIXELS_PER_CELL, + _build_palette_from_edges, + _check_canvas_limits, + _hex_mask, + _hex_vertices, + _render_integer, + _save_png_atomic, +) + + +FORMULA_SCHEMA: Final = "cm13-formula-snapshot-v1" +TILESET_SCHEMA: Final = "wang-tileset-snapshot-v1" +REGION_SCHEMA: Final = "wang-region-snapshot-v1" +MANIFEST_SCHEMA: Final = "wang-explain-manifest-v1" +DIRECTIONS: Final = ("N", "E", "S", "W") +HEX_DIRECTIONS: Final = ("E", "SE", "SW", "W", "NW", "NE") +_SHA256_PATTERN: Final = re.compile(r"[0-9a-f]{64}") +_FORMULA_PANEL_WIDTH: Final = 360 +_LEGEND_WIDTH: Final = 190 +_PANEL_GAP: Final = 20 +_HEADER_HEIGHT: Final = 58 + + +@dataclass(frozen=True, slots=True) +class FormulaSnapshot: + source_name: str + source_sha256: str + variable_count: int + clauses: tuple[tuple[int, int, int], ...] + + +@dataclass(frozen=True, slots=True) +class TilesetSnapshot: + colors: tuple[int, ...] + tile_edges: tuple[tuple[int, int, int, int], ...] + + +@dataclass(frozen=True, slots=True) +class RegionSnapshot: + min_x: int + min_y: int + max_x: int + max_y: int + source_formula_sha256: str + active: tuple[bool, ...] + boundary: tuple[ + tuple[int | None, int | None, int | None, int | None] | None, + ..., + ] + + @property + def width(self) -> int: + return self.max_x - self.min_x + 1 + + @property + def height(self) -> int: + return self.max_y - self.min_y + 1 + + +@dataclass(frozen=True, slots=True) +class ExplainabilityBundle: + source_formula_sha256: str + formula: FormulaSnapshot + tileset: TilesetSnapshot + region: RegionSnapshot + + +def _fail(path: str, message: str) -> None: + raise WangSquareRenderError(f"explainability snapshot {path}: {message}") + + +def _object(value: object, path: str) -> dict[str, object]: + if type(value) is not dict: + _fail(path, "must be an object") + return value + + +def _array(value: object, path: str) -> list[object]: + if type(value) is not list: + _fail(path, "must be an array") + return value + + +def _string(value: object, path: str) -> str: + if type(value) is not str: + _fail(path, "must be a string") + return value + + +def _integer(value: object, path: str, *, nonnegative: bool) -> int: + if type(value) is not int: + _fail(path, "must be an integer") + if nonnegative and value < 0: + _fail(path, "must be nonnegative") + return value + + +def _fields( + value: dict[str, object], + expected: frozenset[str], + path: str, +) -> None: + actual = frozenset(value) + missing = sorted(expected - actual) + extra = sorted(actual - expected) + if missing: + _fail(path, f"missing fields: {', '.join(missing)}") + if extra: + _fail(path, f"unknown fields: {', '.join(extra)}") + + +def _literal(value: object, expected: str, path: str) -> None: + if _string(value, path) != expected: + _fail(path, f"must equal {expected!r}") + + +def _sha256(value: object, path: str) -> str: + digest = _string(value, path) + if _SHA256_PATTERN.fullmatch(digest) is None: + _fail(path, "must be a lowercase SHA-256 digest") + return digest + + +def _basename(value: object, path: str) -> str: + name = _string(value, path) + if ( + not name + or name in {".", ".."} + or Path(name).name != name + or "/" in name + or "\\" in name + ): + _fail(path, "must be a nonempty artifact basename") + return name + + +def _reject_duplicate_members( + pairs: list[tuple[str, object]], +) -> dict[str, object]: + result: dict[str, object] = {} + for key, value in pairs: + if key in result: + raise WangSquareRenderError( + f"JSON object contains duplicate member {key!r}" + ) + result[key] = value + return result + + +def _reject_nonfinite_constant(value: str) -> None: + raise WangSquareRenderError( + f"JSON document contains non-finite number {value}" + ) + + +def _load_json_bytes(encoded: bytes, label: str) -> dict[str, object]: + try: + source = encoded.decode("utf-8") + except UnicodeDecodeError as error: + raise WangSquareRenderError(f"{label}: is not valid UTF-8") from error + try: + document = json.loads( + source, + object_pairs_hook=_reject_duplicate_members, + parse_constant=_reject_nonfinite_constant, + ) + except json.JSONDecodeError as error: + raise WangSquareRenderError( + f"{label}: invalid JSON at line {error.lineno}, " + f"column {error.colno}: {error.msg}" + ) from error + except WangSquareRenderError: + raise + except (ValueError, RecursionError) as error: + raise WangSquareRenderError(f"{label}: invalid JSON value: {error}") from error + return _object(document, label) + + +def _read_bytes(path: Path, label: str) -> bytes: + try: + return path.read_bytes() + except OSError as error: + raise WangSquareRenderError(f"cannot read {label} {path!s}: {error}") from error + + +def _parse_formula(document: dict[str, object]) -> FormulaSnapshot: + _fields( + document, + frozenset({"schema", "source", "variable_count", "clauses"}), + "formula $", + ) + _literal(document["schema"], FORMULA_SCHEMA, "formula $.schema") + source = _object(document["source"], "formula $.source") + _fields(source, frozenset({"name", "sha256"}), "formula $.source") + source_name = _basename(source["name"], "formula $.source.name") + source_digest = _sha256(source["sha256"], "formula $.source.sha256") + variable_count = _integer( + document["variable_count"], + "formula $.variable_count", + nonnegative=True, + ) + if variable_count == 0: + _fail("formula $.variable_count", "must be positive") + clauses = _array(document["clauses"], "formula $.clauses") + if len(clauses) != variable_count: + _fail("formula $.clauses", "length must equal variable_count") + occurrences = [0] * variable_count + projected: list[tuple[int, int, int]] = [] + for clause_id, raw_clause in enumerate(clauses): + path = f"formula $.clauses[{clause_id}]" + clause = _object(raw_clause, path) + _fields(clause, frozenset({"clause_id", "variables"}), path) + actual_id = _integer( + clause["clause_id"], + f"{path}.clause_id", + nonnegative=True, + ) + if actual_id != clause_id: + _fail(f"{path}.clause_id", "must equal canonical position") + variables = _array(clause["variables"], f"{path}.variables") + if len(variables) != 3: + _fail(f"{path}.variables", "must contain exactly three positions") + checked: list[int] = [] + for position, raw_variable in enumerate(variables): + variable = _integer( + raw_variable, + f"{path}.variables[{position}]", + nonnegative=True, + ) + if variable >= variable_count: + _fail(f"{path}.variables[{position}]", "is outside the domain") + occurrences[variable] += 1 + checked.append(variable) + projected.append(tuple(checked)) + if any(count != 3 for count in occurrences): + _fail("formula $.clauses", "every variable must occur exactly three times") + return FormulaSnapshot( + source_name=source_name, + source_sha256=source_digest, + variable_count=variable_count, + clauses=tuple(projected), + ) + + +def _edges( + value: object, + path: str, + *, + optional: bool, +) -> tuple[int | None, int | None, int | None, int | None]: + edges = _object(value, path) + _fields(edges, frozenset(DIRECTIONS), path) + projected: list[int | None] = [] + for direction in DIRECTIONS: + color = edges[direction] + if optional and color is None: + projected.append(None) + else: + projected.append( + _integer(color, f"{path}.{direction}", nonnegative=True) + ) + return tuple(projected) + + +def _parse_tileset(document: dict[str, object]) -> TilesetSnapshot: + _fields( + document, + frozenset({"schema", "geometry", "directions", "colors", "tiles"}), + "tileset $", + ) + _literal(document["schema"], TILESET_SCHEMA, "tileset $.schema") + _literal(document["geometry"], "square", "tileset $.geometry") + if _array(document["directions"], "tileset $.directions") != list(DIRECTIONS): + _fail("tileset $.directions", "must equal N/E/S/W") + raw_colors = _array(document["colors"], "tileset $.colors") + colors = tuple( + _integer(color, f"tileset $.colors[{index}]", nonnegative=True) + for index, color in enumerate(raw_colors) + ) + if not colors or list(colors) != sorted(set(colors)): + _fail("tileset $.colors", "must be nonempty, increasing, and unique") + raw_tiles = _array(document["tiles"], "tileset $.tiles") + if not raw_tiles: + _fail("tileset $.tiles", "must not be empty") + tiles: list[tuple[int, int, int, int]] = [] + for expected_id, raw_tile in enumerate(raw_tiles): + path = f"tileset $.tiles[{expected_id}]" + tile = _object(raw_tile, path) + _fields(tile, frozenset({"tile_id", "edges"}), path) + tile_id = _integer(tile["tile_id"], f"{path}.tile_id", nonnegative=True) + if tile_id != expected_id: + _fail(f"{path}.tile_id", "must equal canonical table position") + projected = _edges(tile["edges"], f"{path}.edges", optional=False) + assert all(color is not None for color in projected) + tiles.append(tuple(projected)) + used = sorted({color for tile in tiles for color in tile}) + if list(colors) != used: + _fail("tileset $.colors", "must equal exactly the colors used by tiles") + return TilesetSnapshot(colors=colors, tile_edges=tuple(tiles)) + + +def _parse_region(document: dict[str, object]) -> RegionSnapshot: + _fields( + document, + frozenset( + { + "schema", + "geometry", + "source_formula_sha256", + "bounds", + "active", + "boundary", + } + ), + "region $", + ) + _literal(document["schema"], REGION_SCHEMA, "region $.schema") + _literal(document["geometry"], "square", "region $.geometry") + source_digest = _sha256( + document["source_formula_sha256"], + "region $.source_formula_sha256", + ) + bounds = _object(document["bounds"], "region $.bounds") + fields = frozenset( + { + "min_x_inclusive", + "min_y_inclusive", + "max_x_inclusive", + "max_y_inclusive", + } + ) + _fields(bounds, fields, "region $.bounds") + min_x = _integer( + bounds["min_x_inclusive"], + "region $.bounds.min_x_inclusive", + nonnegative=False, + ) + min_y = _integer( + bounds["min_y_inclusive"], + "region $.bounds.min_y_inclusive", + nonnegative=False, + ) + max_x = _integer( + bounds["max_x_inclusive"], + "region $.bounds.max_x_inclusive", + nonnegative=False, + ) + max_y = _integer( + bounds["max_y_inclusive"], + "region $.bounds.max_y_inclusive", + nonnegative=False, + ) + if max_x < min_x or max_y < min_y: + _fail("region $.bounds", "inclusive maxima must not precede minima") + width = max_x - min_x + 1 + height = max_y - min_y + 1 + area = width * height + raw_active = _array(document["active"], "region $.active") + raw_boundary = _array(document["boundary"], "region $.boundary") + if len(raw_active) != area or len(raw_boundary) != area: + _fail("region $", f"active and boundary lengths must equal area {area}") + if any(type(value) is not bool for value in raw_active): + _fail("region $.active", "must contain only booleans") + if not any(raw_active): + _fail("region $.active", "must contain an active cell") + active = tuple(raw_active) + boundary: list[ + tuple[int | None, int | None, int | None, int | None] | None + ] = [] + for index, raw_sides in enumerate(raw_boundary): + if not active[index]: + if raw_sides is not None: + _fail(f"region $.boundary[{index}]", "must be null when inactive") + boundary.append(None) + continue + if raw_sides is None: + _fail(f"region $.boundary[{index}]", "must be present when active") + boundary.append( + _edges(raw_sides, f"region $.boundary[{index}]", optional=True) + ) + for index, is_active in enumerate(active): + if not is_active: + continue + sides = boundary[index] + assert sides is not None + x = index % width + y = index // width + for direction, (dx, dy) in enumerate(((0, -1), (1, 0), (0, 1), (-1, 0))): + neighbor_x = x + dx + neighbor_y = y + dy + if ( + 0 <= neighbor_x < width + and 0 <= neighbor_y < height + and active[neighbor_y * width + neighbor_x] + and sides[direction] is not None + ): + _fail( + f"region $.boundary[{index}].{DIRECTIONS[direction]}", + "must be null on an internal edge", + ) + return RegionSnapshot( + min_x=min_x, + min_y=min_y, + max_x=max_x, + max_y=max_y, + source_formula_sha256=source_digest, + active=active, + boundary=tuple(boundary), + ) + + +def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: + """Load one manifest, verify hashes, and project its three artifacts.""" + manifest_path = Path(path) + manifest = _load_json_bytes( + _read_bytes(manifest_path, "manifest"), + str(manifest_path), + ) + _fields( + manifest, + frozenset({"schema", "stage", "source_formula_sha256", "artifacts"}), + "$", + ) + _literal(manifest["schema"], MANIFEST_SCHEMA, "$.schema") + _literal(manifest["stage"], "region", "$.stage") + source_digest = _sha256( + manifest["source_formula_sha256"], + "$.source_formula_sha256", + ) + artifacts = _object(manifest["artifacts"], "$.artifacts") + _fields(artifacts, frozenset({"formula", "tileset", "region"}), "$.artifacts") + expected_schemas = { + "formula": FORMULA_SCHEMA, + "tileset": TILESET_SCHEMA, + "region": REGION_SCHEMA, + } + documents: dict[str, dict[str, object]] = {} + for name, expected_schema in expected_schemas.items(): + reference_path = f"$.artifacts.{name}" + reference = _object(artifacts[name], reference_path) + _fields(reference, frozenset({"path", "sha256", "schema"}), reference_path) + artifact_name = _basename(reference["path"], f"{reference_path}.path") + expected_digest = _sha256( + reference["sha256"], + f"{reference_path}.sha256", + ) + _literal(reference["schema"], expected_schema, f"{reference_path}.schema") + artifact_path = manifest_path.parent / artifact_name + 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)) + + formula = _parse_formula(documents["formula"]) + tileset = _parse_tileset(documents["tileset"]) + region = _parse_region(documents["region"]) + if formula.source_sha256 != source_digest: + _fail("$.source_formula_sha256", "does not match formula snapshot") + if region.source_formula_sha256 != source_digest: + _fail("$.source_formula_sha256", "does not match region snapshot") + colors = set(tileset.colors) + for index, sides in enumerate(region.boundary): + if sides is None: + continue + for direction, color in enumerate(sides): + if color is not None and color not in colors: + _fail( + f"region $.boundary[{index}].{DIRECTIONS[direction]}", + "is absent from the referenced tileset", + ) + return ExplainabilityBundle( + source_formula_sha256=source_digest, + formula=formula, + tileset=tileset, + region=region, + ) + + +def _palette(bundle: ExplainabilityBundle) -> dict[int, tuple[int, int, int]]: + boundary_colors = tuple( + sorted( + { + color + for sides in bundle.region.boundary + if sides is not None + for color in sides + if color is not None + } + ) + ) + edges: tuple[tuple[int, ...], ...] + if boundary_colors: + edges = (*bundle.tileset.tile_edges, boundary_colors) + else: + edges = bundle.tileset.tile_edges + return _build_palette_from_edges(edges) + + +def _formula_lines(formula: FormulaSnapshot) -> list[str]: + lines = [ + f"Source: {formula.source_name}", + "SHA-256:", + formula.source_sha256[:32], + formula.source_sha256[32:], + "", + "Cubic monotone 1-in-3 SAT", + f"Variables: {formula.variable_count}", + f"Clauses: {len(formula.clauses)}", + "", + ] + for clause_id, clause in enumerate(formula.clauses): + variables = ", ".join(f"x{variable}" for variable in clause) + lines.append(f"c{clause_id}: exactly-one({variables})") + return lines + + +def _compose_formula(bundle: ExplainabilityBundle, margin: int) -> np.ndarray: + checked_margin = _render_integer( + margin, + "margin", + minimum=0, + maximum=MAX_MARGIN, + ) + content_width = 780 + width = 2 * checked_margin + content_width + font = explain_font(16) + line_height = 25 + lines = _formula_lines(bundle.formula) + height = 2 * checked_margin + _HEADER_HEIGHT + 20 + len(lines) * line_height + _check_canvas_limits(width, height) + canvas = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB) + draw = ImageDraw.Draw(canvas) + draw_explain_heading( + draw, + (checked_margin, checked_margin), + title="Parsed formula snapshot", + subtitle=( + "positions and duplicates are preserved exactly; " + "variable IDs are zero-based" + ), + ) + y = checked_margin + _HEADER_HEIGHT + for line in lines: + wrapped = wrap_text(draw, line, font, content_width) + y = draw_lines(draw, wrapped, (checked_margin, y), font=font, spacing=7) + return np.asarray(canvas, dtype=np.uint8) + + +def _hex_tile_edges( + tileset: TilesetSnapshot, +) -> tuple[tuple[tuple[int, int, int, int, int, int], ...], int]: + square = WangPresentation( + min_x=0, + min_y=0, + max_x=0, + max_y=0, + tile_edges=tileset.tile_edges, + cells=(0,), + boundary=((None, None, None, None),), + ) + port = reduce_square_to_hex(square) + check_square_to_hex(square, port) + return port.tile_edges, port.fresh_color + + +def _region_hex_port(bundle: ExplainabilityBundle) -> WangHexPort: + region = bundle.region + square = WangPresentation( + min_x=region.min_x, + min_y=region.min_y, + max_x=region.max_x, + max_y=region.max_y, + tile_edges=bundle.tileset.tile_edges, + # The static region has no assignment. Empty presentation cells let + # the existing port/checker validate only table, bounds, and boundary. + cells=(None,) * len(region.active), + boundary=region.boundary, + ) + port = reduce_square_to_hex(square) + check_square_to_hex(square, port) + return port + + +def _compose_tileset( + bundle: ExplainabilityBundle, + pixels_per_cell: int, + margin: int, + *, + hex_mode: bool, +) -> np.ndarray: + checked = _render_integer( + pixels_per_cell, + "pixels_per_cell", + minimum=MIN_PIXELS_PER_CELL, + maximum=MAX_PIXELS_PER_CELL, + ) + checked_margin = _render_integer( + margin, + "margin", + minimum=0, + maximum=MAX_MARGIN, + ) + columns = 6 + rows = (len(bundle.tileset.tile_edges) + columns - 1) // columns + gap = 14 + palette = _palette(bundle) + fresh: int | None = None + if hex_mode: + tile_edges, fresh = _hex_tile_edges(bundle.tileset) + palette = _build_palette_from_edges(tile_edges) + radius = max(28, checked) + shoulder = radius // 2 + tile_width = 2 * radius + 1 + tile_height = 2 * radius + 1 + else: + tile_edges = bundle.tileset.tile_edges + tile_width = tile_height = max(64, checked * 2) + radius = 0 + shoulder = 0 + grid_width = columns * tile_width + (columns - 1) * gap + grid_height = rows * tile_height + (rows - 1) * gap + width = 2 * checked_margin + grid_width + _PANEL_GAP + _LEGEND_WIDTH + height = max(2 * checked_margin + _HEADER_HEIGHT + grid_height, 410) + _check_canvas_limits(width, height) + canvas = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB) + draw = ImageDraw.Draw(canvas) + geometry = "hex" if hex_mode else "square" + draw_explain_heading( + draw, + (checked_margin, checked_margin), + title=f"Tile sheet ({len(tile_edges)} tiles) - {geometry}", + subtitle="tile ID at center; numeric logical color on every side", + ) + grid_y = checked_margin + _HEADER_HEIGHT + vertices = _hex_vertices(radius, shoulder) if hex_mode else () + for tile_id, edges in enumerate(tile_edges): + column = tile_id % columns + row = tile_id // columns + x = checked_margin + column * (tile_width + gap) + y = grid_y + row * (tile_height + gap) + if hex_mode: + asset = hex_explain_tile( + edges, + palette, + radius, + vertices, + tile_id=tile_id, + edge_labels=True, + ) + canvas.paste(asset, (x, y), _hex_mask(radius, vertices)) + else: + asset = square_explain_tile( + edges, + palette, + tile_width, + tile_id=tile_id, + edge_labels=True, + ) + canvas.paste(asset, (x, y)) + legend_x = checked_margin + grid_width + _PANEL_GAP + _, legend_height = draw_palette_legend( + ImageDraw.Draw(canvas), + palette, + (legend_x, grid_y), + columns=2, + ) + if fresh is not None: + ImageDraw.Draw(canvas).text( + (legend_x, grid_y + legend_height + 10), + f"kappa = {fresh} (fresh axis)", + font=explain_font(13), + fill=EXPLAIN_TEXT_RGB, + ) + return np.asarray(canvas, dtype=np.uint8) + + +def _formula_panel( + canvas: Image.Image, + bundle: ExplainabilityBundle, + origin: tuple[int, int], + max_height: int, +) -> int: + draw = ImageDraw.Draw(canvas) + x, y = origin + draw.text( + (x, y), + "Formula being simulated", + font=explain_font(17), + fill=EXPLAIN_TEXT_RGB, + ) + y += 30 + font = explain_font(13) + for line in _formula_lines(bundle.formula): + wrapped = wrap_text(draw, line, font, _FORMULA_PANEL_WIDTH) + for item in wrapped: + if y + 20 > max_height: + draw.text((x, y), "...", font=font, fill=EXPLAIN_MUTED_RGB) + return y + 22 + draw.text((x, y), item, font=font, fill=EXPLAIN_TEXT_RGB) + y += 20 + return y + + +def _compose_region_square( + bundle: ExplainabilityBundle, + pixels_per_cell: int, + margin: int, +) -> np.ndarray: + ppc = _render_integer( + pixels_per_cell, + "pixels_per_cell", + minimum=MIN_PIXELS_PER_CELL, + maximum=MAX_PIXELS_PER_CELL, + ) + checked_margin = _render_integer( + margin, + "margin", + minimum=0, + maximum=MAX_MARGIN, + ) + region = bundle.region + grid_width = region.width * ppc + grid_height = region.height * ppc + side_width = max(_FORMULA_PANEL_WIDTH, _LEGEND_WIDTH) + width = 2 * checked_margin + grid_width + _PANEL_GAP + side_width + formula_height = 30 + len(_formula_lines(bundle.formula)) * 20 + legend_rows = (len(_palette(bundle)) + 1) // 2 + side_height = formula_height + 20 + 36 + legend_rows * 22 + 42 + height = max( + 2 * checked_margin + _HEADER_HEIGHT + grid_height, + 2 * checked_margin + _HEADER_HEIGHT + side_height, + ) + _check_canvas_limits(width, height) + canvas = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB) + draw = ImageDraw.Draw(canvas) + draw_explain_heading( + draw, + (checked_margin, checked_margin), + title="Yang-Zhang region - before solving", + subtitle=( + "active mask and exposed boundary constraints; " + "no tile is assigned" + ), + ) + grid_x = checked_margin + grid_y = checked_margin + _HEADER_HEIGHT + palette = _palette(bundle) + inactive = square_inactive_tile(ppc) + for index, active in enumerate(region.active): + x = grid_x + (index % region.width) * ppc + y = grid_y + (index // region.width) * ppc + if not active: + canvas.paste(inactive, (x, y)) + continue + sides = region.boundary[index] + assert sides is not None + canvas.paste(square_region_tile(ppc, sides, palette), (x, y)) + side_x = grid_x + grid_width + _PANEL_GAP + formula_end = _formula_panel( + canvas, + bundle, + (side_x, grid_y), + height - checked_margin, + ) + legend_y = formula_end + 16 + _, legend_height = draw_palette_legend( + ImageDraw.Draw(canvas), + palette, + (side_x, legend_y), + columns=2, + ) + draw_inactive_key( + ImageDraw.Draw(canvas), + (side_x, legend_y + legend_height + 8), + ) + return np.asarray(canvas, dtype=np.uint8) + + +def _compose_region_hex( + bundle: ExplainabilityBundle, + pixels_per_cell: int, + margin: int, +) -> np.ndarray: + radius = _render_integer( + pixels_per_cell, + "pixels_per_cell", + minimum=MIN_PIXELS_PER_CELL, + maximum=MAX_PIXELS_PER_CELL, + ) + checked_margin = _render_integer( + margin, + "margin", + minimum=0, + maximum=MAX_MARGIN, + ) + region = bundle.region + port = _region_hex_port(bundle) + shoulder = radius // 2 + raw_width = ( + 2 * radius * (region.width - 1) + + radius * (region.height - 1) + + 2 * radius + + 1 + ) + raw_height = ( + (radius + shoulder) * (region.height - 1) + 2 * radius + 1 + ) + side_width = max(_FORMULA_PANEL_WIDTH, _LEGEND_WIDTH) + width = 2 * checked_margin + raw_width + _PANEL_GAP + side_width + formula_height = 30 + len(_formula_lines(bundle.formula)) * 20 + legend_rows = (len(_palette(bundle)) + 1) // 2 + side_height = formula_height + 20 + 36 + legend_rows * 22 + 42 + height = max( + 2 * checked_margin + _HEADER_HEIGHT + raw_height, + 2 * checked_margin + _HEADER_HEIGHT + side_height, + ) + _check_canvas_limits(width, height) + canvas = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB) + draw = ImageDraw.Draw(canvas) + draw_explain_heading( + draw, + (checked_margin, checked_margin), + title="Yang-Zhang region - checked axial presentation", + subtitle="square coordinates (x,y) become (q,r); no tile is assigned", + ) + grid_x = checked_margin + grid_y = checked_margin + _HEADER_HEIGHT + vertices = _hex_vertices(radius, shoulder) + mask = _hex_mask(radius, vertices) + neutral = Image.new("RGB", (2 * radius + 1, 2 * radius + 1), EXPLAIN_PANEL_RGB) + ImageDraw.Draw(neutral).polygon( + vertices, + fill=EXPLAIN_ACTIVE_RGB, + outline=EXPLAIN_OUTLINE_RGB, + ) + inactive = Image.new("RGB", neutral.size, EXPLAIN_PANEL_RGB) + inactive_draw = ImageDraw.Draw(inactive) + inactive_draw.polygon( + vertices, + fill=(215, 220, 228), + outline=EXPLAIN_OUTLINE_RGB, + ) + inactive_draw.line( + (radius // 2, radius // 2, radius + radius // 2, radius + radius // 2), + fill=EXPLAIN_OUTLINE_RGB, + width=1, + ) + inactive_draw.line( + (radius + radius // 2, radius // 2, radius // 2, radius + radius // 2), + fill=EXPLAIN_OUTLINE_RGB, + width=1, + ) + palette = _palette(bundle) + min_anchor_x = 2 * radius * region.min_x + radius * region.min_y + min_anchor_y = (radius + shoulder) * region.min_y + overlays: list[ + tuple[tuple[int, int], tuple[int, int], tuple[int, int, int]] + ] = [] + for index, active in enumerate(region.active): + local_q = index % region.width + local_r = index // region.width + q = region.min_x + local_q + r = region.min_y + local_r + anchor_x = 2 * radius * q + radius * r + anchor_y = (radius + shoulder) * r + x = grid_x + anchor_x - min_anchor_x + y = grid_y + anchor_y - min_anchor_y + canvas.paste(neutral if active else inactive, (x, y), mask) + if not active: + continue + sides = port.boundary[index] + assert sides is not None + for direction, color in enumerate(sides): + if color is None: + continue + first = vertices[(direction + 1) % 6] + second = vertices[(direction + 2) % 6] + overlays.append( + ( + (x + first[0], y + first[1]), + (x + second[0], y + second[1]), + palette[color], + ) + ) + draw = ImageDraw.Draw(canvas) + for first, second, rgb in overlays: + draw_boundary_side(draw, first, second, rgb, width=max(2, radius // 7)) + side_x = grid_x + raw_width + _PANEL_GAP + formula_end = _formula_panel( + canvas, + bundle, + (side_x, grid_y), + height - checked_margin, + ) + legend_y = formula_end + 16 + _, legend_height = draw_palette_legend( + ImageDraw.Draw(canvas), + palette, + (side_x, legend_y), + columns=2, + ) + draw_inactive_key( + ImageDraw.Draw(canvas), + (side_x, legend_y + legend_height + 8), + ) + return np.asarray(canvas, dtype=np.uint8) + + +def render_pipeline_snapshot( + input_path: str | Path, + output_path: str | Path, + *, + view: str, + pixels_per_cell: int = DEFAULT_PIXELS_PER_CELL, + margin: int = DEFAULT_MARGIN, + hex_mode: bool = False, +) -> None: + """Render one strict manifest view and atomically install its PNG.""" + bundle = load_explainability_bundle(input_path) + if view == "formula": + if hex_mode: + raise WangSquareRenderError("--hex is not meaningful for formula view") + canvas = _compose_formula(bundle, margin) + elif view == "tileset": + canvas = _compose_tileset( + bundle, + pixels_per_cell, + margin, + hex_mode=hex_mode, + ) + elif view == "region": + if hex_mode: + canvas = _compose_region_hex(bundle, pixels_per_cell, margin) + else: + canvas = _compose_region_square(bundle, pixels_per_cell, margin) + else: + raise WangSquareRenderError( + "snapshot view must be one of formula, tileset, or region" + ) + _save_png_atomic(canvas, output_path) diff --git a/renderer/wang_square.py b/renderer/wang_square.py index 7016620..2567b34 100644 --- a/renderer/wang_square.py +++ b/renderer/wang_square.py @@ -19,6 +19,18 @@ import numpy as np from PIL import Image, ImageDraw +from wang_explain import ( + EXPLAIN_PANEL_RGB, + EXPLAIN_TEXT_RGB, + draw_boundary_side, + draw_explain_heading, + draw_inactive_key, + draw_palette_legend, + explain_font, + hex_explain_tile, + square_explain_tile, + square_inactive_tile, +) from wang_hex_port import ( SQUARE_DIRECTIONS, WangHexPort, @@ -41,6 +53,9 @@ MAX_MARGIN: Final = 4096 MAX_CANVAS_SIDE: Final = 16384 MAX_CANVAS_PIXELS: Final = 64 * 1024 * 1024 +EXPLAIN_HEADER_HEIGHT: Final = 54 +EXPLAIN_LEGEND_WIDTH: Final = 190 +EXPLAIN_PANEL_GAP: Final = 20 BACKGROUND_RGB: Final = (248, 248, 244) GRID_RGB: Final = (32, 35, 42) @@ -588,6 +603,270 @@ def _compose_wang_hex( return np.asarray(canvas, dtype=np.uint8) +def _palette_with_boundary( + tile_edges: tuple[tuple[int, ...], ...], + boundary: tuple[tuple[int | None, ...] | None, ...], +) -> dict[int, tuple[int, int, int]]: + colors = { + color + for sides in boundary + if sides is not None + for color in sides + if color is not None + } + if colors: + return _build_palette_from_edges((*tile_edges, tuple(sorted(colors)))) + return _build_palette_from_edges(tile_edges) + + +def _compose_wang_square_explain( + presentation: WangPresentation, + *, + pixels_per_cell: int = DEFAULT_PIXELS_PER_CELL, + margin: int = DEFAULT_MARGIN, +) -> np.ndarray: + """Compose an opt-in square view with explicit colored side bands.""" + ppc = _render_integer( + pixels_per_cell, + "pixels_per_cell", + minimum=MIN_PIXELS_PER_CELL, + maximum=MAX_PIXELS_PER_CELL, + ) + checked_margin = _render_integer( + margin, + "margin", + minimum=0, + maximum=MAX_MARGIN, + ) + grid_width = presentation.width * ppc + grid_height = presentation.height * ppc + canvas_width = ( + 2 * checked_margin + + grid_width + + EXPLAIN_PANEL_GAP + + EXPLAIN_LEGEND_WIDTH + ) + canvas_height = max( + 2 * checked_margin + EXPLAIN_HEADER_HEIGHT + grid_height, + 2 * checked_margin + EXPLAIN_HEADER_HEIGHT + 300, + ) + _check_canvas_limits(canvas_width, canvas_height) + + canvas = Image.new( + "RGB", + (canvas_width, canvas_height), + EXPLAIN_PANEL_RGB, + ) + draw = ImageDraw.Draw(canvas) + draw_explain_heading( + draw, + (checked_margin, checked_margin), + title="Verified Wang solution - square", + subtitle="colored N/E/S/W bands; tile ID at each active cell", + ) + grid_x = checked_margin + grid_y = checked_margin + EXPLAIN_HEADER_HEIGHT + palette = _palette_with_boundary( + presentation.tile_edges, + presentation.boundary, + ) + inactive = square_inactive_tile(ppc) + tile_assets: dict[int, Image.Image] = {} + overlays: list[ + tuple[ + tuple[int, int], + tuple[int, int], + tuple[int, int, int], + ] + ] = [] + + for index, tile_id in enumerate(presentation.cells): + local_x = index % presentation.width + local_y = index // presentation.width + x = grid_x + local_x * ppc + y = grid_y + local_y * ppc + if tile_id is None: + canvas.paste(inactive, (x, y)) + continue + asset = tile_assets.get(tile_id) + if asset is None: + asset = square_explain_tile( + presentation.tile_edges[tile_id], + palette, + ppc, + tile_id=tile_id, + edge_labels=False, + ) + tile_assets[tile_id] = asset + canvas.paste(asset, (x, y)) + sides = presentation.boundary[index] + if sides is None: + continue + segments = ( + ((x, y), (x + ppc - 1, y)), + ((x + ppc - 1, y), (x + ppc - 1, y + ppc - 1)), + ((x, y + ppc - 1), (x + ppc - 1, y + ppc - 1)), + ((x, y), (x, y + ppc - 1)), + ) + for direction, color in enumerate(sides): + if color is not None: + overlays.append((*segments[direction], palette[color])) + + draw = ImageDraw.Draw(canvas) + for first, second, rgb in overlays: + draw_boundary_side( + draw, + first, + second, + rgb, + width=max(2, ppc // 12), + ) + legend_x = grid_x + grid_width + EXPLAIN_PANEL_GAP + _, legend_height = draw_palette_legend( + draw, + palette, + (legend_x, grid_y), + columns=2, + ) + draw_inactive_key(draw, (legend_x, grid_y + legend_height + 12)) + return np.asarray(canvas, dtype=np.uint8) + + +def _compose_wang_hex_explain( + square: WangPresentation, + *, + pixels_per_cell: int = DEFAULT_PIXELS_PER_CELL, + margin: int = DEFAULT_MARGIN, +) -> np.ndarray: + """Compose an opt-in checked hex view with explicit six-side bands.""" + presentation = reduce_square_to_hex(square) + check_square_to_hex(square, presentation) + raw_width, raw_height, radius, shoulder, _ = _hex_canvas_dimensions( + presentation, + pixels_per_cell, + 0, + ) + checked_margin = _render_integer( + margin, + "margin", + minimum=0, + maximum=MAX_MARGIN, + ) + canvas_width = ( + 2 * checked_margin + + raw_width + + EXPLAIN_PANEL_GAP + + EXPLAIN_LEGEND_WIDTH + ) + canvas_height = max( + 2 * checked_margin + EXPLAIN_HEADER_HEIGHT + raw_height, + 2 * checked_margin + EXPLAIN_HEADER_HEIGHT + 350, + ) + _check_canvas_limits(canvas_width, canvas_height) + canvas = Image.new( + "RGB", + (canvas_width, canvas_height), + EXPLAIN_PANEL_RGB, + ) + draw = ImageDraw.Draw(canvas) + draw_explain_heading( + draw, + (checked_margin, checked_margin), + title="Verified Wang solution - Basire/Culik hex view", + subtitle="E/SE/SW/W/NW/NE bands; kappa marks the presentation-only axis", + ) + grid_x = checked_margin + grid_y = checked_margin + EXPLAIN_HEADER_HEIGHT + vertices = _hex_vertices(radius, shoulder) + mask = _hex_mask(radius, vertices) + inactive = _hex_hole_asset(radius, vertices) + palette = _palette_with_boundary( + presentation.tile_edges, + presentation.boundary, + ) + tile_assets: dict[int, Image.Image] = {} + overlays: list[ + tuple[ + tuple[int, int], + tuple[int, int], + tuple[int, int, int], + ] + ] = [] + min_anchor_x = ( + 2 * radius * presentation.min_q + radius * presentation.min_r + ) + min_anchor_y = (radius + shoulder) * presentation.min_r + for index, tile_id in enumerate(presentation.cells): + local_q = index % presentation.width + local_r = index // presentation.width + q = presentation.min_q + local_q + r = presentation.min_r + local_r + anchor_x = 2 * radius * q + radius * r + anchor_y = (radius + shoulder) * r + x = grid_x + anchor_x - min_anchor_x + y = grid_y + anchor_y - min_anchor_y + if tile_id is None: + asset = inactive + else: + asset = tile_assets.get(tile_id) + if asset is None: + asset = hex_explain_tile( + presentation.tile_edges[tile_id], + palette, + radius, + vertices, + tile_id=tile_id, + edge_labels=False, + ) + tile_assets[tile_id] = asset + canvas.paste(asset, (x, y), mask) + if tile_id is None: + continue + sides = presentation.boundary[index] + if sides is None: + continue + for direction, color in enumerate(sides): + if color is None: + continue + first = vertices[(direction + 1) % 6] + second = vertices[(direction + 2) % 6] + overlays.append( + ( + (x + first[0], y + first[1]), + (x + second[0], y + second[1]), + palette[color], + ) + ) + + draw = ImageDraw.Draw(canvas) + for first, second, rgb in overlays: + draw_boundary_side( + draw, + first, + second, + rgb, + width=max(2, radius // 8), + ) + legend_x = grid_x + raw_width + EXPLAIN_PANEL_GAP + _, legend_height = draw_palette_legend( + draw, + palette, + (legend_x, grid_y), + columns=2, + ) + draw.text( + (legend_x, grid_y + legend_height + 8), + f"kappa = {presentation.fresh_color}", + font=explain_font(13), + fill=EXPLAIN_TEXT_RGB, + ) + draw_inactive_key( + draw, + (legend_x, grid_y + legend_height + 38), + ) + return np.asarray(canvas, dtype=np.uint8) + + def _save_png_atomic(canvas: np.ndarray, output_path: str | Path) -> None: destination = Path(output_path) temporary: Path | None = None @@ -627,15 +906,28 @@ def render_wang_square( pixels_per_cell: int = DEFAULT_PIXELS_PER_CELL, margin: int = DEFAULT_MARGIN, hex_mode: bool = False, + explain: bool = False, ) -> None: """Load a v1 presentation and atomically write square or hex pixels.""" presentation = load_wang_presentation(input_path) - if hex_mode: + if hex_mode and explain: + canvas = _compose_wang_hex_explain( + presentation, + pixels_per_cell=pixels_per_cell, + margin=margin, + ) + elif hex_mode: canvas = _compose_wang_hex( presentation, pixels_per_cell=pixels_per_cell, margin=margin, ) + elif explain: + canvas = _compose_wang_square_explain( + presentation, + pixels_per_cell=pixels_per_cell, + margin=margin, + ) else: canvas = compose_wang_square( presentation, @@ -648,10 +940,13 @@ def render_wang_square( def _parser() -> argparse.ArgumentParser: parser = argparse.ArgumentParser( description=( - "Render a wang-solution-v1 tiling as a diagnostic square or hex PNG" + "Render a Wang solution or a static explainability snapshot as PNG" ) ) - parser.add_argument("input", help="path to a wang-solution-v1 JSON file") + parser.add_argument( + "input", + help="path to wang-solution-v1 JSON or a wang-explain-manifest-v1 file", + ) parser.add_argument("output", help="path to the output PNG") parser.add_argument( "--pixels-per-cell", @@ -673,6 +968,17 @@ def _parser() -> argparse.ArgumentParser: action="store_true", help="port the square witness to pointy-top axial hexagons", ) + parser.add_argument( + "--explain", + action="store_true", + help="add colored edge bands, tile IDs, boundary emphasis, and a legend", + ) + parser.add_argument( + "--view", + choices=("solution", "formula", "tileset", "region"), + default="solution", + help="input stage to render (default: solution)", + ) return parser @@ -680,13 +986,30 @@ def main(argv: list[str] | None = None) -> None: parser = _parser() args = parser.parse_args(argv) try: - render_wang_square( - args.input, - args.output, - pixels_per_cell=args.pixels_per_cell, - margin=args.margin, - hex_mode=args.hex, - ) + if args.view == "solution": + render_wang_square( + args.input, + args.output, + pixels_per_cell=args.pixels_per_cell, + margin=args.margin, + hex_mode=args.hex, + explain=args.explain, + ) + else: + if args.explain: + raise WangSquareRenderError( + "snapshot views are already explainable; omit --explain" + ) + from wang_snapshot import render_pipeline_snapshot + + render_pipeline_snapshot( + args.input, + args.output, + view=args.view, + pixels_per_cell=args.pixels_per_cell, + margin=args.margin, + hex_mode=args.hex, + ) except (FileNotFoundError, WangSquareRenderError) as error: parser.error(str(error)) diff --git a/schemas/cm13-formula-snapshot-v1.schema.json b/schemas/cm13-formula-snapshot-v1.schema.json new file mode 100644 index 0000000..2d16852 --- /dev/null +++ b/schemas/cm13-formula-snapshot-v1.schema.json @@ -0,0 +1,65 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "urn:tiling-foundry:schema:cm13-formula-snapshot-v1", + "title": "Tiling Foundry parsed CM13 formula snapshot v1", + "type": "object", + "additionalProperties": false, + "required": ["schema", "source", "variable_count", "clauses"], + "properties": { + "schema": { + "const": "cm13-formula-snapshot-v1" + }, + "source": { + "type": "object", + "additionalProperties": false, + "required": ["name", "sha256"], + "properties": { + "name": { + "type": "string", + "minLength": 1, + "pattern": "^[^/\\\\]+$", + "not": { + "enum": [".", ".."] + } + }, + "sha256": { + "$ref": "#/$defs/sha256" + } + } + }, + "variable_count": { + "type": "integer", + "minimum": 1 + }, + "clauses": { + "type": "array", + "minItems": 1, + "items": { + "type": "object", + "additionalProperties": false, + "required": ["clause_id", "variables"], + "properties": { + "clause_id": { + "type": "integer", + "minimum": 0 + }, + "variables": { + "type": "array", + "minItems": 3, + "maxItems": 3, + "items": { + "type": "integer", + "minimum": 0 + } + } + } + } + } + }, + "$defs": { + "sha256": { + "type": "string", + "pattern": "^[0-9a-f]{64}$" + } + } +} diff --git a/schemas/wang-explain-manifest-v1.schema.json b/schemas/wang-explain-manifest-v1.schema.json new file mode 100644 index 0000000..9fa3554 --- /dev/null +++ b/schemas/wang-explain-manifest-v1.schema.json @@ -0,0 +1,77 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "urn:tiling-foundry:schema:wang-explain-manifest-v1", + "title": "Tiling Foundry static explainability manifest v1", + "type": "object", + "additionalProperties": false, + "required": ["schema", "stage", "source_formula_sha256", "artifacts"], + "properties": { + "schema": { + "const": "wang-explain-manifest-v1" + }, + "stage": { + "const": "region" + }, + "source_formula_sha256": { + "$ref": "#/$defs/sha256" + }, + "artifacts": { + "type": "object", + "additionalProperties": false, + "required": ["formula", "tileset", "region"], + "properties": { + "formula": { + "$ref": "#/$defs/formula_reference" + }, + "tileset": { + "$ref": "#/$defs/tileset_reference" + }, + "region": { + "$ref": "#/$defs/region_reference" + } + } + } + }, + "$defs": { + "sha256": { + "type": "string", + "pattern": "^[0-9a-f]{64}$" + }, + "artifact_path": { + "type": "string", + "minLength": 1, + "pattern": "^[^/\\\\]+$", + "not": { + "enum": [".", ".."] + } + }, + "formula_reference": { + "$ref": "#/$defs/reference", + "properties": { + "schema": {"const": "cm13-formula-snapshot-v1"} + } + }, + "tileset_reference": { + "$ref": "#/$defs/reference", + "properties": { + "schema": {"const": "wang-tileset-snapshot-v1"} + } + }, + "region_reference": { + "$ref": "#/$defs/reference", + "properties": { + "schema": {"const": "wang-region-snapshot-v1"} + } + }, + "reference": { + "type": "object", + "additionalProperties": false, + "required": ["path", "sha256", "schema"], + "properties": { + "path": {"$ref": "#/$defs/artifact_path"}, + "sha256": {"$ref": "#/$defs/sha256"}, + "schema": {"type": "string"} + } + } + } +} diff --git a/schemas/wang-region-snapshot-v1.schema.json b/schemas/wang-region-snapshot-v1.schema.json new file mode 100644 index 0000000..16e298f --- /dev/null +++ b/schemas/wang-region-snapshot-v1.schema.json @@ -0,0 +1,86 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "urn:tiling-foundry:schema:wang-region-snapshot-v1", + "title": "Tiling Foundry unassigned square Wang region snapshot v1", + "type": "object", + "additionalProperties": false, + "required": [ + "schema", + "geometry", + "source_formula_sha256", + "bounds", + "active", + "boundary" + ], + "properties": { + "schema": { + "const": "wang-region-snapshot-v1" + }, + "geometry": { + "const": "square" + }, + "source_formula_sha256": { + "$ref": "#/$defs/sha256" + }, + "bounds": { + "$ref": "#/$defs/inclusive_bounds" + }, + "active": { + "type": "array", + "minItems": 1, + "contains": {"const": true}, + "items": { + "type": "boolean" + } + }, + "boundary": { + "type": "array", + "minItems": 1, + "items": { + "oneOf": [ + {"$ref": "#/$defs/optional_edges"}, + {"type": "null"} + ] + } + } + }, + "$defs": { + "sha256": { + "type": "string", + "pattern": "^[0-9a-f]{64}$" + }, + "inclusive_bounds": { + "type": "object", + "additionalProperties": false, + "required": [ + "min_x_inclusive", + "min_y_inclusive", + "max_x_inclusive", + "max_y_inclusive" + ], + "properties": { + "min_x_inclusive": {"type": "integer"}, + "min_y_inclusive": {"type": "integer"}, + "max_x_inclusive": {"type": "integer"}, + "max_y_inclusive": {"type": "integer"} + } + }, + "nullable_color": { + "oneOf": [ + {"type": "integer", "minimum": 0}, + {"type": "null"} + ] + }, + "optional_edges": { + "type": "object", + "additionalProperties": false, + "required": ["N", "E", "S", "W"], + "properties": { + "N": {"$ref": "#/$defs/nullable_color"}, + "E": {"$ref": "#/$defs/nullable_color"}, + "S": {"$ref": "#/$defs/nullable_color"}, + "W": {"$ref": "#/$defs/nullable_color"} + } + } + } +} diff --git a/schemas/wang-tileset-snapshot-v1.schema.json b/schemas/wang-tileset-snapshot-v1.schema.json new file mode 100644 index 0000000..b34e26d --- /dev/null +++ b/schemas/wang-tileset-snapshot-v1.schema.json @@ -0,0 +1,70 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "urn:tiling-foundry:schema:wang-tileset-snapshot-v1", + "title": "Tiling Foundry square Wang tileset snapshot v1", + "type": "object", + "additionalProperties": false, + "required": ["schema", "geometry", "directions", "colors", "tiles"], + "properties": { + "schema": { + "const": "wang-tileset-snapshot-v1" + }, + "geometry": { + "const": "square" + }, + "directions": { + "type": "array", + "prefixItems": [ + {"const": "N"}, + {"const": "E"}, + {"const": "S"}, + {"const": "W"} + ], + "minItems": 4, + "maxItems": 4 + }, + "colors": { + "type": "array", + "minItems": 1, + "uniqueItems": true, + "items": { + "$ref": "#/$defs/color" + } + }, + "tiles": { + "type": "array", + "minItems": 1, + "items": { + "type": "object", + "additionalProperties": false, + "required": ["tile_id", "edges"], + "properties": { + "tile_id": { + "type": "integer", + "minimum": 0 + }, + "edges": { + "$ref": "#/$defs/edges" + } + } + } + } + }, + "$defs": { + "color": { + "type": "integer", + "minimum": 0 + }, + "edges": { + "type": "object", + "additionalProperties": false, + "required": ["N", "E", "S", "W"], + "properties": { + "N": {"$ref": "#/$defs/color"}, + "E": {"$ref": "#/$defs/color"}, + "S": {"$ref": "#/$defs/color"}, + "W": {"$ref": "#/$defs/color"} + } + } + } +} diff --git a/tests/fixtures/pipeline_sat_explain/formula-5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815.json b/tests/fixtures/pipeline_sat_explain/formula-5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815.json new file mode 100644 index 0000000..e7775ba --- /dev/null +++ b/tests/fixtures/pipeline_sat_explain/formula-5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815.json @@ -0,0 +1,34 @@ +{ + "schema": "cm13-formula-snapshot-v1", + "source": { + "name": "pipeline_sat.cm13", + "sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542" + }, + "variable_count": 3, + "clauses": [ + { + "clause_id": 0, + "variables": [ + 0, + 0, + 1 + ] + }, + { + "clause_id": 1, + "variables": [ + 0, + 1, + 2 + ] + }, + { + "clause_id": 2, + "variables": [ + 1, + 2, + 2 + ] + } + ] +} diff --git a/tests/fixtures/pipeline_sat_explain/manifest.json b/tests/fixtures/pipeline_sat_explain/manifest.json new file mode 100644 index 0000000..173d555 --- /dev/null +++ b/tests/fixtures/pipeline_sat_explain/manifest.json @@ -0,0 +1,22 @@ +{ + "schema": "wang-explain-manifest-v1", + "stage": "region", + "source_formula_sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542", + "artifacts": { + "formula": { + "path": "formula-5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815.json", + "sha256": "5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815", + "schema": "cm13-formula-snapshot-v1" + }, + "tileset": { + "path": "tileset-462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa.json", + "sha256": "462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa", + "schema": "wang-tileset-snapshot-v1" + }, + "region": { + "path": "region-aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a.json", + "sha256": "aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a", + "schema": "wang-region-snapshot-v1" + } + } +} diff --git a/tests/fixtures/pipeline_sat_explain/region-aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a.json b/tests/fixtures/pipeline_sat_explain/region-aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a.json new file mode 100644 index 0000000..fa245cd --- /dev/null +++ b/tests/fixtures/pipeline_sat_explain/region-aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a.json @@ -0,0 +1,3137 @@ +{ + "schema": "wang-region-snapshot-v1", + "geometry": "square", + "source_formula_sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542", + "bounds": { + "min_x_inclusive": 0, + "min_y_inclusive": 0, + "max_x_inclusive": 40, + "max_y_inclusive": 10 + }, + "active": [ + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true + ], + "boundary": [ + { + "N": 0, + "E": null, + "S": null, + "W": 1 + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": 3, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": 2 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": 2, + "S": null, + "W": null + }, + null, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": 3, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": 2 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": 2, + "S": null, + "W": null + }, + null, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": 1 + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": 3, + "S": 0, + "W": null + } + ] +} diff --git a/tests/fixtures/pipeline_sat_explain/tileset-462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa.json b/tests/fixtures/pipeline_sat_explain/tileset-462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa.json new file mode 100644 index 0000000..41d70c7 --- /dev/null +++ b/tests/fixtures/pipeline_sat_explain/tileset-462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa.json @@ -0,0 +1,237 @@ +{ + "schema": "wang-tileset-snapshot-v1", + "geometry": "square", + "directions": [ + "N", + "E", + "S", + "W" + ], + "colors": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15 + ], + "tiles": [ + { + "tile_id": 0, + "edges": { + "N": 0, + "E": 2, + "S": 7, + "W": 1 + } + }, + { + "tile_id": 1, + "edges": { + "N": 7, + "E": 2, + "S": 8, + "W": 1 + } + }, + { + "tile_id": 2, + "edges": { + "N": 8, + "E": 2, + "S": 0, + "W": 1 + } + }, + { + "tile_id": 3, + "edges": { + "N": 0, + "E": 3, + "S": 0, + "W": 1 + } + }, + { + "tile_id": 4, + "edges": { + "N": 0, + "E": 4, + "S": 0, + "W": 2 + } + }, + { + "tile_id": 5, + "edges": { + "N": 0, + "E": 4, + "S": 9, + "W": 3 + } + }, + { + "tile_id": 6, + "edges": { + "N": 9, + "E": 3, + "S": 0, + "W": 2 + } + }, + { + "tile_id": 7, + "edges": { + "N": 0, + "E": 2, + "S": 0, + "W": 2 + } + }, + { + "tile_id": 8, + "edges": { + "N": 0, + "E": 3, + "S": 0, + "W": 3 + } + }, + { + "tile_id": 9, + "edges": { + "N": 5, + "E": 2, + "S": 5, + "W": 2 + } + }, + { + "tile_id": 10, + "edges": { + "N": 5, + "E": 3, + "S": 5, + "W": 3 + } + }, + { + "tile_id": 11, + "edges": { + "N": 0, + "E": 10, + "S": 6, + "W": 2 + } + }, + { + "tile_id": 12, + "edges": { + "N": 6, + "E": 2, + "S": 0, + "W": 10 + } + }, + { + "tile_id": 13, + "edges": { + "N": 0, + "E": 11, + "S": 6, + "W": 3 + } + }, + { + "tile_id": 14, + "edges": { + "N": 6, + "E": 3, + "S": 0, + "W": 11 + } + }, + { + "tile_id": 15, + "edges": { + "N": 6, + "E": 2, + "S": 12, + "W": 2 + } + }, + { + "tile_id": 16, + "edges": { + "N": 12, + "E": 2, + "S": 5, + "W": 2 + } + }, + { + "tile_id": 17, + "edges": { + "N": 6, + "E": 2, + "S": 13, + "W": 3 + } + }, + { + "tile_id": 18, + "edges": { + "N": 13, + "E": 3, + "S": 5, + "W": 2 + } + }, + { + "tile_id": 19, + "edges": { + "N": 6, + "E": 3, + "S": 14, + "W": 2 + } + }, + { + "tile_id": 20, + "edges": { + "N": 14, + "E": 2, + "S": 5, + "W": 3 + } + }, + { + "tile_id": 21, + "edges": { + "N": 6, + "E": 3, + "S": 15, + "W": 3 + } + }, + { + "tile_id": 22, + "edges": { + "N": 15, + "E": 3, + "S": 5, + "W": 3 + } + } + ] +} diff --git a/tests/python/test_pipeline_snapshot.py b/tests/python/test_pipeline_snapshot.py new file mode 100644 index 0000000..e392c22 --- /dev/null +++ b/tests/python/test_pipeline_snapshot.py @@ -0,0 +1,363 @@ +import copy +import hashlib +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +from formats.pipeline_snapshot import ( + FORMULA_SCHEMA, + MANIFEST_SCHEMA, + REGION_SCHEMA, + TILESET_SCHEMA, + PipelineSnapshotError, + build_formula_snapshot, + build_region_snapshot, + build_tileset_snapshot, + dump_pipeline_snapshots, + load_explainability_bundle, + load_pipeline_snapshot, + validate_explain_manifest, + validate_formula_snapshot, + validate_region_snapshot, + validate_tileset_snapshot, +) +from model.tileset import TILESET +from native.reduction_adapter import load_formula_and_region + + +ROOT = Path(__file__).resolve().parents[2] +SAT_PATH = ROOT / "tests/instances/pipeline_sat.cm13" +SOURCE_SHA256 = hashlib.sha256(SAT_PATH.read_bytes()).hexdigest() +COMMITTED_MANIFEST = ROOT / "tests/fixtures/pipeline_sat_explain/manifest.json" +SCHEMA_PATHS = { + FORMULA_SCHEMA: ROOT / "schemas/cm13-formula-snapshot-v1.schema.json", + TILESET_SCHEMA: ROOT / "schemas/wang-tileset-snapshot-v1.schema.json", + REGION_SCHEMA: ROOT / "schemas/wang-region-snapshot-v1.schema.json", + MANIFEST_SCHEMA: ROOT / "schemas/wang-explain-manifest-v1.schema.json", +} + + +def _snapshot_paths(manifest_path: Path) -> dict[str, Path]: + manifest = json.loads(manifest_path.read_text(encoding="utf-8")) + return { + "manifest": manifest_path, + **{ + name: manifest_path.parent / manifest["artifacts"][name]["path"] + for name in ("formula", "tileset", "region") + }, + } + + +class PipelineSnapshotTests(unittest.TestCase): + @classmethod + def setUpClass(cls) -> None: + cls.formula, cls.region = load_formula_and_region(SAT_PATH) + + def test_builders_create_closed_valid_snapshots(self) -> None: + formula = build_formula_snapshot( + self.formula, + source_name=SAT_PATH.name, + source_sha256=SOURCE_SHA256, + ) + tileset = build_tileset_snapshot() + region = build_region_snapshot( + self.region, + source_formula_sha256=SOURCE_SHA256, + origin=(-3, 5), + ) + + validate_formula_snapshot(formula) + validate_tileset_snapshot(tileset) + validate_region_snapshot(region) + self.assertEqual(formula["schema"], FORMULA_SCHEMA) + self.assertEqual(formula["variable_count"], 3) + self.assertEqual(len(formula["clauses"]), 3) + self.assertEqual(tileset["schema"], TILESET_SCHEMA) + self.assertEqual(len(tileset["tiles"]), len(TILESET)) + self.assertEqual(tileset["colors"], list(range(16))) + self.assertEqual(region["schema"], REGION_SCHEMA) + self.assertEqual(region["bounds"]["min_x_inclusive"], -3) + self.assertEqual(region["bounds"]["min_y_inclusive"], 5) + self.assertEqual(sum(region["active"]), 444) + self.assertEqual(region["active"].count(False), 7) + + with self.assertRaisesRegex(TypeError, "immutable N/E/S/W"): + build_tileset_snapshot(((0, 1),)) + + def test_publishes_four_closed_draft_2020_12_schemas(self) -> None: + for contract, path in SCHEMA_PATHS.items(): + with self.subTest(contract=contract): + schema = json.loads(path.read_text(encoding="utf-8")) + self.assertEqual( + schema["$schema"], + "https://json-schema.org/draft/2020-12/schema", + ) + self.assertEqual(schema["properties"]["schema"]["const"], contract) + self.assertFalse(schema["additionalProperties"]) + + def test_dump_is_deterministic_and_manifest_is_hash_bound(self) -> None: + with tempfile.TemporaryDirectory() as first_directory: + first_manifest = dump_pipeline_snapshots( + Path(first_directory) / "pipeline.explain.json", + SAT_PATH, + self.formula, + self.region, + ) + first_paths = _snapshot_paths(first_manifest) + first_bytes = { + name: path.read_bytes() for name, path in first_paths.items() + } + manifest, formula, tileset, region = load_explainability_bundle( + first_manifest + ) + + with tempfile.TemporaryDirectory() as second_directory: + second_manifest = dump_pipeline_snapshots( + Path(second_directory) / "pipeline.explain.json", + SAT_PATH, + self.formula, + self.region, + ) + second_paths = _snapshot_paths(second_manifest) + second_bytes = { + name: path.read_bytes() for name, path in second_paths.items() + } + + self.assertEqual(first_bytes, second_bytes) + committed_bytes = { + name: path.read_bytes() + for name, path in _snapshot_paths(COMMITTED_MANIFEST).items() + } + self.assertEqual(first_bytes, committed_bytes) + self.assertEqual(manifest["schema"], MANIFEST_SCHEMA) + self.assertEqual(formula["source"]["sha256"], SOURCE_SHA256) + self.assertEqual(len(tileset["tiles"]), 23) + self.assertEqual(sum(region["active"]), 444) + + def test_manifest_rejects_changed_artifact_bytes(self) -> None: + with tempfile.TemporaryDirectory() as directory: + manifest_path = dump_pipeline_snapshots( + Path(directory) / "pipeline.explain.json", + SAT_PATH, + self.formula, + self.region, + ) + paths = _snapshot_paths(manifest_path) + paths["formula"].write_bytes(paths["formula"].read_bytes() + b" ") + with self.assertRaisesRegex(PipelineSnapshotError, "does not match"): + load_explainability_bundle(manifest_path) + + def test_bundle_rejects_cross_stage_formula_identity(self) -> None: + with tempfile.TemporaryDirectory() as directory: + manifest_path = dump_pipeline_snapshots( + Path(directory) / "pipeline.explain.json", + SAT_PATH, + self.formula, + self.region, + ) + manifest = json.loads(manifest_path.read_text(encoding="utf-8")) + manifest["source_formula_sha256"] = "0" * 64 + manifest_path.write_text(json.dumps(manifest), encoding="utf-8") + with self.assertRaisesRegex( + PipelineSnapshotError, + "does not match formula artifact", + ): + load_explainability_bundle(manifest_path) + + def test_formula_rejects_bool_variable_and_noncanonical_clause_id(self) -> None: + document = build_formula_snapshot( + self.formula, + source_name=SAT_PATH.name, + source_sha256=SOURCE_SHA256, + ) + bool_variable = copy.deepcopy(document) + bool_variable["clauses"][0]["variables"][0] = True + with self.assertRaisesRegex(PipelineSnapshotError, "must be an integer"): + validate_formula_snapshot(bool_variable) + + wrong_id = copy.deepcopy(document) + wrong_id["clauses"][1]["clause_id"] = 0 + with self.assertRaisesRegex(PipelineSnapshotError, "canonical position"): + validate_formula_snapshot(wrong_id) + + def test_tileset_rejects_color_table_or_tile_id_drift(self) -> None: + document = build_tileset_snapshot() + colors = copy.deepcopy(document) + colors["colors"].append(99) + with self.assertRaisesRegex(PipelineSnapshotError, "colors used"): + validate_tileset_snapshot(colors) + + wrong_id = copy.deepcopy(document) + wrong_id["tiles"][2]["tile_id"] = 1 + with self.assertRaisesRegex(PipelineSnapshotError, "canonical table"): + validate_tileset_snapshot(wrong_id) + + def test_region_rejects_inactive_boundary_and_internal_constraint(self) -> None: + document = build_region_snapshot( + self.region, + source_formula_sha256=SOURCE_SHA256, + ) + inactive_index = document["active"].index(False) + inactive = copy.deepcopy(document) + inactive["boundary"][inactive_index] = { + "N": None, + "E": None, + "S": None, + "W": None, + } + with self.assertRaisesRegex(PipelineSnapshotError, "inactive position"): + validate_region_snapshot(inactive) + + internal = copy.deepcopy(document) + internal["boundary"][0]["E"] = 0 + with self.assertRaisesRegex(PipelineSnapshotError, "shared by active"): + validate_region_snapshot(internal) + + def test_manifest_rejects_parent_path_and_unknown_fields(self) -> None: + with tempfile.TemporaryDirectory() as directory: + manifest_path = dump_pipeline_snapshots( + Path(directory) / "pipeline.explain.json", + SAT_PATH, + self.formula, + self.region, + ) + document = json.loads(manifest_path.read_text(encoding="utf-8")) + traversal = copy.deepcopy(document) + traversal["artifacts"]["formula"]["path"] = "../formula.json" + with self.assertRaisesRegex(PipelineSnapshotError, "artifact basename"): + validate_explain_manifest(traversal) + + extra = copy.deepcopy(document) + extra["render"] = {} + with self.assertRaisesRegex(PipelineSnapshotError, "unknown fields"): + validate_explain_manifest(extra) + + def test_strict_loader_rejects_duplicate_members(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = Path(directory) / "duplicate.json" + path.write_text( + '{"schema":"wang-region-snapshot-v1","schema":"duplicate"}', + encoding="utf-8", + ) + with self.assertRaisesRegex(PipelineSnapshotError, "duplicate member"): + load_pipeline_snapshot(path) + + path.write_text('{"schema":[]}', encoding="utf-8") + with self.assertRaisesRegex( + PipelineSnapshotError, + "must be a string", + ): + load_pipeline_snapshot(path) + + def test_manifest_replace_failure_preserves_existing_output(self) -> None: + with tempfile.TemporaryDirectory() as directory: + destination = Path(directory) / "pipeline.explain.json" + destination.write_bytes(b"previous manifest") + real_replace = __import__("os").replace + + def fail_manifest_replace(source, target): + if Path(target) == destination: + raise OSError("injected manifest replace failure") + real_replace(source, target) + + with patch( + "formats.pipeline_snapshot.os.replace", + side_effect=fail_manifest_replace, + ): + with self.assertRaisesRegex( + PipelineSnapshotError, + "injected manifest replace failure", + ): + dump_pipeline_snapshots( + destination, + SAT_PATH, + self.formula, + self.region, + ) + self.assertEqual(destination.read_bytes(), b"previous manifest") + self.assertFalse(list(Path(directory).glob(".*.tmp"))) + + def test_manifest_name_collision_is_rejected_before_overwrite(self) -> None: + formula = build_formula_snapshot( + self.formula, + source_name=SAT_PATH.name, + source_sha256=SOURCE_SHA256, + ) + encoded = f"{json.dumps(formula, ensure_ascii=False, indent=2)}\n".encode() + digest = hashlib.sha256(encoded).hexdigest() + with tempfile.TemporaryDirectory() as directory: + destination = Path(directory) / f"formula-{digest}.json" + destination.write_bytes(b"existing manifest") + + with self.assertRaisesRegex(PipelineSnapshotError, "must not collide"): + dump_pipeline_snapshots( + destination, + SAT_PATH, + self.formula, + self.region, + ) + + self.assertEqual(destination.read_bytes(), b"existing manifest") + + def test_exported_bundle_loads_without_site_packages_or_native_library( + self, + ) -> None: + with tempfile.TemporaryDirectory() as directory: + manifest_path = dump_pipeline_snapshots( + Path(directory) / "pipeline.explain.json", + SAT_PATH, + self.formula, + self.region, + ) + script = ( + "import sys; " + "from formats.pipeline_snapshot import load_explainability_bundle; " + "bundle=load_explainability_bundle(sys.argv[1]); " + "assert bundle[0]['schema']=='wang-explain-manifest-v1'; " + "assert 'z3' not in sys.modules and 'native._lib' not in sys.modules" + ) + environment = {"PYTHONPATH": str(ROOT / "python")} + completed = subprocess.run( + [sys.executable, "-S", "-B", "-c", script, str(manifest_path)], + cwd=ROOT, + env=environment, + capture_output=True, + text=True, + check=False, + ) + self.assertEqual(completed.returncode, 0, completed.stderr) + + def test_cli_exports_the_real_formula_to_region_pipeline(self) -> None: + with tempfile.TemporaryDirectory() as directory: + manifest_path = Path(directory) / "nested" / "manifest.json" + completed = subprocess.run( + [ + sys.executable, + str(ROOT / "tools/export_pipeline_snapshots.py"), + str(SAT_PATH), + str(manifest_path), + "--origin-x", + "-7", + "--origin-y", + "4", + ], + cwd=ROOT, + capture_output=True, + text=True, + check=False, + ) + bundle = load_explainability_bundle(manifest_path) + + self.assertEqual(completed.returncode, 0, completed.stderr) + self.assertIn(f"manifest={manifest_path}", completed.stdout) + self.assertEqual(bundle[1]["source"]["name"], SAT_PATH.name) + self.assertEqual(bundle[3]["bounds"]["min_x_inclusive"], -7) + self.assertEqual(bundle[3]["bounds"]["min_y_inclusive"], 4) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/export_pipeline_snapshots.py b/tools/export_pipeline_snapshots.py new file mode 100644 index 0000000..79febe8 --- /dev/null +++ b/tools/export_pipeline_snapshots.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 +"""Export static explainability snapshots from one real CM13 reduction.""" + +from __future__ import annotations + +import argparse +from pathlib import Path +import sys + + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "python")) + +from formats.pipeline_snapshot import ( # noqa: E402 + dump_pipeline_snapshots, + load_pipeline_snapshot, +) +from native.reduction_adapter import load_formula_and_region # noqa: E402 + + +def _parser() -> argparse.ArgumentParser: + parser = argparse.ArgumentParser( + description=( + "parse a CM13 formula, build its Yang-Zhang region, and export " + "hash-bound static snapshots for the isolated renderer" + ) + ) + parser.add_argument("source", type=Path, help="input .cm13 formula") + parser.add_argument("manifest", type=Path, help="output manifest JSON") + parser.add_argument("--origin-x", type=int, default=0) + parser.add_argument("--origin-y", type=int, default=0) + return parser + + +def main(arguments: list[str] | None = None) -> int: + args = _parser().parse_args(arguments) + args.manifest.parent.mkdir(parents=True, exist_ok=True) + formula, region = load_formula_and_region(args.source) + manifest_path = dump_pipeline_snapshots( + args.manifest, + args.source, + formula, + region, + origin=(args.origin_x, args.origin_y), + ) + manifest = load_pipeline_snapshot(manifest_path) + artifacts = manifest["artifacts"] + print(f"manifest={manifest_path}") + for name in ("formula", "tileset", "region"): + artifact_path = manifest_path.parent / artifacts[name]["path"] + print(f"{name}={artifact_path}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())