diff --git a/README.md b/README.md index 7482fc4..140af67 100644 --- a/README.md +++ b/README.md @@ -230,6 +230,9 @@ Implemented and tested as of 25 August 2026: - a scoped Python cross-check coordinator that connects Boolean Z3 to native witness extension, extracts assignments from native or Wang-Z3 tilings, and retains copied counterexamples across native cleanup; +- a solver-neutral Python tiling-result model and a native-only coordinator + that solves either serial path, copies the result out of its native lifetime, + and requires the independent Python checker without importing Z3; - exhaustive witness-level evidence over all 1,701 canonical formulas through three variables, every one of their `2^n` assignments, and both native solver entry points: direct Boolean validity agrees with extension SAT, and every @@ -243,6 +246,10 @@ Implemented and tested as of 25 August 2026: - a JSON Lines comparison suite over fixed `.cm13` inputs, with separate prepared-Region and file-to-verified-decision scopes for the native reference, native optimized, Boolean Z3, and Wang Z3 paths; +- the closed `wang-solution-v1` square SAT contract, its dependency-free + semantic validator, and a deterministic Python exporter that validates SAT + status, dense cells, canonical tile IDs, boundary constraints, and + adjacency before writing a self-contained JSON document; - a provenance-pinned PAP Render snapshot under `renderer/`, preserving its standalone Python 3.14 project and 144-test suite without coupling its graphical dependencies to the native core or Python reference tools; @@ -253,7 +260,7 @@ Not implemented yet: - native OpenMP solver; - square-to-hex translation and verification; -- JSON export and renderer integration. +- Wang square and hex renderer integration. ## Next milestones @@ -266,7 +273,7 @@ Development proceeds through small, testable modules: 3. evaluate propagation scheduling and OpenMP only after the serial mechanisms meet their gates; 4. implement and verify the square-to-hex translation; -5. stabilize JSON and renderer integration last. +5. connect verified solution documents to the isolated renderer last. 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 @@ -378,6 +385,7 @@ src/verify/ independent tiling verification src/io/ formula parsing and serialization python/model/ pure Python data contracts python/native/ C ABI adapters and ownership boundaries +python/formats/ versioned solution validation and deterministic export python/crosscheck/ scoped native/Z3 witness orchestration python/oracles/ independent Z3 oracles and witness checks python/hex/ square-to-hex translation and verifier @@ -391,9 +399,11 @@ The C parser is canonical for native input. Native adapters copy data into Python-owned models and never expose C pointers. Oracles accept models rather than paths: the Boolean oracle consumes `Formula`, while the Wang oracle consumes `Region + TILESET`. Both witness checkers are pure Python and -independent of Z3. The cross-check layer alone coordinates those components -with scoped native lifetimes; Python does not duplicate parsing or the -Yang–Zhang reduction. +independent of Z3. The cross-check layer coordinates Boolean/Wang witness +relations, while the smaller native-only solve coordinator supplies verified +tilings to producers without importing either Z3 oracle. Both paths keep +native lifetimes scoped; Python does not duplicate parsing or the Yang–Zhang +reduction. ## Documentation diff --git a/docs/wang_solution_v1.md b/docs/wang_solution_v1.md index d270d4d..0e68678 100644 --- a/docs/wang_solution_v1.md +++ b/docs/wang_solution_v1.md @@ -29,6 +29,46 @@ The machine-readable structural definition is is `python/formats/wang_solution.py`, and the representative golden document is `tests/fixtures/wang_solution_v1_square_sat.json`. +## Producing a document + +`python/formats/wang_solution_export.py` builds the contract from the immutable +Python `Region`, a solver-neutral `TilingSolveResult`, the canonical `TILESET`, +an explicit coordinate origin, and optional non-semantic metadata. The +producer rejects UNSAT and UNKNOWN results, malformed dense storage, assignments +to holes, absent tile IDs, and tilings rejected by the independent Python +checker. It then validates the complete document with +`validate_wang_solution()` before writing any output. + +The native-only coordinator parses, builds, and solves within scoped C +lifetimes, copies the region and result, and runs the Python checker without +importing or invoking Z3: + +```python +from formats.wang_solution_export import dump_wang_solution +from native.solve_pipeline import solve_native_tiling + +region, result = solve_native_tiling("input.cm13", optimized=True) +dump_wang_solution( + "solution.json", + region, + result, + origin=(0, 0), + metadata={"producer": "native-optimized"}, +) +``` + +The producer loads `libwang.so`; the resulting JSON does not. A downstream +consumer receives only the versioned document and never needs the native +library, Z3, solver domains, or Python producer modules. + +Serialization is deterministic for the same semantic inputs: contract fields, +tile directions, and dense arrays have fixed order; metadata is copied and its +object keys are ordered recursively; output is UTF-8 with two-space indentation +and one final newline. The complete document is encoded before the destination +is opened, then installed with an atomic same-directory replace; an invalid +input or failed replace leaves an existing output unchanged. The exporter does +not synthesize timestamps, hostnames, commit IDs, or other changing metadata. + ## Fields and ordering The top-level fields are closed and have these meanings: @@ -106,7 +146,9 @@ JSON parsers. diagnostics. Its contents must never select a tile, change coordinates, override a boundary color, affect SAT status, or be required to reproduce the tiling. Semantic validation deliberately ignores the entire object after -checking that it contains JSON values. +checking that it contains JSON values. The exporter deep-copies those values +and rejects cycles, non-string object keys, non-finite numbers, invalid UTF-8 +text, and non-JSON Python objects. ## Versioning @@ -119,4 +161,8 @@ placing it there does not expand the correctness contract. The golden fixture spans inclusive bounds `[-1,2]` through `[2,4]`: twelve dense positions, ten active cells, and two holes. Its complete 23-entry table is tested for exact `(N,E,S,W)` parity with the canonical Python `TILESET`, and -targeted mutations exercise every cross-field rejection above. +targeted mutations exercise every cross-field rejection above. Export tests +reconstruct the same document from `Region + TilingSolveResult`, while separate +integration tests export real SAT witnesses from both native serial paths and +reject their shared UNSAT fixture. The compact golden is therefore not tied to +one permissible solver search witness. diff --git a/python/formats/wang_solution_export.py b/python/formats/wang_solution_export.py new file mode 100644 index 0000000..b17678f --- /dev/null +++ b/python/formats/wang_solution_export.py @@ -0,0 +1,254 @@ +"""Deterministic producer for verified ``wang-solution-v1`` documents.""" + +from __future__ import annotations + +import json +import math +import os +from pathlib import Path +import tempfile + +from formats.wang_solution import ( + GEOMETRY, + SCHEMA_NAME, + STATUS, + validate_wang_solution, +) +from model.region import Region +from model.tiling import TilingSolveResult, TilingSolveStatus +from model.tileset import COLOR_NONE, TILESET +from oracles.tiling_check import is_valid_tiling + + +_DIRECTIONS = ("N", "E", "S", "W") + + +class WangSolutionExportError(ValueError): + """Raised when producer inputs cannot form a v1 SAT document.""" + + +def _copy_json_string(value: str, path: str) -> str: + try: + value.encode("utf-8") + except UnicodeEncodeError as error: + raise WangSolutionExportError( + f"{path} must contain valid UTF-8 text" + ) from error + return value + + +def _copy_json_value( + value: object, + path: str, + active_containers: set[int], +) -> object: + if value is None or type(value) in (bool, int): + return value + if type(value) is str: + return _copy_json_string(value, path) + if type(value) is float: + if not math.isfinite(value): + raise WangSolutionExportError( + f"{path} must not contain a non-finite number" + ) + return value + if type(value) is list: + identity = id(value) + if identity in active_containers: + raise WangSolutionExportError(f"{path} must not contain a cycle") + active_containers.add(identity) + try: + return [ + _copy_json_value( + item, + f"{path}[{index}]", + active_containers, + ) + for index, item in enumerate(value) + ] + finally: + active_containers.remove(identity) + if type(value) is dict: + if any(type(key) is not str for key in value): + raise WangSolutionExportError( + f"{path} object member names must be strings" + ) + identity = id(value) + if identity in active_containers: + raise WangSolutionExportError(f"{path} must not contain a cycle") + active_containers.add(identity) + try: + for key in value: + _copy_json_string(key, f"{path} object member name") + return { + key: _copy_json_value( + value[key], + f"{path}.{key}", + active_containers, + ) + for key in sorted(value) + } + finally: + active_containers.remove(identity) + raise WangSolutionExportError(f"{path} must contain only JSON values") + + +def _copy_metadata(metadata: dict[str, object] | None) -> dict[str, object]: + if metadata is None: + return {} + if type(metadata) is not dict: + raise WangSolutionExportError("metadata must be a JSON object") + copied = _copy_json_value(metadata, "metadata", set()) + assert type(copied) is dict + return copied + + +def _validate_origin(origin: tuple[int, int]) -> tuple[int, int]: + if ( + type(origin) is not tuple + or len(origin) != 2 + or any(type(coordinate) is not int for coordinate in origin) + ): + raise WangSolutionExportError( + "origin must be an immutable pair of integer coordinates" + ) + return origin + + +def _validated_tiling( + region: Region, + result: TilingSolveResult, +) -> tuple[int | None, ...]: + if not isinstance(region, Region): + raise TypeError("region must be a Region") + if not isinstance(result, TilingSolveResult): + raise TypeError("result must be a TilingSolveResult") + if result.status is not TilingSolveStatus.SAT or result.tiling is None: + raise WangSolutionExportError("only a SAT result can be exported") + + tiling = result.tiling + if len(tiling) != region.width * region.height: + raise WangSolutionExportError( + "tiling length must match the region dimensions" + ) + for index, (active, tile_id) in enumerate( + zip(region.active, tiling, strict=True) + ): + if not active: + if tile_id is not None: + raise WangSolutionExportError( + f"inactive cell {index} must contain None" + ) + continue + if type(tile_id) is not int or not 0 <= tile_id < len(TILESET): + raise WangSolutionExportError( + f"active cell {index} must contain a canonical tile ID" + ) + + if not is_valid_tiling(region, TILESET, tiling): + raise WangSolutionExportError( + "tiling does not satisfy the region boundary and adjacency constraints" + ) + return tiling + + +def build_wang_solution( + region: Region, + result: TilingSolveResult, + *, + origin: tuple[int, int], + metadata: dict[str, object] | None = None, +) -> dict[str, object]: + """Build and validate one self-contained square SAT solution document.""" + min_x, min_y = _validate_origin(origin) + tiling = _validated_tiling(region, result) + copied_metadata = _copy_metadata(metadata) + + tile_table = [ + { + "tile_id": tile_id, + "edges": { + direction: tile[direction_index] + for direction_index, direction in enumerate(_DIRECTIONS) + }, + } + for tile_id, tile in enumerate(TILESET) + ] + 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": SCHEMA_NAME, + "status": STATUS, + "geometry": GEOMETRY, + "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, + }, + "tile_table": tile_table, + "cells": list(tiling), + "boundary": boundary, + "metadata": copied_metadata, + } + validate_wang_solution(document) + return document + + +def dump_wang_solution( + path: str | Path, + region: Region, + result: TilingSolveResult, + *, + origin: tuple[int, int], + metadata: dict[str, object] | None = None, +) -> None: + """Validate and atomically write a deterministic UTF-8 v1 document.""" + document = build_wang_solution( + region, + result, + origin=origin, + metadata=metadata, + ) + serialized = json.dumps( + document, + ensure_ascii=False, + allow_nan=False, + indent=2, + ) + encoded = f"{serialized}\n".encode("utf-8") + destination = Path(path) + temporary: Path | None = None + try: + with tempfile.NamedTemporaryFile( + mode="wb", + dir=destination.parent, + prefix=f".{destination.name}.", + suffix=".tmp", + delete=False, + ) as stream: + temporary = Path(stream.name) + stream.write(encoded) + os.replace(temporary, destination) + temporary = None + finally: + if temporary is not None: + try: + temporary.unlink() + except FileNotFoundError: + pass diff --git a/python/model/tiling.py b/python/model/tiling.py new file mode 100644 index 0000000..6a62471 --- /dev/null +++ b/python/model/tiling.py @@ -0,0 +1,27 @@ +"""Solver-neutral result contract for dense Wang tilings.""" + +from dataclasses import dataclass +from enum import Enum + + +class TilingSolveStatus(Enum): + SAT = "sat" + UNSAT = "unsat" + UNKNOWN = "unknown" + + +@dataclass(frozen=True, slots=True) +class TilingSolveResult: + """A SAT result owns one dense tiling; other statuses own none.""" + + status: TilingSolveStatus + tiling: tuple[int | None, ...] | None = None + + def __post_init__(self) -> None: + if type(self.status) is not TilingSolveStatus: + raise TypeError("status must be a TilingSolveStatus") + if self.tiling is not None and type(self.tiling) is not tuple: + raise TypeError("tiling storage must be an immutable tuple") + has_tiling = self.tiling is not None + if has_tiling != (self.status is TilingSolveStatus.SAT): + raise ValueError("only SAT results carry a tiling") diff --git a/python/native/solve_pipeline.py b/python/native/solve_pipeline.py new file mode 100644 index 0000000..bd5875e --- /dev/null +++ b/python/native/solve_pipeline.py @@ -0,0 +1,42 @@ +"""Native-only Wang solve orchestration over one reduction lifetime.""" + +from model.region import Region +from model.tiling import TilingSolveResult, TilingSolveStatus +from model.tileset import TILESET +from native.formula_adapter import PathLike, _loaded_formula +from native.region_adapter import _built_reduction, _copy_region +from native.witness_adapter import NativeWitnessError, _solve_native +from oracles.tiling_check import is_valid_tiling + + +def solve_native_tiling( + path: PathLike, + optimized: bool = False, +) -> tuple[Region, TilingSolveResult]: + """Solve one parsed reduction without importing or invoking Z3. + + Native formula, reduction, and result storage are destroyed before the + copied Python ``Region`` and ``TilingSolveResult`` reach the caller. Every + SAT witness also passes the independent pure-Python tiling checker. + """ + if type(optimized) is not bool: + raise TypeError("optimized must be a boolean") + + with _loaded_formula(path) as native_formula: + with _built_reduction(native_formula) as native_reduction: + region = _copy_region(native_reduction.region) + result = _solve_native( + native_reduction, + region, + optimized=optimized, + ) + if result.status is TilingSolveStatus.SAT: + if result.tiling is None or not is_valid_tiling( + region, + TILESET, + result.tiling, + ): + raise NativeWitnessError( + "native SAT tiling was rejected by the Python checker" + ) + return region, result diff --git a/python/native/witness_adapter.py b/python/native/witness_adapter.py index 152fe0c..b37c091 100644 --- a/python/native/witness_adapter.py +++ b/python/native/witness_adapter.py @@ -18,11 +18,11 @@ from functools import cache from model.region import Region +from model.tiling import TilingSolveResult, TilingSolveStatus from model.tileset import TILE_COUNT from native._lib import library from native.formula_adapter import _Cm13Formula from native.region_adapter import _Region, _YangZhangReduction -from oracles.tiling_solver import TilingSolveResult, TilingSolveStatus _TILE_NONE = 255 diff --git a/python/oracles/tiling_solver.py b/python/oracles/tiling_solver.py index a685ea1..35fb5de 100644 --- a/python/oracles/tiling_solver.py +++ b/python/oracles/tiling_solver.py @@ -1,11 +1,9 @@ """Independent Wang-tiling Z3 oracle over the pure Python Region model.""" -from dataclasses import dataclass -from enum import Enum - from z3 import And, ArithRef, Int, Or, Solver, sat, unsat from model.region import Region +from model.tiling import TilingSolveResult, TilingSolveStatus from model.tileset import ( COLOR_COUNT, COLOR_NONE, @@ -17,23 +15,6 @@ ) -class TilingSolveStatus(Enum): - SAT = "sat" - UNSAT = "unsat" - UNKNOWN = "unknown" - - -@dataclass(frozen=True, slots=True) -class TilingSolveResult: - status: TilingSolveStatus - tiling: tuple[int | None, ...] | None = None - - def __post_init__(self) -> None: - has_tiling = self.tiling is not None - if has_tiling != (self.status is TilingSolveStatus.SAT): - raise ValueError("only SAT results carry a tiling") - - def _validate_tileset(tileset: Tileset) -> None: if type(tileset) is not tuple: raise TypeError("tileset must be a tuple") diff --git a/tests/python/test_native_solve_pipeline.py b/tests/python/test_native_solve_pipeline.py new file mode 100644 index 0000000..c4cb100 --- /dev/null +++ b/tests/python/test_native_solve_pipeline.py @@ -0,0 +1,152 @@ +import os +from pathlib import Path +import subprocess +import sys +import tempfile +import textwrap +import unittest +from unittest.mock import patch + +from formats.wang_solution import load_wang_solution, validate_wang_solution +from formats.wang_solution_export import ( + WangSolutionExportError, + build_wang_solution, +) +from model.tiling import TilingSolveStatus +from model.tileset import TILESET +from native.solve_pipeline import solve_native_tiling +from native.witness_adapter import NativeWitnessError +from oracles.tiling_check import is_valid_tiling + + +ROOT = Path(__file__).resolve().parents[2] +SAT_PATH = ROOT / "tests/instances/pipeline_sat.cm13" +UNSAT_PATH = ROOT / "tests/instances/pipeline_unsat.cm13" + + +class NativeSolvePipelineTests(unittest.TestCase): + def test_real_native_results_export_without_z3_oracles(self) -> None: + for optimized in (False, True): + with self.subTest(optimized=optimized, expected="SAT"): + region, result = solve_native_tiling( + SAT_PATH, + optimized=optimized, + ) + self.assertIs(result.status, TilingSolveStatus.SAT) + self.assertIsNotNone(result.tiling) + self.assertTrue(is_valid_tiling(region, TILESET, result.tiling)) + validate_wang_solution( + build_wang_solution(region, result, origin=(0, 0)) + ) + + with self.subTest(optimized=optimized, expected="UNSAT"): + region, result = solve_native_tiling( + UNSAT_PATH, + optimized=optimized, + ) + self.assertIs(result.status, TilingSolveStatus.UNSAT) + self.assertIsNone(result.tiling) + with self.assertRaises(WangSolutionExportError): + build_wang_solution(region, result, origin=(0, 0)) + + def test_sat_result_must_pass_the_independent_python_checker(self) -> None: + with patch( + "native.solve_pipeline.is_valid_tiling", + return_value=False, + ): + with self.assertRaisesRegex( + NativeWitnessError, + "rejected by the Python checker", + ): + solve_native_tiling(SAT_PATH) + + def test_optimized_selector_is_strictly_boolean(self) -> None: + with self.assertRaisesRegex(TypeError, "optimized must be a boolean"): + solve_native_tiling(SAT_PATH, optimized=1) + + def test_native_export_runs_without_site_packages_or_z3(self) -> None: + script = textwrap.dedent( + """ + import sys + from pathlib import Path + + from formats.wang_solution_export import dump_wang_solution + from model.tiling import TilingSolveStatus + from native.solve_pipeline import solve_native_tiling + + source = Path(sys.argv[1]) + destination = Path(sys.argv[2]) + region, result = solve_native_tiling(source, optimized=True) + assert result.status is TilingSolveStatus.SAT + dump_wang_solution( + destination, + region, + result, + origin=(0, 0), + metadata={"producer": "native-optimized"}, + ) + assert "z3" not in sys.modules + """ + ) + environment = os.environ.copy() + environment["PYTHONPATH"] = str(ROOT / "python") + with tempfile.TemporaryDirectory() as temporary_directory: + destination = Path(temporary_directory) / "native-solution.json" + completed = subprocess.run( + [ + sys.executable, + "-S", + "-B", + "-c", + script, + str(SAT_PATH), + str(destination), + ], + cwd=ROOT, + env=environment, + check=False, + capture_output=True, + text=True, + ) + + self.assertEqual(completed.returncode, 0, completed.stderr) + self.assertEqual( + load_wang_solution(destination)["metadata"], + {"producer": "native-optimized"}, + ) + + def test_stdlib_consumer_loads_the_fixture_without_native_or_z3(self) -> None: + script = textwrap.dedent( + """ + import sys + from formats.wang_solution import load_wang_solution + + document = load_wang_solution(sys.argv[1]) + assert document["status"] == "SAT" + assert "native._lib" not in sys.modules + assert "z3" not in sys.modules + """ + ) + environment = os.environ.copy() + environment["PYTHONPATH"] = str(ROOT / "python") + completed = subprocess.run( + [ + sys.executable, + "-S", + "-B", + "-c", + script, + str(ROOT / "tests/fixtures/wang_solution_v1_square_sat.json"), + ], + cwd=ROOT, + env=environment, + check=False, + capture_output=True, + text=True, + ) + + self.assertEqual(completed.returncode, 0, completed.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/python/test_wang_solution_export.py b/tests/python/test_wang_solution_export.py new file mode 100644 index 0000000..6d7eeb1 --- /dev/null +++ b/tests/python/test_wang_solution_export.py @@ -0,0 +1,297 @@ +import json +from pathlib import Path +import tempfile +import unittest +from unittest.mock import patch + +from formats.wang_solution import load_wang_solution +from formats.wang_solution_export import ( + WangSolutionExportError, + build_wang_solution, + dump_wang_solution, +) +from model.region import Region +from model.tiling import TilingSolveResult, TilingSolveStatus +from model.tileset import COLOR_NONE, TILE_COUNT + + +ROOT = Path(__file__).resolve().parents[2] +FIXTURE = ROOT / "tests/fixtures/wang_solution_v1_square_sat.json" + + +def _golden_region() -> Region: + none = COLOR_NONE + return Region( + width=4, + height=3, + active=( + True, + True, + False, + True, + True, + True, + False, + True, + True, + True, + True, + True, + ), + boundary=( + (0, none, none, 2), + (0, 2, none, none), + (none, none, none, none), + (0, 2, none, 2), + (none, none, none, 2), + (none, 2, none, none), + (none, none, none, none), + (none, 2, none, 2), + (none, none, 0, 2), + (none, none, 0, none), + (0, none, 0, none), + (none, 2, 0, none), + ), + ) + + +def _golden_result() -> TilingSolveResult: + return TilingSolveResult( + TilingSolveStatus.SAT, + (7, 7, None, 7, 7, 7, None, 7, 7, 7, 7, 7), + ) + + +class TilingSolveResultModelTests(unittest.TestCase): + def test_rejects_non_enum_status_and_mutable_storage(self) -> None: + with self.assertRaisesRegex(TypeError, "status must be"): + TilingSolveResult("sat") + with self.assertRaisesRegex(TypeError, "immutable tuple"): + TilingSolveResult(TilingSolveStatus.SAT, [7]) + + +class WangSolutionBuildTests(unittest.TestCase): + def test_builds_the_existing_golden_fixture_from_models(self) -> None: + with FIXTURE.open(encoding="utf-8") as stream: + expected = json.load(stream) + + document = build_wang_solution( + _golden_region(), + _golden_result(), + origin=(-1, 2), + metadata={ + "fixture": "canonical-tileset-square-with-holes", + "note": "This object is not used to establish tiling correctness.", + }, + ) + + self.assertEqual(document, expected) + + def test_copies_and_recursively_orders_metadata(self) -> None: + metadata = { + "z": {"second": [2, {"z": 0, "a": 1}], "first": True}, + "a": "first", + } + document = build_wang_solution( + _golden_region(), + _golden_result(), + origin=(0, 0), + metadata=metadata, + ) + copied = document["metadata"] + assert type(copied) is dict + + self.assertEqual(list(copied), ["a", "z"]) + nested = copied["z"] + assert type(nested) is dict + self.assertEqual(list(nested), ["first", "second"]) + metadata["z"]["second"][1]["a"] = 99 + self.assertEqual(nested["second"][1]["a"], 1) + + def test_rejects_non_sat_results_and_invalid_origins(self) -> None: + for status in (TilingSolveStatus.UNSAT, TilingSolveStatus.UNKNOWN): + with self.subTest(status=status): + with self.assertRaisesRegex( + WangSolutionExportError, + "only a SAT result", + ): + build_wang_solution( + _golden_region(), + TilingSolveResult(status), + origin=(0, 0), + ) + + for origin in ((0, False), [0, 0], (0,), (0, 0, 0)): + with self.subTest(origin=origin): + with self.assertRaisesRegex( + WangSolutionExportError, + "origin must be", + ): + build_wang_solution( + _golden_region(), + _golden_result(), + origin=origin, + ) + + def test_rejects_wrong_dimensions_inactive_values_and_tile_ids(self) -> None: + valid = list(_golden_result().tiling) + mutations = { + "short dimensions": valid[:-1], + "inactive assignment": valid[:2] + [7] + valid[3:], + "active None": [None] + valid[1:], + "boolean tile ID": [True] + valid[1:], + "negative tile ID": [-1] + valid[1:], + "absent tile ID": [TILE_COUNT] + valid[1:], + } + + for name, tiling in mutations.items(): + with self.subTest(name=name): + with self.assertRaises(WangSolutionExportError): + build_wang_solution( + _golden_region(), + TilingSolveResult( + TilingSolveStatus.SAT, + tuple(tiling), + ), + origin=(0, 0), + ) + + def test_rejects_boundary_and_adjacency_violations(self) -> None: + none = COLOR_NONE + boundary_mismatch = Region( + width=1, + height=1, + active=(True,), + boundary=((1, none, none, none),), + ) + adjacency_mismatch = Region( + width=2, + height=1, + active=(True, True), + boundary=((none,) * 4, (none,) * 4), + ) + invalid = ( + ( + boundary_mismatch, + TilingSolveResult(TilingSolveStatus.SAT, (7,)), + ), + ( + adjacency_mismatch, + TilingSolveResult(TilingSolveStatus.SAT, (7, 8)), + ), + ) + + for region, result in invalid: + with self.subTest(region=region): + with self.assertRaisesRegex( + WangSolutionExportError, + "boundary and adjacency", + ): + build_wang_solution(region, result, origin=(0, 0)) + + def test_rejects_metadata_outside_strict_json(self) -> None: + cyclic: dict[str, object] = {} + cyclic["self"] = cyclic + invalid = ( + [], + {1: "integer key"}, + {"tuple": (1, 2)}, + {"nan": float("nan")}, + {"infinity": float("inf")}, + {"surrogate": "\ud800"}, + cyclic, + ) + for metadata in invalid: + with self.subTest(metadata=metadata): + with self.assertRaises(WangSolutionExportError): + build_wang_solution( + _golden_region(), + _golden_result(), + origin=(0, 0), + metadata=metadata, + ) + + +class WangSolutionDumpTests(unittest.TestCase): + def test_dump_is_deterministic_and_round_trips_through_the_strict_loader( + self, + ) -> None: + first_metadata = { + "z": {"z": 2, "a": 1}, + "a": "ordered", + } + second_metadata = { + "a": "ordered", + "z": {"a": 1, "z": 2}, + } + with tempfile.TemporaryDirectory() as temporary_directory: + first = Path(temporary_directory) / "first.json" + second = Path(temporary_directory) / "second.json" + dump_wang_solution( + first, + _golden_region(), + _golden_result(), + origin=(-1, 2), + metadata=first_metadata, + ) + dump_wang_solution( + second, + _golden_region(), + _golden_result(), + origin=(-1, 2), + metadata=second_metadata, + ) + + self.assertEqual(first.read_bytes(), second.read_bytes()) + self.assertTrue(first.read_bytes().endswith(b"\n")) + self.assertEqual( + load_wang_solution(first), + load_wang_solution(second), + ) + + def test_invalid_input_does_not_replace_an_existing_output(self) -> None: + with tempfile.TemporaryDirectory() as temporary_directory: + destination = Path(temporary_directory) / "solution.json" + destination.write_text("preserve me\n", encoding="utf-8") + + with self.assertRaises(WangSolutionExportError): + dump_wang_solution( + destination, + _golden_region(), + TilingSolveResult(TilingSolveStatus.UNSAT), + origin=(0, 0), + ) + + self.assertEqual( + destination.read_text(encoding="utf-8"), + "preserve me\n", + ) + + def test_write_failure_preserves_existing_output_and_removes_temporary( + self, + ) -> None: + with tempfile.TemporaryDirectory() as temporary_directory: + destination = Path(temporary_directory) / "solution.json" + destination.write_text("preserve me\n", encoding="utf-8") + + with patch( + "formats.wang_solution_export.os.replace", + side_effect=OSError("replace failed"), + ): + with self.assertRaisesRegex(OSError, "replace failed"): + dump_wang_solution( + destination, + _golden_region(), + _golden_result(), + origin=(0, 0), + ) + + self.assertEqual( + destination.read_text(encoding="utf-8"), + "preserve me\n", + ) + self.assertEqual(list(Path(temporary_directory).iterdir()), [destination]) + + +if __name__ == "__main__": + unittest.main()