Add native reduction provenance snapshots

README.md

@@ -73,6 +73,7 @@ solving remains future work.
 | 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 |
 | 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 C JSON layer | Not implemented; `src/io/json.c` is a placeholder |
 | `TaskPlan` and native OpenMP solver | Not implemented; only the build scaffold exists |
 
@@ -97,13 +98,14 @@ The implemented paths are:
                           |                                      v
                           |                             Boolean witness checker
                           v
-                  Yang–Zhang builder --> Region
-                                          |  |\
-                                          |  | +--> static manifest --> region view
-                                          |  |                         + tile sheet
-                                          |  +----> copied Region + TILESET
-                                          |                |
-                                          |                v
+                  Yang–Zhang builder --> Region + ReductionExplanation
+                                          |  |  |\
+                                          |  |  | +--> v2 manifest --> reduction view
+                                          |  |  +----> v1 manifest --> region view
+                                          |  |                           + tile sheet
+                                          |  +-------> copied Region + TILESET
+                                          |                  |
+                                          |                  v
                                 native reference/       Wang Z3
                                 optimized solver           |
                                        |                   v
@@ -151,12 +153,11 @@ diagram.
 Planned work remains separated into independently reviewed changes. The new
 priority is explainability across the deterministic pipeline:
 
-1. add provenance overlays from formula positions to region structures without
-   changing the generic `Region` model;
-2. define bounded, deterministic event traces for native DFS and explicit
+1. define bounded, deterministic event traces for native DFS and explicit
    encoding summaries for Z3, then render partial states by replay;
-3. publish a compact formula-to-final-image gallery from versioned examples;
-4. resume serial MRV and hard-UNSAT evidence before `TaskPlan` and OpenMP work.
+2. 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.
 
 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
@@ -179,7 +180,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 234-test combined suite independently:
+`make check`. Run its 238-test combined suite independently:
 
 ```sh
 cd renderer
@@ -216,6 +217,9 @@ inverse proof, checker boundary, and integer axial raster convention.
 The [static snapshot contract](docs/wang_explainability_snapshots.md) documents
 the real formula-to-region export and the formula, tile-sheet, region, and
 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.
 
 Useful individual targets:
 

docs/development_principles.md

@@ -86,18 +86,18 @@ A module is implemented when it has:
 | `tile` | Fixed tileset, colors, and local matching | Search state |
 | `permutation` | Signal tokens and adjacent-swap generation | Region geometry |
 | `region` | Active cells and exposed boundary constraints | Solver domains and scheduling |
-| `yang_zhang` | Reduction construction and the transferred swap trace | Solver state and duplicated permutation data |
+| `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 |
 | `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 data contracts | I/O, ctypes, Z3, and native 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/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 and static pipeline snapshot validation and deterministic export | Native lifetimes, solving, and presentation |
+| `python/formats` | Solution, static-stage, and reduction-provenance validation and deterministic 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 snapshot consumption and static formula, tile-sheet, and region composition | Native access, solving, and semantic verification |
+| `renderer/wang_snapshot.py` | Strict hash-bound formula, tile-sheet, region, and recorded reduction-provenance views | Native access, solving, and geometry reconstruction |
 | `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
@@ -108,8 +108,9 @@ 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`, tileset, and tiling
-models. No ctypes pointer reaches those models or their consumers.
+complete values into immutable Python `Formula`, `Region`,
+`ReductionExplanation`, tileset, and tiling models. No ctypes pointer reaches
+those models or their consumers.
 
 ```text
                     C parser + Yang–Zhang builder
@@ -140,10 +141,12 @@ positions of every clause and releases the native formula in a `finally`
 block.
 
 The reduction coordinator parses once. While the native formula is live, it
