Export verified square Wang solutions

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
 

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.

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