From bc96e8b5befcd1d06b836cd907c244651873a2d3 Mon Sep 17 00:00:00 2001 From: Manuel Magnabosco Date: Wed, 26 Aug 2026 01:03:29 +0200 Subject: [PATCH] Render square Wang solutions as hexagons --- README.md | 54 ++- docs/development_principles.md | 26 +- docs/historical_architecture.md | 9 +- docs/wang_solution_v1.md | 12 +- docs/wang_square_to_hex.md | 173 +++++++ renderer/README.md | 68 ++- renderer/UPSTREAM.md | 18 +- .../test_data/wang_solution_v1_hex_sat.png | Bin 0 -> 3019 bytes renderer/test_wang_hex.py | 350 ++++++++++++++ renderer/test_wang_square.py | 1 + renderer/wang_hex_port.py | 431 ++++++++++++++++++ renderer/wang_square.py | 265 ++++++++--- 12 files changed, 1290 insertions(+), 117 deletions(-) create mode 100644 docs/wang_square_to_hex.md create mode 100644 renderer/test_data/wang_solution_v1_hex_sat.png create mode 100644 renderer/test_wang_hex.py create mode 100644 renderer/wang_hex_port.py diff --git a/README.md b/README.md index b0dcaf4..54c9fdd 100644 --- a/README.md +++ b/README.md @@ -56,8 +56,9 @@ benchmark case. It does not require a GPU. ## Current status The implemented components cover the square pipeline from `.cm13` input -through a verified solution document and the separate diagnostic PNG command. -Hex translation and parallel solving remain future work. +through a verified solution document, the default square diagnostic PNG, and +the checked presentation-only square-to-hex view selected by `--hex`. Parallel +solving remains future work. | Capability | Status | | --- | --- | @@ -69,8 +70,8 @@ Hex translation and parallel solving remain future work. | Wang Z3 oracle | Implemented over copied `Region + TILESET` | | Boolean–Wang witness correspondence | Implemented; exhaustive evidence covers all 1,701 canonical formulas through three variables and 27,044 constrained native solves | | Verified square solution export | Implemented as the closed `wang-solution-v1` contract and deterministic exporter | -| Wang square diagnostic renderer | Implemented as a separate presentation-only CLI in the isolated `renderer/` project | -| Square-to-hex translation and verification | Not implemented; the two Python modules are empty placeholders | +| 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 | | 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 | @@ -108,13 +109,17 @@ The implemented paths are: copied tiling + Python checker | v - wang-solution-v1 --> square PNG + wang-solution-v1 --> square PNG (default) + \ + +--> pure hex port/check --> hex PNG (--hex) ``` The witness bridge relates exact Boolean assignments to the variable cells of the same live Yang–Zhang reduction. Its precise scope and evidence are recorded in the [witness correspondence design](docs/designs/2026-08-21-witness-extension-design.md). -The square-to-hex and OpenMP stages are not part of the implemented diagram. +The square-to-hex branch changes presentation only; it consumes the same +square witness after verification. OpenMP is not part of the implemented +diagram. ## Correctness boundaries @@ -130,6 +135,9 @@ The square-to-hex and OpenMP stages are not part of the implemented diagram. independent formula checker. - Witness correspondence does not claim a unique tiling for each assignment or that extending an extracted assignment reproduces the original tiling. +- The hex port is a bijection over the image tile table, not a second solver or + correctness oracle. Its pure checker proves translation equivalence while + leaving source solution validation upstream. - OpenMP is introduced only after the serial path is correct and measurable. - Project conventions must be distinguished from claims inherited from the Yang–Zhang paper. @@ -138,12 +146,10 @@ The square-to-hex and OpenMP stages are not part of the implemented diagram. Planned work remains separated into independently reviewed changes: -1. formalize, implement, and independently verify square-to-hex translation, - then add the explicit hex mode to the existing Wang renderer command; -2. evaluate MRV indexing on weakly constrained search and build a separate +1. evaluate MRV indexing on weakly constrained search and build a separate hard-UNSAT corpus before making parallelism claims; -3. harden allocation and cleanup failure paths before concurrent execution; -4. define and validate a minimal serial `TaskPlan` before implementing OpenMP. +2. harden allocation and cleanup failure paths before concurrent execution; +3. define and validate a minimal serial `TaskPlan` before implementing OpenMP. 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 @@ -166,7 +172,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 189-test combined suite independently: +`make check`. Run its 213-test combined suite independently: ```sh cd renderer @@ -177,7 +183,7 @@ CI mirrors that command in a separate read-only Python 3.14 job. Snapshot provenance and update instructions are recorded in [`renderer/UPSTREAM.md`](renderer/UPSTREAM.md). -To exercise the Wang square renderer on the versioned solution fixture: +To exercise the Wang renderer on the versioned square solution fixture: ```sh cd renderer @@ -186,8 +192,20 @@ uv run --locked python wang_square.py \ output/wang-square.png ``` +The same command produces the checked pointy-top axial presentation only when +the explicit flag is present: + +```sh +uv run --locked python wang_square.py \ + ../tests/fixtures/wang_solution_v1_square_sat.json \ + output/wang-hex.png \ + --hex +``` + The [square solution contract](docs/wang_solution_v1.md) includes the producer -API for exporting a verified native result before rendering it. +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. Useful individual targets: @@ -270,8 +288,8 @@ 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/ empty square-to-hex placeholders -renderer/ isolated legacy and Wang square PNG rendering +python/hex/ deliberately unused empty hex-core placeholders +renderer/ isolated legacy and square/default, hex/explicit Wang rendering tests/ C, Python, and instance regressions benchmarks/ fixed reference corpus and profiling runner docs/ theory and architecture references @@ -294,8 +312,8 @@ The [GitHub Pages documentation](https://xtraid.github.io/tiling-foundry/) organizes the technical material by reader interest: - **Architecture and correctness** covers module ownership, the serial solver, - independent verification, Boolean–Wang witness correspondence, and the - square solution data contract. + independent verification, Boolean–Wang witness correspondence, the square + solution data contract, and the presentation-only square-to-hex proof. - **Yang–Zhang reduction** covers geometry, formula-to-region construction, proof obligations, and primary references. - **Solver optimization** separates the current methodology from dated, diff --git a/docs/development_principles.md b/docs/development_principles.md index 6d6c057..f19821c 100644 --- a/docs/development_principles.md +++ b/docs/development_principles.md @@ -96,7 +96,8 @@ A module is implemented when it has: | `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 | -| `renderer/wang_square.py` | Structural presentation projection and square rasterization | Semantic verification and solver access | +| `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 | `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; @@ -124,7 +125,12 @@ models. No ctypes pointer reaches those models or their consumers. immutable Python models generic native solver / \ v v - Python oracles checkers / exporter --> square renderer + Python oracles checkers / exporter --> Wang renderer + | \ + | +--> pure hex port/check + v | + square PNG v + hex PNG ``` The formula adapter uses `cm13_formula_load_path(...)`, the path-based external @@ -201,7 +207,15 @@ produces the closed square-only `wang-solution-v1` document. The [data contract]({{ '/wang-solution-v1/' | relative_url }}) is authoritative for schema, semantic validation, deterministic serialization, and metadata rules. -The isolated square renderer consumes only that document. It projects the -fields needed to choose pixels and produces a diagnostic PNG. Rendering is -presentation, not proof, and cannot replace either semantic validation or the -independent verifier. Hex translation and hex rendering are not implemented. +The isolated Wang renderer consumes only that document. Its default path +projects the fields needed for the existing square diagnostic PNG. Explicit +`--hex` mode applies the pure in-memory +[square-to-hex port]({{ '/wang-square-to-hex/' | relative_url }}), runs its +raster-independent checker, and then composes a pointy-top axial PNG. The port +preserves the square table, selected IDs, coordinates, holes, boundary, and +matching truth values; it does not create a hex schema or core model. + +Rendering is presentation, not proof. The port checker establishes translation +equivalence but deliberately does not require the source matching relations to +be true, so neither raster path can replace semantic validation or the +independent verifier. diff --git a/docs/historical_architecture.md b/docs/historical_architecture.md index 5d506a9..897f42a 100644 --- a/docs/historical_architecture.md +++ b/docs/historical_architecture.md @@ -31,13 +31,14 @@ than the early `vars`/`clause` sketch. The current public headers and tests are authoritative for behavior. The serial and optimized solvers are implemented and measured. The Python -square solution contract, exporter, and presentation-only square renderer are -also implemented. Native C JSON remains a placeholder, while `TaskPlan`, the -native OpenMP solver, and square-to-hex translation remain future work. +square solution contract, exporter, presentation-only square renderer, and +checked square-to-hex presentation port are also implemented. Native C JSON, +`TaskPlan`, and the native OpenMP solver remain future work. Current boundaries and status are documented in the [architecture page]({{ '/development_principles/' | relative_url }}), the -[solution contract]({{ '/wang-solution-v1/' | relative_url }}), and the +[solution contract]({{ '/wang-solution-v1/' | relative_url }}), the +[square-to-hex reference]({{ '/wang-square-to-hex/' | relative_url }}), and the [solver optimization methodology]({{ '/solver_performance_scope/' | relative_url }}). ## Document metadata diff --git a/docs/wang_solution_v1.md b/docs/wang_solution_v1.md index 0e68678..b185fdc 100644 --- a/docs/wang_solution_v1.md +++ b/docs/wang_solution_v1.md @@ -134,11 +134,13 @@ 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. It must not 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. +The renderer remains a presentation-only consumer. Its explicit hex mode uses +the same square document through the in-memory +[square-to-hex port]({{ '/wang-square-to-hex/' | relative_url }}); 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 diff --git a/docs/wang_square_to_hex.md b/docs/wang_square_to_hex.md new file mode 100644 index 0000000..e9e80d9 --- /dev/null +++ b/docs/wang_square_to_hex.md @@ -0,0 +1,173 @@ +--- +layout: page +title: Square-to-hex presentation port +permalink: /wang-square-to-hex/ +description: Algebra, coordinate convention, inverse proof, and raster boundary for the verified presentation-only square-to-hex port. +section: Architecture and correctness +document_kind: Technical reference +status: Current specification +updated: 2026-08-26 +nav_order: 32 +--- + +# Square-to-hex presentation port + +## Scope and attribution + +This port turns an already selected square Wang presentation into a pointy-top +hexagonal presentation. It is not a solver, a second solution format, or a new +core geometry. The input remains the square-only +[Wang solution v1 contract]({{ '/wang-solution-v1/' | relative_url }}), and the +hexagonal value exists only in renderer memory. + +Section 4 and Figure 13 of Sky Basire's 2022 report describe the construction +principle: transfer the four square edge colors and give the two additional +hexagon sides one common color. The report is available through its +[institutional record](https://ir.canterbury.ac.nz/items/0f6603bb-28d2-4012-a1ec-06e0248d1c92), +[DOI](https://doi.org/10.26021/14719), and +[PDF](https://ir.canterbury.ac.nz/bitstreams/c69151f2-cf3b-4158-9f6b-b4e80013e440/download). +Basire cites Karel Culik II's +[*Small Aperiodic Sets of Triangular and Hexagonal Tiles*](https://link.springer.com/chapter/10.1007/978-3-642-60207-8_27) +for the underlying square-tile simulation result. + +The exact edge tuple, coordinate convention, deterministic fresh-color rule, +and finite-region bijection below are Tiling Foundry's formalization of that +construction. They are not attributed to either source's diagram notation. + +## Project convention + +The source stores square edges as `(N,E,S,W)`. Its dense row-major coordinates +increase to the east with `x` and to the south with `y`. The port uses +pointy-top axial coordinates + +```text +(q,r) = (x,y) +``` + +and stores hex edges clockwise as `(E,SE,SW,W,NW,NE)`. The corresponding axial +neighbors are: + +| Hex side | Neighbor | Square relation | +| --- | --- | --- | +| `E` | `(q+1,r)` | `(x+1,y)`, square `E` | +| `SE` | `(q,r+1)` | `(x,y+1)`, square `S` | +| `SW` | `(q-1,r+1)` | additional axis | +| `W` | `(q-1,r)` | `(x-1,y)`, square `W` | +| `NW` | `(q,r-1)` | `(x,y-1)`, square `N` | +| `NE` | `(q+1,r-1)` | additional axis | + +Let `C` be the finite set of all colors in the square tile table. The table is +nonempty, so the renderer chooses the deterministic fresh color + +```text +kappa = max(C) + 1. +``` + +Nonnegative integer colors are unbounded in the v1 contract. Therefore +`kappa` is defined and is not in `C`. Each square tile maps as + +```text +H(N,E,S,W) = (E,S,kappa,W,N,kappa) + E SE SW W NW NE +``` + +Tile-table order is unchanged, so `tile_id` remains the positional index. The +boundary tuple maps independently as + +```text +B(N,E,S,W) = (E,S,null,W,N,null). +``` + +A null boundary entry for a hole remains null. No constraint is invented on +the added axis; its tile edges are still both `kappa`. + +## Equivalence and inverse + +The map has a left inverse on its image: + +```text +P(E,SE,SW,W,NW,NE) = (NW,E,SE,W). +``` + +For every square tile `t`, `P(H(t)) = t`. Thus `H` is injective, preserves the +tile-table cardinality, and introduces no tile choice. + +Consider two active source positions. At `(x,y)` and `(x+1,y)`, square +east/west matching is + +```text +t(x,y).E = t(x+1,y).W. +``` + +Those positions become axial east/west neighbors, and `H` puts the same two +colors on hex `E` and `W`. At `(x,y)` and `(x,y+1)`, square south/north +matching becomes hex `SE/NW` matching for the same reason. Every active pair +on the third axial direction compares `kappa` with `kappa`, so that axis adds a +tautology and cannot remove a square witness. + +Conversely, take a valid hex tiling whose tile table is exactly the image of +`H`. Project every tile with `P`. Hex `E/W` matching gives square `E/W` +matching; hex `SE/NW` matching gives square `S/N` matching; the remaining axis +contains no projected information. This recovers one and only one square +tiling. + +The pointwise maps preserve inclusive coordinates, dense row-major indices, +active cells, holes, boundary values, and selected tile IDs. They therefore +form a bijection between square witnesses and witnesses over the image table +on the corresponding axial region. Existence and nonexistence are preserved, +as is the number of witnesses. The serialized v1 format is SAT-only, so an +UNSAT result has no document or renderer invocation; UNSAT preservation is a +property of the reduction, not a claimed JSON feature. + +## Independent port checker + +`renderer/wang_hex_port.py` contains the pure reducer and checker. It imports +only the Python standard library. The checker does not call the reducer and +does not use pixel coordinates. Before hex rasterization it checks: + +- exact coordinate, table, assignment, hole, and boundary preservation; +- all six edges of every mapped tile and freshness of `kappa`; +- the inverse projection for every positional tile ID; +- equality of square and hex matching truth values on both meaningful axes; +- `kappa/kappa` matching on every active pair along the additional axis; +- equality of boundary-matching truth values after direction mapping. + +The truth-value comparison is deliberate. If a structurally present input has +an invalid square adjacency, the corresponding hex adjacency remains invalid; +the checker establishes translation equivalence without turning the renderer +into another solution validator. Contract validation and the independent +tiling verifier remain upstream obligations. + +## Raster boundary + +The existing `renderer/wang_square.py` command remains the only Wang renderer +command. Without a geometry flag it follows the unchanged square path. With +`--hex`, it reduces and checks the same in-memory presentation before composing +hex pixels: + +```sh +uv run --locked python wang_square.py \ + ../tests/fixtures/wang_solution_v1_square_sat.json \ + output/wang-hex.png \ + --hex +``` + +For hex mode, `--pixels-per-cell s` is the integer axial raster radius. Centers +use + +```text +pixel_x = 2*s*q + s*r +pixel_y = (s + floor(s/2))*r. +``` + +Integer vertices and a normalized bounding box make negative coordinates and +pixel placement deterministic. The same injective palette is extended with +`kappa`; because `kappa` is greater than every square color, existing logical +colors retain their square RGB assignments. Holes use the neutral checkerboard +inside the same pointy-top mask. The committed fixture golden is RGB 337×177 +at the default radius and margin. + +The raster consumes the checked result but proves nothing about SAT, +adjacency, boundary validity, or solver behavior. It loads no native library or +Z3 module, writes no intermediate hex serialization, and leaves the root +`python/hex/` placeholders untouched. diff --git a/renderer/README.md b/renderer/README.md index 0d5e059..97b2978 100644 --- a/renderer/README.md +++ b/renderer/README.md @@ -6,9 +6,10 @@ A command-line pixel art renderer that composites a scene from a tile-based back **Status**: feature-complete. The code works and is tested; any future changes will be refactoring, cleanup, or optimization. -Tiling Foundry also supplies a separate presentation-only Wang square backend. -It consumes the versioned JSON boundary without importing the solver or -changing this legacy pixel-art pipeline. +Tiling Foundry also supplies a separate presentation-only Wang backend. Its +default square path and explicit checked `--hex` view consume the same +versioned square JSON without importing the solver or changing this legacy +pixel-art pipeline. ## Output @@ -37,9 +38,10 @@ python main.py 255 (invalid) @@ -225,8 +250,9 @@ Raises `RenderingException` on pipeline errors. uv run --locked pytest -q ``` -The complete isolated suite has 189 tests: the 144 preserved legacy tests -below and 45 Wang square tests. To run only the original upstream suite: +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: ```bash uv run --locked pytest tests.py -v diff --git a/renderer/UPSTREAM.md b/renderer/UPSTREAM.md index bd150d4..ebacbd5 100644 --- a/renderer/UPSTREAM.md +++ b/renderer/UPSTREAM.md @@ -21,12 +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`, `test_wang_square.py`, and the -decoded-pixel golden `test_data/wang_solution_v1_square_sat.png`, 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 also leave `pyproject.toml`, `uv.lock`, and the pinned -dependencies unchanged. +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 +also leave `pyproject.toml`, `uv.lock`, and the pinned dependencies unchanged. ## Verification @@ -43,9 +42,10 @@ uv run --locked pytest -q ``` The import baseline remains 144 collected tests and 144 passing tests. The -combined local suite is 189 tests: 144 preserved legacy tests and 45 Wang -square tests. Keep the renderer environment under `renderer/.venv`; its local -`.gitignore` excludes that environment and generated Python/build files. +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 +generated Python/build files. The preserved `renderer/.github/workflows/ci.yml` is nested upstream evidence; GitHub does not run it as a workflow of the containing repository. The diff --git a/renderer/test_data/wang_solution_v1_hex_sat.png b/renderer/test_data/wang_solution_v1_hex_sat.png new file mode 100644 index 0000000000000000000000000000000000000000..749f4903d5155235ec4a25a1af0fb5857b5c83f6 GIT binary patch literal 3019 zcmYk8dsGwG7RIq%KB>ieRc@s=ZI#ki0Yw4BYwD{?k>G>JH3CtnAPNLx0nw1CsH}=K zN`Qb#$f}A_C{Q4PK}=c|F%2P@h$vAa5E5Q7z+jRglbJgS*Sq@9tnZxt?X&lpwSMQE zU-l4oE?%^9k%NQ7;^1A|_c=Js*^BAA1s`DFDYs8oJ2*HN25;XIezI53y?^YWYQ+!D z+?czIZlK7v#fLfvJ2p{ z9sL12_HGW_`+itF1P>ot_jR01+8y04Vo(RjV#^$}1cvF@EXHA7TcDMk-)c-$`Za@EJI z=ZDqh23$-8ipKc_V{3+y`ASui7=2ysI1F^Q?^>IUO*+*D3TI+(jtP81>WR`b zVyiB*`65}YWlZ2n_t7JIU0^DkncT3^R;_uFq3V_C1FYNlo69$0ZRJ#Jn78+SMW;|HCFn3QworNoDAvbzL>cG@I$eURvaqW6K#hKa6dj8~?YFNWtfAJw z1b(ipIcVEZMi+VHVv*{jBd^eUj&J#MrsT+<)^X%D#<$seqWk*;Dy z=+rHj4e1^!aL>JltZoah3JNuKn0rX*@|-9#$=Y#-)coqfc_gGpACpW10;95lS{9iy z5al^jt83juS)6nSj1RIh^sSQ`;;o8K1~d&cf%BMSS4;c=trC5K^_zN#I0~1Bq4EB_ z^?1hn1gb{!LB)|0`q*#e{q6lOv7}D8Xqb9l^VQ9YPI(XyY0nJWL%FKlr)#Iq;8fWR ziR=y*oo1@+xvKF6#z{z|xlS?K@X%sA?BA_XFb&xw-atCC^`&+{dRIy-u4Zo9gOFs=1 zfDe^FvN?W0lM+4IX$f6RqdYe|3TZ)X=vyh2medwZ;PP_(tqdKNBY5D-?_^*}<=~`p z>i zc*Iasq{50@b$RFf!E>CbP3nq_%@#fFHPE8)LO0NsgIv8ctLJUch(25jS6k(BIMO7k zBO^p&mFr=e3r(u6eJLU?)dDY3PKP0lypFB)y@^Gl5U}B2ZlyUY*ABxoG@!#k1p@rF z&AX+)L)*;mrG^!&!g@ssqSN<(M!RK(Y^M%^*0f7n1c}W1%M8itfLmSl9v-#IYlaH6 zMeEdJNTGuBZxz3Sm%tljxTB{j;C&P6Da;+3VzB^CUp9ZR&J$=ID~jabrnRCkkT$1{ z{7$h@Va)i9MhSS?a@jOx!im^LZ_&6QDILHi@(k%J&QClX6L=IPZr2%WmQSCc36QFB zFc45asD(aJEILN}jz-d+j+VF`(7TO@bHLny_Jq3-Mr*2QF7l;zXVdF@ki&)?fQ2chIME$MwFxkTqrGhMn(997K`l8R8O@&hVRT@s#ab4SU?I!k zUGm$>KI%h6ZbwuY9JBY^w6pv$N`iE=z-- zjSaCm=I(rC4DVSKz0JlcDI7gs2o~G$bylF)G_alOmnQMo!X-9#X^*Y7!5+~zEAI$q zb>x;DK(>~XYl8q+KirqX1(>NpF299l^hAAW58+-;WS>A|x zCuN7(a>2LsP~zvz{knGJQp{SyvRUtQFst`^o7J-#{g#Wu`ZnZg@c<{sI^DWb3Szh= z2c3%@p2>cP@GF1nk$Y+z+NhcItW)%?%H=OilMR)XuLO6%uwUJngTJgmp_dXmVvU+N zOXtF8VXaLV&=C>BtW-MNngfrg87*l>m9@nuvjrwtWI3WODyKxTQ(^?cn)T4I{hJ{W zy9|$Ghub4fV}F(wyE#C|FQ_n*AL9JgMwj013X+VK|KWof1VO$CC%xzifxN-sQJ8I^lG^*Z`f2f5H4E}Gbu4I> zo9?C%>gB&kaB+=>bai30$AY#^K!!%*3TwjNA*|>4_c_4^2&a0zE}Q`)n$Zd)N(46NEG<0cMO zPts6zP3Bt~$(QWM(4*$s7BOn2pH&?vIcdf4M9tVIMaJ%t|AbhGft71y22uYB>}Y=i z%e0BZa4xjPx8tnW!O)Ls=53`s9jJ>L>07MTSMequ0#^V~4$6A(&9dfV?l-lOu7g`8 z-Z$q0aBQ;Ylk7oB<8DWqd46v!$98XCTLDivX*{21ua>+E!RGTo=TYhd%{+n&HV-@Q z@WD)3 zE9*Df#iZg#f4fLhT$=TaC@;;1niPwC?V(KUe)|lbFb&q$#dzS&{kR9D_OQIQ=iT(vW zVqDmq#2n+=ez?waW+mG!S WangPresentation: + if boundary is None: + boundary = tuple( + None if tile_id is None else (None, None, None, None) + for tile_id in cells + ) + return WangPresentation( + min_x=min_x, + min_y=min_y, + max_x=min_x + width - 1, + max_y=min_y + height - 1, + tile_edges=(edges,), + cells=cells, + boundary=boundary, + ) + + +def _mutate_tile_edge( + presentation: WangHexPort, tile_id: int, direction: int, value: int +) -> WangHexPort: + table = list(presentation.tile_edges) + edges = list(table[tile_id]) + edges[direction] = value + table[tile_id] = tuple(edges) + return replace(presentation, tile_edges=tuple(table)) + + +def test_fixture_port_preserves_coordinates_table_cells_holes_and_boundary(): + square = load_wang_presentation(FIXTURE) + port = reduce_square_to_hex(square) + + assert (port.min_q, port.min_r, port.max_q, port.max_r) == (-1, 2, 2, 4) + assert port.fresh_color == 16 + assert len(port.tile_edges) == len(square.tile_edges) == 23 + assert port.tile_edges[0] == (2, 7, 16, 1, 0, 16) + assert port.cells is square.cells + assert port.cells.count(None) == 2 + assert port.boundary[0] == (None, None, None, 2, 0, None) + assert port.boundary[1] == (2, None, None, None, 0, None) + assert port.boundary[8] == (None, 0, None, 2, None, None) + assert port.boundary[2] is None + check_square_to_hex(square, port) + + +def test_fresh_color_occurs_only_on_opposite_sw_and_ne_edges(): + square = load_wang_presentation(FIXTURE) + port = reduce_square_to_hex(square) + + assert all(port.fresh_color not in edges for edges in square.tile_edges) + for square_edges, hex_edges in zip( + square.tile_edges, port.tile_edges, strict=True + ): + assert hex_edges[2] == hex_edges[5] == port.fresh_color + assert port.fresh_color not in (hex_edges[0], hex_edges[1], *hex_edges[3:5]) + assert (hex_edges[4], hex_edges[0], hex_edges[1], hex_edges[3]) == ( + square_edges + ) + + +@pytest.mark.parametrize("direction", range(6)) +def test_checker_rejects_a_mutation_on_each_hex_side(direction): + square = load_wang_presentation(FIXTURE) + port = reduce_square_to_hex(square) + broken = _mutate_tile_edge(port, 0, direction, 999) + + with pytest.raises(WangSquareRenderError, match="does not implement H"): + check_square_to_hex(square, broken) + + +@pytest.mark.parametrize( + ("mutation", "message"), + [ + (lambda port: replace(port, min_q=port.min_q - 1), "coordinates"), + (lambda port: replace(port, cells=(None, *port.cells[1:])), "assignment"), + (lambda port: replace(port, fresh_color=999), "fresh color"), + ( + lambda port: replace(port, boundary=port.boundary[:-1]), + "hex boundary", + ), + ], +) +def test_checker_rejects_changed_preserved_state(mutation, message): + square = load_wang_presentation(FIXTURE) + port = reduce_square_to_hex(square) + + with pytest.raises(WangSquareRenderError, match=message): + check_square_to_hex(square, mutation(port)) + + +def test_checker_rejects_added_constraint_on_fresh_boundary_axis(): + square = load_wang_presentation(FIXTURE) + port = reduce_square_to_hex(square) + boundary = list(port.boundary) + first = list(boundary[0]) + first[2] = port.fresh_color + boundary[0] = tuple(first) + + with pytest.raises(WangSquareRenderError, match="boundary mapping"): + check_square_to_hex( + square, replace(port, boundary=tuple(boundary)) + ) + + +def test_reducer_and_checker_reject_type_coercion_and_mutable_storage(): + square = load_wang_presentation(FIXTURE) + port = reduce_square_to_hex(square) + + with pytest.raises(WangSquareRenderError, match="square tile table.*tuple"): + reduce_square_to_hex( + replace(square, tile_edges=list(square.tile_edges)) + ) + + with pytest.raises(WangSquareRenderError, match="hex tile table.*tuple"): + check_square_to_hex( + square, replace(port, tile_edges=list(port.tile_edges)) + ) + + bool_edges = list(port.tile_edges[0]) + bool_edges[3] = True # Equal to the expected integer 1 without type checks. + bool_table = (tuple(bool_edges), *port.tile_edges[1:]) + with pytest.raises(WangSquareRenderError, match="invalid edge color"): + check_square_to_hex( + square, replace(port, tile_edges=bool_table) + ) + + with pytest.raises(WangSquareRenderError, match="fresh color.*integer"): + check_square_to_hex( + square, replace(port, fresh_color=float(port.fresh_color)) + ) + + +def test_port_checker_preserves_invalid_matching_truth_without_becoming_verifier(): + square = WangPresentation( + min_x=-2, + min_y=4, + max_x=-1, + max_y=4, + tile_edges=((0, 10, 0, 20),), + cells=(0, 0), + boundary=((999, None, None, None), (None, None, None, None)), + ) + port = reduce_square_to_hex(square) + + # The east/west colors and the north boundary are deliberately invalid. + # The checker establishes equivalence of those false relations, not SAT. + check_square_to_hex(square, port) + + +def test_pure_port_imports_no_raster_solver_or_native_modules(tmp_path): + script = f""" +import importlib.util +from pathlib import Path +import sys + +module_path = Path({str(RENDERER_DIR / 'wang_hex_port.py')!r}) +spec = importlib.util.spec_from_file_location('isolated_wang_hex_port', module_path) +module = importlib.util.module_from_spec(spec) +sys.modules[spec.name] = module +spec.loader.exec_module(module) +for forbidden in ('numpy', 'PIL', 'z3', 'formats', 'model', 'native', 'oracles'): + assert forbidden not in sys.modules, forbidden +""" + + completed = subprocess.run( + [sys.executable, "-B", "-c", script], + cwd=tmp_path, + text=True, + capture_output=True, + check=False, + ) + + assert completed.returncode == 0, completed.stderr + + +def test_hex_canvas_is_dynamic_rgb_and_translation_invariant(): + square = load_wang_presentation(FIXTURE) + translated = replace( + square, + min_x=19, + min_y=-11, + max_x=22, + max_y=-9, + ) + + first = wang_square._compose_wang_hex( + square, pixels_per_cell=8, margin=3 + ) + second = wang_square._compose_wang_hex( + translated, pixels_per_cell=8, margin=3 + ) + + assert first.shape == (47, 87, 3) + assert first.dtype == np.uint8 + assert np.array_equal(first, second) + assert tuple(first[0, 0]) == BACKGROUND_RGB + + +def test_hex_raster_places_eswwnwne_edge_colors_in_pointy_top_wedges(): + square = _presentation() + port = reduce_square_to_hex(square) + palette = wang_square._build_palette_from_edges(port.tile_edges) + canvas = wang_square._compose_wang_hex( + square, pixels_per_cell=8, margin=0 + ) + + assert tuple(canvas[8, 14]) == palette[20] # E + assert tuple(canvas[12, 11]) == palette[30] # SE + assert tuple(canvas[12, 5]) == palette[port.fresh_color] # SW + assert tuple(canvas[8, 2]) == palette[40] # W + assert tuple(canvas[4, 5]) == palette[10] # NW + assert tuple(canvas[4, 11]) == palette[port.fresh_color] # NE + assert tuple(canvas[8, 16]) == GRID_RGB + + +def test_hex_hole_uses_neutral_checkerboard_not_logical_palette(): + square = _presentation(cells=(None, 0), width=2) + canvas = wang_square._compose_wang_hex( + square, pixels_per_cell=8, margin=0 + ) + hole_pixels = {tuple(pixel) for row in canvas[:, :16] for pixel in row} + + assert HOLE_LIGHT_RGB in hole_pixels + assert HOLE_DARK_RGB in hole_pixels + assert not hole_pixels & set(build_palette(square).values()) + + +def test_hex_rejects_oversized_canvas_before_allocation(): + square = _presentation( + cells=(0,) * 33, + width=33, + boundary=((None, None, None, None),) * 33, + ) + + with pytest.raises(WangSquareRenderError, match="canvas side exceeds"): + wang_square._compose_wang_hex( + square, pixels_per_cell=512, margin=0 + ) + + +def test_default_mode_remains_byte_identical_and_skips_hex_port( + tmp_path, monkeypatch +): + output = tmp_path / "render.png" + + def fail_port(_presentation): + raise AssertionError("default mode entered hex port") + + monkeypatch.setattr(wang_square, "reduce_square_to_hex", fail_port) + render_wang_square(FIXTURE, output) + + assert output.read_bytes() == SQUARE_GOLDEN.read_bytes() + + +def test_hex_checker_failure_preserves_existing_output(tmp_path, monkeypatch): + output = tmp_path / "render.png" + output.write_bytes(b"previous output") + + def fail_check(_square, _candidate): + raise WangSquareRenderError("injected port rejection") + + monkeypatch.setattr(wang_square, "check_square_to_hex", fail_check) + with pytest.raises(WangSquareRenderError, match="port rejection"): + render_wang_square(FIXTURE, output, hex_mode=True) + + assert output.read_bytes() == b"previous output" + assert not list(tmp_path.glob(".render.png.*.png")) + + +def test_hex_fixture_render_matches_decoded_golden_pixels(tmp_path): + output = tmp_path / "render.png" + render_wang_square(FIXTURE, output, hex_mode=True) + + with Image.open(output) as actual, Image.open(HEX_GOLDEN) as expected: + actual.load() + expected.load() + assert actual.mode == expected.mode == "RGB" + assert actual.size == expected.size == (337, 177) + assert actual.tobytes() == expected.tobytes() + assert hashlib.sha256(actual.tobytes()).hexdigest() == ( + "c5d40ce2ec0c124c32da789a21231b336b4c8b6242bb2fd85a579f7257811f04" + ) + + +def test_cli_hex_flag_renders_same_square_witness_as_hexagons(tmp_path): + output = tmp_path / "render.png" + wang_square.main( + [ + str(FIXTURE), + str(output), + "--hex", + "--pixels-per-cell", + "8", + "--margin", + "0", + ] + ) + + with Image.open(output) as image: + assert image.mode == "RGB" + assert image.size == (81, 41) diff --git a/renderer/test_wang_square.py b/renderer/test_wang_square.py index 8bcac33..bc40573 100644 --- a/renderer/test_wang_square.py +++ b/renderer/test_wang_square.py @@ -427,6 +427,7 @@ def test_consumer_process_does_not_import_core_z3_or_load_libwang(tmp_path): import sys module_path = Path({str(RENDERER_DIR / 'wang_square.py')!r}) +sys.path.insert(0, str(module_path.parent)) spec = importlib.util.spec_from_file_location('isolated_wang_square', module_path) module = importlib.util.module_from_spec(spec) sys.modules[spec.name] = module diff --git a/renderer/wang_hex_port.py b/renderer/wang_hex_port.py new file mode 100644 index 0000000..42ec2b0 --- /dev/null +++ b/renderer/wang_hex_port.py @@ -0,0 +1,431 @@ +"""Pure square-to-hex presentation port for ``wang-solution-v1``. + +The source document remains square-only. This module changes neither the +solver domain nor the serialized contract: it maps the already selected tile +table, cells, coordinates, and boundary presentation into an in-memory +pointy-top axial view. It deliberately has no NumPy, Pillow, solver, or native +library dependency. +""" + +from __future__ import annotations + +from dataclasses import dataclass +from typing import Final + + +SQUARE_DIRECTIONS: Final = ("N", "E", "S", "W") +HEX_DIRECTIONS: Final = ("E", "SE", "SW", "W", "NW", "NE") + +_SQUARE_N: Final = 0 +_SQUARE_E: Final = 1 +_SQUARE_S: Final = 2 +_SQUARE_W: Final = 3 + +_HEX_E: Final = 0 +_HEX_SE: Final = 1 +_HEX_SW: Final = 2 +_HEX_W: Final = 3 +_HEX_NW: Final = 4 +_HEX_NE: Final = 5 + +SquareEdges = tuple[int, int, int, int] +HexEdges = tuple[int, int, int, int, int, int] +SquareBoundary = tuple[int | None, int | None, int | None, int | None] +HexBoundary = tuple[ + int | None, + int | None, + int | None, + int | None, + int | None, + int | None, +] + + +class WangSquareRenderError(ValueError): + """Raised when a Wang presentation cannot be rendered safely.""" + + +@dataclass(frozen=True, slots=True) +class WangPresentation: + """Immutable projection of the square fields relevant to presentation.""" + + min_x: int + min_y: int + max_x: int + max_y: int + tile_edges: tuple[SquareEdges, ...] + cells: tuple[int | None, ...] + boundary: tuple[SquareBoundary | 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 WangHexPort: + """In-memory hex view derived one-to-one from a square presentation.""" + + min_q: int + min_r: int + max_q: int + max_r: int + tile_edges: tuple[HexEdges, ...] + cells: tuple[int | None, ...] + boundary: tuple[HexBoundary | None, ...] + fresh_color: int + + @property + def width(self) -> int: + return self.max_q - self.min_q + 1 + + @property + def height(self) -> int: + return self.max_r - self.min_r + 1 + + +def _port_fail(message: str) -> None: + raise WangSquareRenderError(f"square-to-hex port: {message}") + + +def _check_square_storage(presentation: WangPresentation) -> None: + for name, value in ( + ("min_x", presentation.min_x), + ("min_y", presentation.min_y), + ("max_x", presentation.max_x), + ("max_y", presentation.max_y), + ): + if type(value) is not int: + _port_fail(f"square {name} must be an integer") + if presentation.max_x < presentation.min_x: + _port_fail("square max_x must be at least min_x") + if presentation.max_y < presentation.min_y: + _port_fail("square max_y must be at least min_y") + if type(presentation.tile_edges) is not tuple: + _port_fail("square tile table must be an immutable tuple") + if not presentation.tile_edges: + _port_fail("square tile table must not be empty") + for tile_id, edges in enumerate(presentation.tile_edges): + if type(edges) is not tuple or len(edges) != len(SQUARE_DIRECTIONS): + _port_fail(f"square tile {tile_id} must have four immutable edges") + if any(type(color) is not int or color < 0 for color in edges): + _port_fail(f"square tile {tile_id} has an invalid edge color") + + if type(presentation.cells) is not tuple: + _port_fail("square cells must be an immutable tuple") + if type(presentation.boundary) is not tuple: + _port_fail("square boundary must be an immutable tuple") + area = presentation.width * presentation.height + if len(presentation.cells) != area: + _port_fail("square cells must match the inclusive bounds area") + if len(presentation.boundary) != area: + _port_fail("square boundary must match the inclusive bounds area") + for index, tile_id in enumerate(presentation.cells): + if tile_id is not None and ( + type(tile_id) is not int + or tile_id < 0 + or tile_id >= len(presentation.tile_edges) + ): + _port_fail(f"square cell {index} has an invalid tile ID") + for index, sides in enumerate(presentation.boundary): + if sides is None: + continue + if type(sides) is not tuple or len(sides) != len(SQUARE_DIRECTIONS): + _port_fail(f"square boundary entry {index} must have four sides") + if any( + color is not None and (type(color) is not int or color < 0) + for color in sides + ): + _port_fail(f"square boundary entry {index} has an invalid color") + + +def _check_hex_bounds(presentation: WangHexPort) -> None: + for name, value in ( + ("min_q", presentation.min_q), + ("min_r", presentation.min_r), + ("max_q", presentation.max_q), + ("max_r", presentation.max_r), + ): + if type(value) is not int: + _port_fail(f"hex {name} must be an integer") + if presentation.max_q < presentation.min_q: + _port_fail("hex max_q must be at least min_q") + if presentation.max_r < presentation.min_r: + _port_fail("hex max_r must be at least min_r") + + +def _check_hex_storage(presentation: WangHexPort) -> None: + if type(presentation.tile_edges) is not tuple: + _port_fail("hex tile table must be an immutable tuple") + if not presentation.tile_edges: + _port_fail("hex tile table must not be empty") + for tile_id, edges in enumerate(presentation.tile_edges): + if type(edges) is not tuple or len(edges) != len(HEX_DIRECTIONS): + _port_fail(f"hex tile {tile_id} must have six immutable edges") + if any(type(color) is not int or color < 0 for color in edges): + _port_fail(f"hex tile {tile_id} has an invalid edge color") + + if type(presentation.cells) is not tuple: + _port_fail("hex cells must be an immutable tuple") + if type(presentation.boundary) is not tuple: + _port_fail("hex boundary must be an immutable tuple") + area = presentation.width * presentation.height + if len(presentation.cells) != area: + _port_fail("hex cells must match the inclusive bounds area") + if len(presentation.boundary) != area: + _port_fail("hex boundary must match the inclusive bounds area") + for index, tile_id in enumerate(presentation.cells): + if tile_id is not None and ( + type(tile_id) is not int + or tile_id < 0 + or tile_id >= len(presentation.tile_edges) + ): + _port_fail(f"hex cell {index} has an invalid tile ID") + for index, sides in enumerate(presentation.boundary): + if sides is None: + continue + if type(sides) is not tuple or len(sides) != len(HEX_DIRECTIONS): + _port_fail(f"hex boundary entry {index} must have six sides") + if any( + color is not None and (type(color) is not int or color < 0) + for color in sides + ): + _port_fail(f"hex boundary entry {index} has an invalid color") + if ( + type(presentation.fresh_color) is not int + or presentation.fresh_color < 0 + ): + _port_fail("hex fresh color must be a nonnegative integer") + + +def _fresh_color(presentation: WangPresentation) -> int: + return max( + color + for edges in presentation.tile_edges + for color in edges + ) + 1 + + +def reduce_square_to_hex(presentation: WangPresentation) -> WangHexPort: + """Map one square presentation to a pointy-top axial hex view. + + Axial coordinates are ``(q, r) = (x, y)``. Hex edges are stored as + ``(E, SE, SW, W, NW, NE)`` and each square ``(N, E, S, W)`` tile becomes + ``(E, S, kappa, W, N, kappa)``. + """ + if not isinstance(presentation, WangPresentation): + raise TypeError("presentation must be a WangPresentation") + _check_square_storage(presentation) + kappa = _fresh_color(presentation) + + hex_tiles = tuple( + ( + edges[_SQUARE_E], + edges[_SQUARE_S], + kappa, + edges[_SQUARE_W], + edges[_SQUARE_N], + kappa, + ) + for edges in presentation.tile_edges + ) + hex_boundary: list[HexBoundary | None] = [] + for sides in presentation.boundary: + if sides is None: + hex_boundary.append(None) + continue + hex_boundary.append( + ( + sides[_SQUARE_E], + sides[_SQUARE_S], + None, + sides[_SQUARE_W], + sides[_SQUARE_N], + None, + ) + ) + + return WangHexPort( + min_q=presentation.min_x, + min_r=presentation.min_y, + max_q=presentation.max_x, + max_r=presentation.max_y, + tile_edges=hex_tiles, + cells=presentation.cells, + boundary=tuple(hex_boundary), + fresh_color=kappa, + ) + + +def _check_matching_equivalence( + square: WangPresentation, + candidate: WangHexPort, +) -> None: + """Check that matching truth values survive the port without judging them.""" + width = square.width + for index, tile_id in enumerate(square.cells): + if tile_id is None: + continue + square_edges = square.tile_edges[tile_id] + hex_edges = candidate.tile_edges[tile_id] + local_x = index % width + local_y = index // width + + if local_x + 1 < width: + east_id = square.cells[index + 1] + if east_id is not None: + square_match = ( + square_edges[_SQUARE_E] + == square.tile_edges[east_id][_SQUARE_W] + ) + hex_match = ( + hex_edges[_HEX_E] + == candidate.tile_edges[east_id][_HEX_W] + ) + if square_match != hex_match: + _port_fail(f"east/west matching changed at cell {index}") + + if local_y + 1 < square.height: + southeast_id = square.cells[index + width] + if southeast_id is not None: + square_match = ( + square_edges[_SQUARE_S] + == square.tile_edges[southeast_id][_SQUARE_N] + ) + hex_match = ( + hex_edges[_HEX_SE] + == candidate.tile_edges[southeast_id][_HEX_NW] + ) + if square_match != hex_match: + _port_fail(f"south/north matching changed at cell {index}") + + if local_x > 0 and local_y + 1 < square.height: + southwest_id = square.cells[index + width - 1] + if southwest_id is not None and ( + hex_edges[_HEX_SW] + != candidate.tile_edges[southwest_id][_HEX_NE] + ): + _port_fail(f"fresh-axis matching failed at cell {index}") + + +def _check_boundary_equivalence( + square: WangPresentation, + candidate: WangHexPort, +) -> None: + for index, (tile_id, square_sides, hex_sides) in enumerate( + zip(square.cells, square.boundary, candidate.boundary, strict=True) + ): + if square_sides is None: + if hex_sides is not None: + _port_fail(f"boundary null changed at cell {index}") + continue + if ( + type(hex_sides) is not tuple + or len(hex_sides) != len(HEX_DIRECTIONS) + ): + _port_fail(f"hex boundary entry {index} must have six sides") + expected = ( + square_sides[_SQUARE_E], + square_sides[_SQUARE_S], + None, + square_sides[_SQUARE_W], + square_sides[_SQUARE_N], + None, + ) + if hex_sides != expected: + _port_fail(f"boundary mapping changed at cell {index}") + + # Compare truth values instead of requiring a semantically valid input. + # Rendering therefore checks the port but does not become a verifier. + if tile_id is None: + continue + square_edges = square.tile_edges[tile_id] + hex_edges = candidate.tile_edges[tile_id] + for square_direction, hex_direction in ( + (_SQUARE_N, _HEX_NW), + (_SQUARE_E, _HEX_E), + (_SQUARE_S, _HEX_SE), + (_SQUARE_W, _HEX_W), + ): + required = square_sides[square_direction] + if required is None: + continue + if ( + square_edges[square_direction] == required + ) != (hex_edges[hex_direction] == hex_sides[hex_direction]): + _port_fail(f"boundary matching changed at cell {index}") + + +def check_square_to_hex( + square: WangPresentation, + candidate: WangHexPort, +) -> None: + """Independently check a port without using any raster geometry. + + The checker establishes exact field preservation, the six-edge mapping, + inverse projection, boundary mapping, and matching equivalence. It does + not require the source matching relations to be true and is therefore not + a substitute for solution validation or the independent tiling verifier. + """ + if not isinstance(square, WangPresentation): + raise TypeError("square must be a WangPresentation") + if not isinstance(candidate, WangHexPort): + raise TypeError("candidate must be a WangHexPort") + _check_square_storage(square) + _check_hex_bounds(candidate) + + expected_bounds = ( + square.min_x, + square.min_y, + square.max_x, + square.max_y, + ) + actual_bounds = ( + candidate.min_q, + candidate.min_r, + candidate.max_q, + candidate.max_r, + ) + if actual_bounds != expected_bounds: + _port_fail("axial coordinates do not preserve square coordinates") + _check_hex_storage(candidate) + if candidate.cells != square.cells: + _port_fail("cell assignment or holes changed") + if len(candidate.boundary) != len(square.boundary): + _port_fail("boundary cardinality changed") + if len(candidate.tile_edges) != len(square.tile_edges): + _port_fail("tile-table cardinality changed") + + kappa = _fresh_color(square) + if candidate.fresh_color != kappa: + _port_fail("fresh color is not max(C) + 1") + if any(kappa in edges for edges in square.tile_edges): + _port_fail("fresh color occurs in the square color set") + + for tile_id, (square_edges, hex_edges) in enumerate( + zip(square.tile_edges, candidate.tile_edges, strict=True) + ): + if ( + hex_edges[_HEX_E] != square_edges[_SQUARE_E] + or hex_edges[_HEX_SE] != square_edges[_SQUARE_S] + or hex_edges[_HEX_SW] != kappa + or hex_edges[_HEX_W] != square_edges[_SQUARE_W] + or hex_edges[_HEX_NW] != square_edges[_SQUARE_N] + or hex_edges[_HEX_NE] != kappa + ): + _port_fail(f"hex tile {tile_id} does not implement H") + projected = ( + hex_edges[_HEX_NW], + hex_edges[_HEX_E], + hex_edges[_HEX_SE], + hex_edges[_HEX_W], + ) + if projected != square_edges: + _port_fail(f"inverse projection failed for tile {tile_id}") + + _check_boundary_equivalence(square, candidate) + _check_matching_equivalence(square, candidate) diff --git a/renderer/wang_square.py b/renderer/wang_square.py index ce7bf9e..7016620 100644 --- a/renderer/wang_square.py +++ b/renderer/wang_square.py @@ -2,14 +2,14 @@ This module deliberately does not verify Wang adjacency or boundary semantics. It accepts the structural fields needed for presentation, projects away -``boundary`` and ``metadata``, and renders the selected tile edge colors. -Successful rendering is not a correctness claim. +``metadata``, and renders the selected tile edge colors. The default square +path is unchanged; explicit hex mode applies and checks the pure Basire/Culik +port before rasterization. Successful rendering is not a correctness claim. """ from __future__ import annotations import argparse -from dataclasses import dataclass import json import os from pathlib import Path @@ -17,13 +17,22 @@ from typing import Final import numpy as np -from PIL import Image +from PIL import Image, ImageDraw + +from wang_hex_port import ( + SQUARE_DIRECTIONS, + WangHexPort, + WangPresentation, + WangSquareRenderError, + check_square_to_hex, + reduce_square_to_hex, +) SCHEMA_NAME: Final = "wang-solution-v1" GEOMETRY: Final = "square" STATUS: Final = "SAT" -DIRECTIONS: Final = ("N", "E", "S", "W") +DIRECTIONS: Final = SQUARE_DIRECTIONS DEFAULT_PIXELS_PER_CELL: Final = 32 DEFAULT_MARGIN: Final = 8 @@ -66,30 +75,6 @@ ) -class WangSquareRenderError(ValueError): - """Raised when an input cannot be presented as a v1 square image.""" - - -@dataclass(frozen=True, slots=True) -class WangPresentation: - """Immutable projection of only the fields that determine the pixels.""" - - min_x: int - min_y: int - max_x: int - max_y: int - tile_edges: tuple[tuple[int, int, int, int], ...] - cells: tuple[int | 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 - - def _fail(path: str, message: str) -> None: raise WangSquareRenderError(f"{path}: {message}") @@ -145,19 +130,22 @@ def _reject_nonfinite_constant(value: str) -> None: ) -def _validate_optional_edges(value: object, path: str) -> None: +def _validate_optional_edges( + value: object, path: str +) -> tuple[int | None, int | None, int | None, int | None] | None: if value is None: - return + return None edges = _require_object(value, path) _require_exact_fields(edges, frozenset(DIRECTIONS), path) + projected: list[int | None] = [] for direction in DIRECTIONS: color = edges[direction] if color is not None: - _require_integer( - color, - f"{path}.{direction}", - nonnegative=True, + color = _require_integer( + color, f"{path}.{direction}", nonnegative=True ) + projected.append(color) + return tuple(projected) def _project_wang_presentation(document: object) -> WangPresentation: @@ -248,13 +236,16 @@ def _project_wang_presentation(document: object) -> WangPresentation: _fail(f"$.cells[{index}]", f"references absent tile_id {tile_id}") cells.append(tile_id) - # Boundary data is checked only for v1 transport shape. It is not compared - # with cells or edges, and it never reaches the presentation projection. + # Boundary data is checked only for v1 transport shape. It is retained for + # the pure hex port, but is not compared with cells/edges or used by the + # square raster. boundary = _require_array(root["boundary"], "$.boundary") if len(boundary) != area: _fail("$.boundary", f"length must equal inclusive bounds area {area}") - for index, sides in enumerate(boundary): + projected_boundary = tuple( _validate_optional_edges(sides, f"$.boundary[{index}]") + for index, sides in enumerate(boundary) + ) _require_object(root["metadata"], "$.metadata") return WangPresentation( @@ -264,11 +255,12 @@ def _project_wang_presentation(document: object) -> WangPresentation: max_y=max_y, tile_edges=tuple(tile_edges), cells=tuple(cells), + boundary=projected_boundary, ) def load_wang_presentation(path: str | Path) -> WangPresentation: - """Load strict JSON and return only the fields that determine pixels.""" + """Load strict JSON and project metadata away from presentation data.""" source = Path(path) try: with source.open(encoding="utf-8") as stream: @@ -300,14 +292,11 @@ def load_wang_presentation(path: str | Path) -> WangPresentation: return _project_wang_presentation(document) -def build_palette( - presentation: WangPresentation, +def _build_palette_from_edges( + tile_edges: tuple[tuple[int, ...], ...], ) -> dict[int, tuple[int, int, int]]: - """Assign a deterministic, injective RGB color to each logical color.""" - if not isinstance(presentation, WangPresentation): - raise TypeError("presentation must be a WangPresentation") logical_colors = sorted( - {color for edges in presentation.tile_edges for color in edges} + {color for edges in tile_edges for color in edges} ) available = _RGB_SPACE_SIZE - len(_RESERVED_RGB) if len(logical_colors) > available: @@ -332,6 +321,15 @@ def build_palette( return palette +def build_palette( + presentation: WangPresentation, +) -> dict[int, tuple[int, int, int]]: + """Assign a deterministic, injective RGB color to each logical color.""" + if not isinstance(presentation, WangPresentation): + raise TypeError("presentation must be a WangPresentation") + return _build_palette_from_edges(presentation.tile_edges) + + def _render_integer( value: object, name: str, @@ -364,6 +362,11 @@ def _canvas_dimensions( ) width = presentation.width * ppc + 2 * checked_margin height = presentation.height * ppc + 2 * checked_margin + _check_canvas_limits(width, height) + return width, height, ppc, checked_margin + + +def _check_canvas_limits(width: int, height: int) -> None: if width > MAX_CANVAS_SIDE or height > MAX_CANVAS_SIDE: raise WangSquareRenderError( f"canvas side exceeds limit {MAX_CANVAS_SIDE}: {width}x{height}" @@ -372,7 +375,6 @@ def _canvas_dimensions( raise WangSquareRenderError( f"canvas area exceeds limit {MAX_CANVAS_PIXELS}: {width}x{height}" ) - return width, height, ppc, checked_margin def _tile_asset( @@ -447,6 +449,145 @@ def compose_wang_square( return canvas +def _hex_canvas_dimensions( + presentation: WangHexPort, + pixels_per_cell: object, + margin: object, +) -> tuple[int, int, int, int, int]: + 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 + ) + shoulder = radius // 2 + width = ( + 2 * radius * (presentation.width - 1) + + radius * (presentation.height - 1) + + 2 * radius + + 1 + + 2 * checked_margin + ) + height = ( + (radius + shoulder) * (presentation.height - 1) + + 2 * radius + + 1 + + 2 * checked_margin + ) + _check_canvas_limits(width, height) + return width, height, radius, shoulder, checked_margin + + +def _hex_vertices(radius: int, shoulder: int) -> tuple[tuple[int, int], ...]: + centre = radius + far = 2 * radius + return ( + (centre, 0), + (far, centre - shoulder), + (far, centre + shoulder), + (centre, far), + (0, centre + shoulder), + (0, centre - shoulder), + ) + + +def _hex_mask(radius: int, vertices: tuple[tuple[int, int], ...]) -> Image.Image: + size = 2 * radius + 1 + mask = Image.new("L", (size, size), 0) + ImageDraw.Draw(mask).polygon(vertices, fill=255) + return mask + + +def _hex_tile_asset( + edges: tuple[int, int, int, int, int, int], + palette: dict[int, tuple[int, int, int]], + radius: int, + vertices: tuple[tuple[int, int], ...], +) -> Image.Image: + size = 2 * radius + 1 + asset = Image.new("RGB", (size, size), BACKGROUND_RGB) + draw = ImageDraw.Draw(asset) + centre = (radius, radius) + for direction, color in enumerate(edges): + first_vertex = vertices[(direction + 1) % 6] + second_vertex = vertices[(direction + 2) % 6] + draw.polygon( + (centre, first_vertex, second_vertex), + fill=palette[color], + ) + draw.line((*vertices, vertices[0]), fill=GRID_RGB, width=1) + return asset + + +def _hex_hole_asset( + radius: int, + vertices: tuple[tuple[int, int], ...], +) -> Image.Image: + size = 2 * radius + 1 + coordinates = np.arange(size, dtype=np.int32) + x = np.broadcast_to(coordinates, (size, size)) + y = x.T + checker_size = max(2, radius // 4) + checker = ((x // checker_size) + (y // checker_size)) % 2 + colors = np.asarray((HOLE_LIGHT_RGB, HOLE_DARK_RGB), dtype=np.uint8) + asset = Image.fromarray(colors[checker], mode="RGB") + ImageDraw.Draw(asset).line( + (*vertices, vertices[0]), fill=GRID_RGB, width=1 + ) + return asset + + +def _compose_wang_hex( + square: WangPresentation, + *, + pixels_per_cell: int = DEFAULT_PIXELS_PER_CELL, + margin: int = DEFAULT_MARGIN, +) -> np.ndarray: + """Port, check, and compose one pointy-top axial hex canvas.""" + presentation = reduce_square_to_hex(square) + check_square_to_hex(square, presentation) + width, height, radius, shoulder, checked_margin = _hex_canvas_dimensions( + presentation, pixels_per_cell, margin + ) + canvas = Image.new("RGB", (width, height), BACKGROUND_RGB) + vertices = _hex_vertices(radius, shoulder) + mask = _hex_mask(radius, vertices) + hole = _hex_hole_asset(radius, vertices) + palette = _build_palette_from_edges(presentation.tile_edges) + tile_assets: dict[int, Image.Image] = {} + + min_center_x = ( + 2 * radius * presentation.min_q + radius * presentation.min_r + ) + min_center_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 + center_x = 2 * radius * q + radius * r + center_y = (radius + shoulder) * r + x = checked_margin + center_x - min_center_x + y = checked_margin + center_y - min_center_y + if tile_id is None: + asset = hole + else: + asset = tile_assets.get(tile_id) + if asset is None: + asset = _hex_tile_asset( + presentation.tile_edges[tile_id], + palette, + radius, + vertices, + ) + tile_assets[tile_id] = asset + canvas.paste(asset, (x, y), mask) + 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 @@ -485,20 +626,30 @@ def render_wang_square( *, pixels_per_cell: int = DEFAULT_PIXELS_PER_CELL, margin: int = DEFAULT_MARGIN, + hex_mode: bool = False, ) -> None: - """Load a v1 presentation, compose it, and atomically write one PNG.""" + """Load a v1 presentation and atomically write square or hex pixels.""" presentation = load_wang_presentation(input_path) - canvas = compose_wang_square( - presentation, - pixels_per_cell=pixels_per_cell, - margin=margin, - ) + if hex_mode: + canvas = _compose_wang_hex( + presentation, + pixels_per_cell=pixels_per_cell, + margin=margin, + ) + else: + canvas = compose_wang_square( + presentation, + pixels_per_cell=pixels_per_cell, + margin=margin, + ) _save_png_atomic(canvas, output_path) def _parser() -> argparse.ArgumentParser: parser = argparse.ArgumentParser( - description="Render a wang-solution-v1 square tiling as a diagnostic PNG" + description=( + "Render a wang-solution-v1 tiling as a diagnostic square or hex PNG" + ) ) parser.add_argument("input", help="path to a wang-solution-v1 JSON file") parser.add_argument("output", help="path to the output PNG") @@ -507,7 +658,7 @@ def _parser() -> argparse.ArgumentParser: type=int, default=DEFAULT_PIXELS_PER_CELL, help=( - "square cell size in pixels " + "square cell size or hex radius in pixels " f"(default: {DEFAULT_PIXELS_PER_CELL})" ), ) @@ -517,6 +668,11 @@ def _parser() -> argparse.ArgumentParser: default=DEFAULT_MARGIN, help=f"canvas margin in pixels (default: {DEFAULT_MARGIN})", ) + parser.add_argument( + "--hex", + action="store_true", + help="port the square witness to pointy-top axial hexagons", + ) return parser @@ -529,6 +685,7 @@ def main(argv: list[str] | None = None) -> None: args.output, pixels_per_cell=args.pixels_per_cell, margin=args.margin, + hex_mode=args.hex, ) except (FileNotFoundError, WangSquareRenderError) as error: parser.error(str(error))