-builds the corresponding `YangZhangReduction` and copies any Python views that
-the selected path needs. Cleanup destroys the reduction before the formula.
-The swap trace stays native because no Python consumer uses it. Python models
-are not reverse-marshalled into `Cm13Formula` or `Region`.
+builds either the compact `YangZhangReduction` or the separate opt-in
+`YangZhangExplainedReduction`, then copies only the Python views selected by
+that path. Cleanup uses the matching destructor before releasing the formula.
+The explanation adapter copies the exact source/target signals, swap-bound
+gadget spans, and region extent before cleanup. Python models are not
+reverse-marshalled into `Cm13Formula` or `Region`.
 
 `native/_lib.py` centralizes lazy `libwang.so` loading.
 `native/reduction_adapter.py` provides the copy-only formula/region path.

docs/reduction_notes.md

@@ -211,7 +211,10 @@ reduction stages:
   its active mask;
 - complete colors on every exposed side, including the staircase notches;
 - variable, clause, and isolated crossover boundary markers;
-- transactional transfer of the exact adjacent-swap trace.
+- transactional transfer of the exact adjacent-swap trace;
+- immutable source/target signal and gadget-span provenance from the same
+  construction, as specified by the
+  [reduction explanation contract]({{ '/wang-reduction-explanation/' | relative_url }}).
 
 Parsing, solving, tile selection, and persistent gadget annotations belong to
 other modules. The

docs/wang_explainability_snapshots.md

@@ -124,6 +124,11 @@ solver events nor a partial assignment. Deterministic event traces, replayed
 partial states, and algorithm-specific ordering require a separate trace
 contract because native DFS and Z3 do not expose the same kind of step.
 
+The next construction boundary is implemented separately by the
+[reduction explanation contract]({{ '/wang-reduction-explanation/' | relative_url }}).
+Its opt-in manifest v2 adds native-produced signals, adjacent-swap replay, and
+gadget spans while leaving this manifest v1 and the generic `Region` unchanged.
+
 The producer is standard-library-only and depends on copied immutable models.
 The renderer independently consumes the JSON without importing `libwang.so`,
 native adapters, or Z3. Golden PNGs cover all five static geometry/view pairs

docs/wang_reduction_explanation.md

