Wang solution v1 data contract

Scope

wang-solution-v1 is the boundary between a producer of a verified square Wang tiling and downstream tools such as a renderer. It is a SAT-only data contract: status is always SAT, geometry is always square, and every active position selects one tile. UNSAT and UNKNOWN outcomes are not solution documents.

The format contains no native pointers, solver domains, search traces, Yang–Zhang swap data, renderer assets, or hexagonal coordinates. A consumer can validate and inspect the fixture without loading the native library.

The machine-readable structural definition is schemas/wang-solution-v1.schema.json. The dependency-free semantic validator 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:

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:

The inclusive width and height are:

width  = max_x_inclusive - min_x_inclusive + 1
height = max_y_inclusive - min_y_inclusive + 1

Both dense arrays therefore have width * height entries. Array index i maps to local (i % width, i // width) and absolute coordinates (min_x_inclusive + i % width, min_y_inclusive + i // width). Coordinate offsets do not change adjacency.

tile_table[i].tile_id must equal i, so IDs are unique, consecutive, and canonical. Every active cells entry indexes that table. Edge order is always (N,E,S,W) even though JSON stores the four names explicitly.

An active boundary entry always has all four direction names. A null color means no boundary constraint. Constraints are legal only on an exposed side: the neighboring coordinate lies outside the inclusive bounds or is a hole. The color must equal the selected tile edge. Boundary constraints do not replace ordinary east/west and south/north matching between active cells.

Structural and semantic guarantees

The JSON Schema establishes only properties local to one JSON value:

• exact top-level and nested member names;
• literal schema, status, and geometry values;
• object and array shapes;
• integer, null, and nonnegative-color types;
• the presence of all four named directions;
• an object, but no correctness meaning, for metadata.

JSON Schema alone does not establish relationships between separate fields. The standard-library validator first mirrors the structural checks and then establishes the cross-field semantics:

• inclusive minima do not exceed inclusive maxima;
• both dense arrays have exactly the bounds area;
• tile IDs equal their canonical positions and all cell references exist;
• holes and active cells have the corresponding boundary representation;
• constraints occur only on exposed edges and match selected tile colors;
• every active horizontal and vertical adjacency has equal colors.

Passing only the structural schema is not a correctness claim. validate_wang_solution() is transport and contract validation: it establishes the internal consistency of the serialized witness, but it is neither a solver nor the independent application verifier. The integration boundary must run the independent verifier before presenting a solution as correct.

The renderer remains a presentation-only consumer. Its explicit hex mode uses the same square document through the in-memory square-to-hex port; it does not extend this schema. Neither raster mode may import this formats module, replace the independent verifier, or decide correctness from a successful render. load_wang_solution() additionally rejects malformed JSON, duplicate object members, and non-finite numeric extensions accepted by some JSON parsers.

Metadata boundary

metadata may carry producer names, display labels, timestamps, or similar 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. 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

V1 is closed: unknown structural fields are rejected. A breaking change to geometry, coordinate meaning, tile identity, dense ordering, boundary semantics, or correctness rules requires a new schema name and a separate validator. Non-semantic producer or presentation data belongs in metadata; 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. 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.