Add deterministic solver trace replay

Makefile

@@ -45,6 +45,7 @@ SERIAL_SOURCES := \
 	src/crosscheck/yang_zhang_witness.c \
 	src/solver/byte_support_table.c \
 	src/solver/failed_leaf_trace.c \
+	src/solver/solver_event_trace.c \
 	src/solver/solver_serial.c \
 	src/verify/verify_tiling.c \
 	src/io/json.c \

README.md

@@ -74,6 +74,8 @@ solving remains future work.
 | Square-to-hex presentation port | Implemented as a pure in-memory Basire/Culik mapping with a raster-independent checker; no hex solver, schema, or core model |
 | Static explainability snapshots | Implemented for parsed formula, canonical tile sheet, and unassigned region, with hash-bound JSON contracts and square/hex diagnostic views |
 | Reduction construction provenance | Implemented as a separate opt-in native-owned result with exact signal orders, swap-bound gadget spans, manifest v2, and a square overlay view; the compact standard ABI does not allocate it |
+| Native solver event trace | Implemented as separate opt-in reference/optimized entry points with bounded observed events, full initial state, checkpoints, manifest v3, independent offline replay, and deterministic PNG/GIF views |
+| Reproducible Z3 summaries | Implemented for fixed seed/thread settings and explicit Boolean/Wang encoding order, result/model, and stable project-owned counts; no internal Z3 trace claim |
 | 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 |
 
@@ -107,17 +109,19 @@ The implemented paths are:
                                           |                  |
                                           |                  v
                                 native reference/       Wang Z3
-                                optimized solver           |
-                                       |                   v
-                                       v             Python tiling checker
-                                native verifier
-                                       |
-                            copied tiling + Python checker
-                                       |
-                                       v
-                            wang-solution-v1 --> square PNG (default/explain)
-                                       \
-                                        +--> pure hex port/check --> hex PNG (--hex)
+                                optimized solver          |  \
+                                   |       |              |   +--> encoding-order summary
+                                   |       +--> observed trace      +--> PNG/GIF
+                                   |                 |       v
+                                   v                 |  Python tiling checker
+                            native verifier           v
+                                   |          offline replay --> PNG/GIF
+                        copied tiling + Python checker
+                                   |
+                                   v
+                        wang-solution-v1 --> square PNG (default/explain)
+                                   \
+                                    +--> pure hex port/check --> hex PNG (--hex)
 ```
 
 The witness bridge relates exact Boolean assignments to the variable cells of
@@ -153,11 +157,11 @@ diagram.
 Planned work remains separated into independently reviewed changes. The new
 priority is explainability across the deterministic pipeline:
 
-1. define bounded, deterministic event traces for native DFS and explicit
-   encoding summaries for Z3, then render partial states by replay;
-2. publish a compact formula-to-final-image gallery and optional technical
+1. publish a compact formula-to-final-image gallery and optional technical
    report from versioned examples;
-3. resume serial MRV and hard-UNSAT evidence before `TaskPlan` and OpenMP work.
+2. resume serial MRV and hard-UNSAT evidence;
+3. define `TaskPlan` only after the serial evidence, then implement and measure
+   real OpenMP execution.
 
 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
@@ -180,7 +184,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 238-test combined suite independently:
+`make check`. Run its 253-test combined suite independently:
 
 ```sh
 cd renderer
@@ -220,6 +224,28 @@ opt-in final explainability views.
 The [reduction explanation contract](docs/wang_reduction_explanation.md)
 defines native signal/gadget provenance, manifest v2, ownership, replay
 invariants, and the square-only construction overlay.
+The [solver event trace contract](docs/wang_solver_trace.md) defines bounded
+native capture, manifest v3, semantic replay, checkpoints, truncation, and the
+presentation-only animation boundary.
+
+To export one observed reference run and render selected replay states:
+
+```sh
+make shared
+uv run python tools/export_solver_trace.py \
+  tests/instances/pipeline_sat.cm13 build/solver-trace/manifest.json \
+  --event-capacity 4096 --checkpoint-interval 128 --checkpoint-capacity 32
+cd renderer
+uv run --locked python wang_trace_render.py \
+  ../build/solver-trace/manifest.json ../build/solver-trace/rendered
+```
+
+The fixed-configuration Boolean and Wang Z3 summaries are exported separately:
+
+```sh
+uv run python tools/export_z3_encoding_summaries.py \
+  tests/instances/pipeline_sat.cm13 build/z3-summaries
+```
 
 Useful individual targets:
 

docs/development_principles.md

@@ -6,7 +6,7 @@ description: How Tiling Foundry separates source data, derived state, native lif
 section: Architecture and correctness
 document_kind: Architecture reference
 status: Current implementation
-updated: 2026-08-25
+updated: 2026-08-27
 nav_order: 10
 ---
 