@@ -0,0 +1,142 @@
+---
+layout: page
+title: "Yang–Zhang reduction explanation contract"
+permalink: /wang-reduction-explanation/
+description: Native-produced signal, permutation, and gadget provenance for one formula-to-region construction.
+section: Yang–Zhang reduction
+document_kind: Data and rendering contract
+status: Current implementation
+updated: 2026-08-27
+nav_order: 25
+---
+
+# Yang–Zhang reduction explanation contract
+
+The reduction builder can preserve an immutable explanation of the region it
+actually constructed. This result connects formula variables and clause
+positions to logical signals, the adjacent-swap program, and the half-open
+rectangles occupied by the coarse gadgets. It is diagnostic provenance, not
+solver input or a second implementation of the reduction.
+
+`Region` remains the generic square-grid model: active cells and exposed
+boundary colors only. The separate `ReductionExplanation` has its own semantic
+invariants, native storage, lifetime, copied Python model, JSON contract, and
+renderer consumer.
+
+## Native result and ownership
+
+A successful opt-in `yang_zhang_build_explained()` owns three related results:
+
+- the completed `Region`;
+- the exact adjacent-swap array used by the construction;
+- a `ReductionExplanation` containing the exact source and target signal
+  arrays passed to the permutation builder and the gadget spans emitted from
+  the same dimensioned build.
+
+The standard `yang_zhang_build()` returns the original compact
+`YangZhangReduction`, frees temporary signals immediately after permutation
+construction, and performs no provenance allocation. Ordinary solving and
+benchmarks therefore do not pay for this diagnostic result, and the public
+reduction ABI does not change. The opt-in entry point instead returns a
+`YangZhangExplainedReduction` containing that compact result plus the owned
+explanation arrays. They remain immutable after construction and
+`yang_zhang_explained_reduction_destroy()` releases and zeros both parts.
+Failed construction transfers nothing and leaves the output destroyed. The
+Python adapter copies every value before that native cleanup; no pointer
+escapes into the immutable Python model.
+
+This structure is not a temporary output bundle. It represents a domain object
+with independent invariants and an owned lifetime, and it has an immediate
+exporter and renderer consumer.
+
+## Signal identity and permutation
+
+Each signal stores its row, kind, unique token ID, and, for variable signals,
+the variable and occurrence numbers. The source order has three rows per
+variable and one redundant row between variable groups. The target order
+follows all three ordered positions of each clause, retaining repeated
+variables exactly.
+
+The recorded crossover gadgets are ordered by their swap ordinal. Each one
+stores `swap_row`; replaying those adjacent swaps over the source token
+identities must produce the target sequence exactly. Validators additionally
+bind the source sequence to formula variables and the target sequence to the
+referenced clause positions.
+
+## Gadget spans
+
+Every gadget uses a half-open rectangle:
+
+```text
+[x_begin, x_end) × [y_begin, y_end)
+```
+
+The closed kind set is:
+
+| Kind | Ordinal identifies | Meaning |
+| --- | --- | --- |
+| `variable` | variable ID | Three-row variable input block |
+| `left_forward` | always zero | Project-specific entry forwarder band |
+| `crossover` | swap index | One adjacent-swap block; width is `swap_row + 1` |
+| `right_forward` | always zero | Project-specific exit forwarder band |
+| `clause` | clause ID | Clause-side staircase interval |
+
+All rectangles must lie inside the constructed region extent. Provenance does
+not enter `Region`, the generic solver, the verifier, or `TaskPlan`.
+
+## Versioned export
+
+The opt-in export adds two closed Draft 2020-12 contracts:
+
+- `wang-reduction-explanation-v1` contains square bounds, source and target
+  signals, gadget spans, the source formula digest, and the exact region
+  artifact digest;
+- `wang-explain-manifest-v2` references formula, tileset, region, and reduction
+  artifacts by basename, schema, and full SHA-256 digest.
+
+Manifest v1 remains unchanged for formula, tile-sheet, and plain region views.
+Generate v2 from the real parser and builder with:
+
+```sh
+make shared
+uv run --frozen python tools/export_pipeline_snapshots.py \
+  tests/instances/pipeline_sat.cm13 \
+  /tmp/pipeline-sat-reduction/manifest.json \
+  --reduction-explanation
+```
+
+The manifest is installed last and atomically. Loading verifies all artifact
+hashes, formula identity, region identity, dimensions, signal populations,
+formula-to-signal correspondence, crossover replay, and gadget bounds.
+
+## Renderer view
+
+The isolated renderer accepts v1 and v2 manifests. The reduction view requires
+v2:
+
+```sh
+cd renderer
+uv run --locked python wang_square.py \
+  ../tests/fixtures/pipeline_sat_reduction_explain/manifest.json \
+  output/reduction.png \
+  --view reduction
+```
+
+It overlays semantic gadget colors on the unassigned region, labels every
+source row and clause destination, lists the parsed formula, and retains the
+logical boundary-color legend. The renderer only displays recorded data; it
+does not reconstruct gadget geometry or load native code.
+
+Reduction provenance is square-specific, so this view rejects `--hex` rather
+than implying that square gadget intervals have a hex-domain meaning. The
+plain region and tileset views retain their separately checked `--hex`
+presentation.
+
+## Scope boundary
+
+The explanation records construction, not solving. It contains no tile
+assignment, domain, propagation, decision, conflict, backtrack, runtime, or Z3
+internal order. Those belong to the separate bounded trace and report packets.
+A valid explanation proves that artifacts agree with the recorded builder
+output; it does not by itself prove SAT, tiling validity, or the mathematical
+correctness of the reduction.

docs/yang_zhang_builder_design.md

@@ -6,7 +6,7 @@ description: Data flow, geometry, ownership, and tested invariants of the implem
 section: Yang–Zhang reduction
 document_kind: Implementation contract
 status: Current implementation
-updated: 2026-08-25
+updated: 2026-08-27
 nav_order: 20
 ---
 
@@ -16,8 +16,9 @@ nav_order: 20
 
 The builder consumes a validated canonical Cubic Monotone 1-in-3 SAT formula.
 It constructs the colored simply connected `Region` used by the fixed 23-tile
-Yang–Zhang reduction and returns the exact adjacent-swap trace in the same
-transactional result.
+Yang–Zhang reduction and returns the exact adjacent-swap trace. An opt-in
+result preserves immutable construction provenance with a separate explicit
+lifetime, without changing the standard reduction ABI.
 
 This is the implementation contract for builder input validation, routing,
 coordinates, active geometry, exposed boundary colors, ownership, and
@@ -49,7 +50,8 @@ transport, and rendering have separate contracts.
 
 ```text
 validated canonical Cubic Monotone 1-in-3 formula
-    -> colored simply connected Region + exact adjacent-swap trace
+    -> YangZhangReduction
+    -> optional YangZhangExplainedReduction
 ```
 
 The builder performs these stages:
@@ -61,7 +63,10 @@ The builder performs these stages:
 4. compute the layout dimensions;
 5. build the complete active mask;
 6. color every exposed unit edge of the region;
-7. return the region and the exact swap array transactionally.
+7. retain the exact source/target signals and emit the gadget spans from those
+   same dimensioned construction stages;
+8. return the compact standard result, or the standard result and explanation
+   together through the opt-in wrapper, transactionally.
 
 Responsibilities outside the builder are:
 
@@ -151,30 +156,51 @@ typedef struct {
     size_t swap_count;
 } YangZhangReduction;
 
+typedef struct {
+    YangZhangReduction reduction;
+    ReductionExplanation explanation;
+} YangZhangExplainedReduction;
+
 bool yang_zhang_build(
     const Cm13Formula *formula,
     YangZhangReduction *out_reduction
 );
 
+bool yang_zhang_build_explained(
+    const Cm13Formula *formula,
+    YangZhangExplainedReduction *out_reduction
+);
+
 void yang_zhang_reduction_destroy(YangZhangReduction *reduction);
+void yang_zhang_explained_reduction_destroy(
+    YangZhangExplainedReduction *reduction
+);
 ```
 
 The exact array returned by `yang_zhang_permutation_build()` is transferred
 into `YangZhangReduction`; it is not copied. It is retained as a diagnostic
 trace of the reduction and as possible input to later task-plan preprocessing.
-The reference solver and independent verifier receive only `Region` and do not
-use this logical trace.
+The opt-in wrapper retains the source and target arrays that were actually
+passed to that permutation build and records half-open variable, forwarder,
+crossover, and clause rectangles. The reference solver and independent
+verifier receive only `Region` and do not use this diagnostic provenance. Its
+full data contract is the [reduction explanation reference]({{ '/wang-reduction-explanation/' | relative_url }}).
 
 The output starts in the destroyed state:
 
 ```c
 YangZhangReduction reduction = {0};
 ```
 
-`yang_zhang_build()` requires a destroyed/zeroed output. On success, the caller
-owns both `region.cells` and `swaps`. On every failure, the output remains in
-the destroyed state. `yang_zhang_reduction_destroy()` accepts null, destroys
-the region, frees the swap array, and resets every field to zero/null.
+Both build entry points require a destroyed/zeroed output. The standard call
+owns only `region.cells` and `swaps`, retains its original public layout, frees
+temporary signals as soon as permutation construction finishes, and does not
+allocate provenance. The opt-in call uses a zeroed
+`YangZhangExplainedReduction`; its `explanation` owns the retained signals and
+gadget spans. On every failure, the selected output remains destroyed.
+`yang_zhang_reduction_destroy()` releases the compact result, while
+`yang_zhang_explained_reduction_destroy()` releases and zeros both parts of the
+opt-in wrapper. Both accept null.
 
 The builder is safe to call concurrently for immutable formulas when each call
 uses a distinct output object. It owns no global mutable state.