@@ -88,16 +88,19 @@ A module is implemented when it has:
 | `region` | Active cells and exposed boundary constraints | Solver domains and scheduling |
 | `yang_zhang` | Reduction construction, transferred swap trace, and immutable signal/gadget provenance | Solver state and presentation metadata |
 | `solver` | Domains, trail, assignments, and search state | Formula and reduction semantics |
+| `solver_trace` | Opt-in bounded semantic events, full initial state, checkpoints, and their owned lifetime | Solving policy, raster composition, and Z3 internals |
 | `verify` | Stateless validation of a candidate tiling | Search logic and solver caches |
 | `crosscheck` | Stateless Boolean/Wang witness translation over a live reduction | Generic solver internals, clause validity, and copied swap data |
 | `task_plan` | Future derived scheduling data | `Region` or serial-solver ownership |
-| `python/model` | Pure immutable formula, region, tiling, and reduction-explanation contracts | I/O, ctypes, Z3, and native ownership |
-| `python/native` | C ABI adaptation, scoped native lifetimes, and complete copy-out | Solver logic and escaping native pointers |
+| `python/model` | Pure immutable formula, region, tiling, reduction-explanation, and solver-trace contracts | I/O, ctypes, Z3, and native ownership |
+| `python/native` | C ABI adaptation, scoped native lifetimes, and complete result/trace copy-out | Solver logic and escaping native pointers |
 | `python/crosscheck` | Scoped composition of adapters, Z3, and independent checkers | Persistent native state and duplicated reduction semantics |
 | `python/oracles` | Independent solvers and checkers over pure models | Parsing, filesystem I/O, and reduction construction |
-| `python/formats` | Solution, static-stage, and reduction-provenance validation and deterministic export | Native lifetimes, solving, and presentation |
+| `python/formats` | Solution, static-stage, reduction-provenance, observed-trace, and Z3 encoding-summary validation/export | Native lifetimes, solving, and presentation |
 | `renderer/wang_hex_port.py` | Pure square-to-hex mapping, inverse checks, and matching-equivalence checks | Raster geometry, semantic verification, and solver access |
 | `renderer/wang_snapshot.py` | Strict hash-bound formula, tile-sheet, region, and recorded reduction-provenance views | Native access, solving, and geometry reconstruction |
+| `renderer/wang_trace.py` | Strict hash-bound trace loading and independent ordered-delta replay | Native access, frame composition, and solving |
+| `renderer/wang_animation.py` | Deterministic atomic PNG, contact-sheet, and GIF encoding from already composed frames | State reconstruction and correctness claims |
 | `renderer/wang_square.py` | One CLI for solution and static views, with square/default or hex/explicit rasterization | Semantic verification and solver access |
 
 `include/wang/task_plan.h`, `src/parallel/solver_openmp.c`, and the two modules
@@ -107,10 +110,10 @@ the implemented solution contract and exporter are Python modules under
 
 ### Native and Python ownership flow
 
-The C parser and Yang–Zhang builder own native allocations. The adapters copy
-complete values into immutable Python `Formula`, `Region`,
-`ReductionExplanation`, tileset, and tiling models. No ctypes pointer reaches
-those models or their consumers.
+The C parser, Yang–Zhang builder, and opt-in traced solver calls own native
+allocations. The adapters copy complete values into immutable Python `Formula`,
+`Region`, `ReductionExplanation`, solver trace, tileset, and tiling models. No
+ctypes pointer reaches those models or their consumers.
 
 ```text
                     C parser + Yang–Zhang builder
@@ -129,9 +132,9 @@ those models or their consumers.
          v                v
    Python oracles    checkers / exporter --> Wang renderer
                                              |       \
-                                             |        +--> pure hex port/check
+                               trace replay -+        +--> pure hex port/check
                                              v                    |
-                                       square PNG                 v
+                                      PNG/GIF views               v
                                                             hex PNG
 ```
 
@@ -154,6 +157,13 @@ reverse-marshalled into `Cm13Formula` or `Region`.
 and `native/solve_pipeline.py` supplies copied, independently checked native
 tilings to producers without importing Z3.
 
+The trace coordinator similarly parses and reduces once, copies the ordinary
+result plus every semantic event and checkpoint before native destruction, and
+checks any SAT tiling independently. Its JSON producer reuses the existing
+formula, tileset, region, reduction, and solution formats. The renderer performs
+one offline replay and passes already composed frames to the shared image
+encoder; it never reconstructs solver state from pixels.
+
 ### Oracle and verifier contracts
 
 | Component | Input | Result | Independence boundary |
@@ -168,6 +178,11 @@ For generic tilesets with duplicate edge tuples, Wang Z3 returns a valid
 positional ID from the constraint-equivalent entries. Its public contract does
 not choose one duplicate over another.
 
+Both Z3 encoders fix `random_seed=0`, `threads=1`, and their explicit constraint
+order. A closed summary records the locked Z3 version, result/model, and stable
+project-owned encoding counts. Raw Z3 statistics and internal debug/search
+order are deliberately outside the stable contract.
+
 ### Witness correspondence boundary
 
 The witness bridge adds exact assignment extension and tiling extraction above