diff --git a/README.md b/README.md index 273168d..2657bf2 100644 --- a/README.md +++ b/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: diff --git a/docs/development_principles.md b/docs/development_principles.md index 3f34ea6..5b6d419 100644 --- a/docs/development_principles.md +++ b/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. diff --git a/docs/reduction_notes.md b/docs/reduction_notes.md index f3cf0aa..fcfde1c 100644 --- a/docs/reduction_notes.md +++ b/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 diff --git a/docs/wang_explainability_snapshots.md b/docs/wang_explainability_snapshots.md index f43047f..37ba5ac 100644 --- a/docs/wang_explainability_snapshots.md +++ b/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 diff --git a/docs/wang_reduction_explanation.md b/docs/wang_reduction_explanation.md new file mode 100644 index 0000000..35160f8 --- /dev/null +++ b/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. diff --git a/docs/yang_zhang_builder_design.md b/docs/yang_zhang_builder_design.md index 187360b..c9fde4d 100644 --- a/docs/yang_zhang_builder_design.md +++ b/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,19 +156,35 @@ 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: @@ -171,10 +192,15 @@ The output starts in the destroyed state: 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. diff --git a/include/wang/reduction_explanation.h b/include/wang/reduction_explanation.h new file mode 100644 index 0000000..74403a1 --- /dev/null +++ b/include/wang/reduction_explanation.h @@ -0,0 +1,59 @@ +#ifndef WANG_REDUCTION_EXPLANATION_H +#define WANG_REDUCTION_EXPLANATION_H + +#include +#include + +#include "wang/permutation.h" + +/* + * Semantic kinds of the coarse Yang-Zhang gadgets built into a Region. + * These values describe construction provenance; solvers never consume them. + */ +typedef enum { + REDUCTION_GADGET_VARIABLE, + REDUCTION_GADGET_LEFT_FORWARD, + REDUCTION_GADGET_CROSSOVER, + REDUCTION_GADGET_RIGHT_FORWARD, + REDUCTION_GADGET_CLAUSE +} ReductionGadgetKind; + +#define REDUCTION_NO_SWAP_ROW UINT32_MAX + +/* + * One half-open rectangle [x_begin, x_end) x [y_begin, y_end). + * + * ordinal identifies the variable, clause, or adjacent swap for those gadget + * kinds. Both forwarder bands use ordinal zero. swap_row is meaningful only + * for REDUCTION_GADGET_CROSSOVER and otherwise equals + * REDUCTION_NO_SWAP_ROW. + */ +typedef struct { + ReductionGadgetKind kind; + uint32_t ordinal; + int32_t x_begin; + int32_t x_end; + int32_t y_begin; + int32_t y_end; + uint32_t swap_row; +} ReductionGadgetSpan; + +/* + * Immutable construction provenance owned by a successful + * YangZhangExplainedReduction returned by yang_zhang_build_explained(). + * + * source_signals and target_signals are the exact sequences passed to the + * permutation builder. Their array index is the zero-based signal row. + * gadgets records the coarse rectangles actually used to build the Region. + * Callers borrow every pointer and must not modify or release this storage. + */ +typedef struct { + SignalToken *source_signals; + SignalToken *target_signals; + size_t signal_count; + + ReductionGadgetSpan *gadgets; + size_t gadget_count; +} ReductionExplanation; + +#endif /* WANG_REDUCTION_EXPLANATION_H */ diff --git a/include/wang/yang_zhang.h b/include/wang/yang_zhang.h index e1c89b1..13ba9e4 100644 --- a/include/wang/yang_zhang.h +++ b/include/wang/yang_zhang.h @@ -7,14 +7,16 @@ #include "wang/formula.h" #include "wang/permutation.h" +#include "wang/reduction_explanation.h" #include "wang/region.h" /* * Result of a Yang-Zhang reduction build. * - * On successful construction, the caller owns both region.cells and swaps. - * Initialize this object to zero before use and release it with - * yang_zhang_reduction_destroy(). + * On successful construction, the caller owns region.cells and swaps. + * Initialize this object to zero before use and release every owned allocation + * with yang_zhang_reduction_destroy(). Its layout is kept ABI-compatible with + * the original public reduction result. */ typedef struct { Region region; @@ -23,9 +25,19 @@ typedef struct { size_t swap_count; } YangZhangReduction; +/* + * Opt-in result that gives the Region build and its diagnostic provenance one + * explicit joint lifetime without changing the YangZhangReduction ABI. + */ +typedef struct { + YangZhangReduction reduction; + ReductionExplanation explanation; +} YangZhangExplainedReduction; + /* * Build the colored region and adjacent-swap trace for a canonical CM1-in-3 - * formula. The formula is borrowed and is never modified. + * formula. The formula is borrowed and is never modified. This standard path + * performs no provenance allocation. * * The output must be zero-initialized or previously destroyed. Construction * is transactional: on failure, the output remains in the destroyed state. @@ -35,9 +47,24 @@ bool yang_zhang_build( YangZhangReduction *out_reduction ); -/* Release all owned storage and reset every field. Accepts NULL. */ +/* + * Build the same region and swap trace while also retaining immutable signal + * and gadget provenance. Geometry and swap generation share the standard + * implementation; this opt-in entry point only changes explanation ownership. + */ +bool yang_zhang_build_explained( + const Cm13Formula *formula, + YangZhangExplainedReduction *out_reduction +); + +/* Release standard result storage and reset every field. Accepts NULL. */ void yang_zhang_reduction_destroy(YangZhangReduction *reduction); +/* Release an opt-in explained result and reset every field. Accepts NULL. */ +void yang_zhang_explained_reduction_destroy( + YangZhangExplainedReduction *reduction +); + /* * Yang-Zhang layout conventions used by this project. * diff --git a/python/formats/pipeline_snapshot.py b/python/formats/pipeline_snapshot.py index b4e1f28..3053de1 100644 --- a/python/formats/pipeline_snapshot.py +++ b/python/formats/pipeline_snapshot.py @@ -18,6 +18,17 @@ from typing import Final from model.formula import Formula +from model.reduction_explanation import ( + GADGET_CLAUSE, + GADGET_CROSSOVER, + GADGET_LEFT_FORWARD, + GADGET_RIGHT_FORWARD, + GADGET_VARIABLE, + SIGNAL_REDUNDANT, + SIGNAL_VARIABLE, + ReductionExplanation, + ReductionSignal, +) from model.region import Region from model.tileset import COLOR_NONE, TILESET, Tileset @@ -26,9 +37,22 @@ TILESET_SCHEMA: Final = "wang-tileset-snapshot-v1" REGION_SCHEMA: Final = "wang-region-snapshot-v1" MANIFEST_SCHEMA: Final = "wang-explain-manifest-v1" +REDUCTION_SCHEMA: Final = "wang-reduction-explanation-v1" +REDUCTION_MANIFEST_SCHEMA: Final = "wang-explain-manifest-v2" GEOMETRY: Final = "square" STAGE: Final = "region" +REDUCTION_STAGE: Final = "reduction" DIRECTIONS: Final = ("N", "E", "S", "W") +SIGNAL_KINDS: Final = frozenset({SIGNAL_VARIABLE, SIGNAL_REDUNDANT}) +GADGET_KINDS: Final = frozenset( + { + GADGET_VARIABLE, + GADGET_LEFT_FORWARD, + GADGET_CROSSOVER, + GADGET_RIGHT_FORWARD, + GADGET_CLAUSE, + } +) _OFFSETS: Final = ((0, -1), (1, 0), (0, 1), (-1, 0)) _SHA256_PATTERN: Final = re.compile(r"[0-9a-f]{64}") @@ -381,6 +405,231 @@ def validate_region_snapshot(document: object) -> None: ) +def _validate_explanation_signals( + value: object, + path: str, + *, + variable_count: int, + height: int, +) -> tuple[tuple[str, int, int | None, int | None], ...]: + signals = _require_array(value, path) + if len(signals) != height: + _fail(path, "length must equal the explanation height") + identities: list[tuple[str, int, int | None, int | None]] = [] + token_ids: set[int] = set() + occurrences: list[set[int]] = [set() for _ in range(variable_count)] + redundant_count = 0 + for row, raw_signal in enumerate(signals): + item_path = f"{path}[{row}]" + signal = _require_object(raw_signal, item_path) + _require_exact_fields( + signal, + frozenset({"row", "kind", "token_id", "variable", "occurrence"}), + item_path, + ) + actual_row = _require_integer( + signal["row"], + f"{item_path}.row", + nonnegative=True, + ) + if actual_row != row: + _fail(f"{item_path}.row", f"must equal canonical row {row}") + kind = _require_string(signal["kind"], f"{item_path}.kind") + if kind not in SIGNAL_KINDS: + _fail(f"{item_path}.kind", "is not a supported signal kind") + token_id = _require_integer( + signal["token_id"], + f"{item_path}.token_id", + nonnegative=True, + ) + if token_id in token_ids: + _fail(path, "token_id values must be unique") + token_ids.add(token_id) + if kind == SIGNAL_VARIABLE: + variable = _require_integer( + signal["variable"], + f"{item_path}.variable", + nonnegative=True, + ) + occurrence = _require_integer( + signal["occurrence"], + f"{item_path}.occurrence", + nonnegative=True, + ) + if variable >= variable_count: + _fail(f"{item_path}.variable", "is outside the formula") + if occurrence >= 3: + _fail(f"{item_path}.occurrence", "must be 0, 1, or 2") + occurrences[variable].add(occurrence) + else: + if signal["variable"] is not None or signal["occurrence"] is not None: + _fail(item_path, "redundant signal metadata must be null") + variable = None + occurrence = None + redundant_count += 1 + identities.append((kind, token_id, variable, occurrence)) + if any(values != {0, 1, 2} for values in occurrences): + _fail(path, "must contain occurrences 0, 1, and 2 for every variable") + if redundant_count != variable_count - 1: + _fail(path, "has an invalid redundant signal count") + return tuple(identities) + + +def validate_reduction_explanation_snapshot(document: object) -> None: + """Validate native-produced Yang-Zhang construction provenance.""" + root = _require_object(document, "$") + _require_exact_fields( + root, + frozenset( + { + "schema", + "geometry", + "source_formula_sha256", + "region_sha256", + "variable_count", + "bounds", + "signals", + "gadgets", + } + ), + "$", + ) + _require_literal(root["schema"], REDUCTION_SCHEMA, "$.schema") + _require_literal(root["geometry"], GEOMETRY, "$.geometry") + _require_sha256(root["source_formula_sha256"], "$.source_formula_sha256") + _require_sha256(root["region_sha256"], "$.region_sha256") + variable_count = _require_integer( + root["variable_count"], + "$.variable_count", + nonnegative=True, + ) + if variable_count == 0: + _fail("$.variable_count", "must be positive") + + bounds = _require_object(root["bounds"], "$.bounds") + _require_exact_fields( + bounds, + frozenset({"x_begin", "x_end", "y_begin", "y_end"}), + "$.bounds", + ) + x_begin = _require_integer( + bounds["x_begin"], + "$.bounds.x_begin", + nonnegative=True, + ) + x_end = _require_integer( + bounds["x_end"], + "$.bounds.x_end", + nonnegative=True, + ) + y_begin = _require_integer( + bounds["y_begin"], + "$.bounds.y_begin", + nonnegative=True, + ) + y_end = _require_integer( + bounds["y_end"], + "$.bounds.y_end", + nonnegative=True, + ) + if x_begin != 0 or y_begin != 0 or x_end <= 0 or y_end <= 0: + _fail("$.bounds", "must be a nonempty zero-origin half-open box") + if y_end != 4 * variable_count - 1: + _fail("$.bounds.y_end", "must equal 4 * variable_count - 1") + + signals = _require_object(root["signals"], "$.signals") + _require_exact_fields(signals, frozenset({"source", "target"}), "$.signals") + source = _validate_explanation_signals( + signals["source"], + "$.signals.source", + variable_count=variable_count, + height=y_end, + ) + target = _validate_explanation_signals( + signals["target"], + "$.signals.target", + variable_count=variable_count, + height=y_end, + ) + if frozenset(source) != frozenset(target): + _fail("$.signals", "source and target must contain the same tokens") + + gadgets = _require_array(root["gadgets"], "$.gadgets") + populations: dict[str, list[int]] = {kind: [] for kind in GADGET_KINDS} + crossover_rows: list[int] = [] + for index, raw_gadget in enumerate(gadgets): + path = f"$.gadgets[{index}]" + gadget = _require_object(raw_gadget, path) + _require_exact_fields( + gadget, + frozenset({"kind", "ordinal", "bounds", "swap_row"}), + path, + ) + kind = _require_string(gadget["kind"], f"{path}.kind") + if kind not in GADGET_KINDS: + _fail(f"{path}.kind", "is not a supported gadget kind") + ordinal = _require_integer( + gadget["ordinal"], + f"{path}.ordinal", + nonnegative=True, + ) + populations[kind].append(ordinal) + gadget_bounds = _require_object(gadget["bounds"], f"{path}.bounds") + _require_exact_fields( + gadget_bounds, + frozenset({"x_begin", "x_end", "y_begin", "y_end"}), + f"{path}.bounds", + ) + coordinates = tuple( + _require_integer( + gadget_bounds[name], + f"{path}.bounds.{name}", + nonnegative=True, + ) + for name in ("x_begin", "x_end", "y_begin", "y_end") + ) + gx_begin, gx_end, gy_begin, gy_end = coordinates + if gx_end <= gx_begin or gy_end <= gy_begin: + _fail(f"{path}.bounds", "must be a nonempty half-open rectangle") + if gx_end > x_end or gy_end > y_end: + _fail(f"{path}.bounds", "must lie inside the explanation bounds") + if kind == GADGET_CROSSOVER: + swap_row = _require_integer( + gadget["swap_row"], + f"{path}.swap_row", + nonnegative=True, + ) + if swap_row >= y_end - 1: + _fail(f"{path}.swap_row", "is outside the signal rows") + if gx_end - gx_begin != swap_row + 1: + _fail(f"{path}.bounds", "width must equal swap_row + 1") + crossover_rows.append(swap_row) + elif gadget["swap_row"] is not None: + _fail(f"{path}.swap_row", "must be null outside crossovers") + + expected_populations = { + GADGET_VARIABLE: variable_count, + GADGET_LEFT_FORWARD: 1, + GADGET_CROSSOVER: len(crossover_rows), + GADGET_RIGHT_FORWARD: 1, + GADGET_CLAUSE: variable_count, + } + for kind, expected_count in expected_populations.items(): + if populations[kind] != list(range(expected_count)): + _fail( + "$.gadgets", + f"{kind} ordinals must equal 0..{expected_count - 1}", + ) + replay = list(source) + for swap_row in crossover_rows: + replay[swap_row], replay[swap_row + 1] = ( + replay[swap_row + 1], + replay[swap_row], + ) + if tuple(replay) != target: + _fail("$.gadgets", "crossover program does not produce target signals") + + def _validate_reference( value: object, path: str, @@ -428,6 +677,36 @@ def validate_explain_manifest(document: object) -> None: ) +def validate_reduction_explain_manifest(document: object) -> None: + """Validate the v2 manifest that adds native reduction provenance.""" + root = _require_object(document, "$") + _require_exact_fields( + root, + frozenset({"schema", "stage", "source_formula_sha256", "artifacts"}), + "$", + ) + _require_literal(root["schema"], REDUCTION_MANIFEST_SCHEMA, "$.schema") + _require_literal(root["stage"], REDUCTION_STAGE, "$.stage") + _require_sha256(root["source_formula_sha256"], "$.source_formula_sha256") + artifacts = _require_object(root["artifacts"], "$.artifacts") + _require_exact_fields( + artifacts, + frozenset({"formula", "tileset", "region", "reduction"}), + "$.artifacts", + ) + for name, schema in ( + ("formula", FORMULA_SCHEMA), + ("tileset", TILESET_SCHEMA), + ("region", REGION_SCHEMA), + ("reduction", REDUCTION_SCHEMA), + ): + _validate_reference( + artifacts[name], + f"$.artifacts.{name}", + expected_schema=schema, + ) + + def _reject_duplicate_members( pairs: list[tuple[str, object]], ) -> dict[str, object]: @@ -488,6 +767,8 @@ def load_pipeline_snapshot(path: str | Path) -> dict[str, object]: TILESET_SCHEMA: validate_tileset_snapshot, REGION_SCHEMA: validate_region_snapshot, MANIFEST_SCHEMA: validate_explain_manifest, + REDUCTION_SCHEMA: validate_reduction_explanation_snapshot, + REDUCTION_MANIFEST_SCHEMA: validate_reduction_explain_manifest, } validator = validators.get(schema) if validator is None: @@ -496,26 +777,25 @@ def load_pipeline_snapshot(path: str | Path) -> dict[str, object]: return document -def load_explainability_bundle( +def _load_manifest_artifacts( manifest_path: str | Path, -) -> tuple[ - dict[str, object], - dict[str, object], - dict[str, object], - dict[str, object], -]: - """Load a manifest and its three hash-bound artifacts.""" + *, + manifest_schema: str, + artifact_schemas: tuple[tuple[str, str], ...], +) -> tuple[dict[str, object], dict[str, dict[str, object]]]: path = Path(manifest_path) manifest = load_pipeline_snapshot(path) - if manifest["schema"] != MANIFEST_SCHEMA: - _fail("$.schema", f"must equal {MANIFEST_SCHEMA!r}") + if manifest["schema"] != manifest_schema: + _fail("$.schema", f"must equal {manifest_schema!r}") artifacts = _require_object(manifest["artifacts"], "$.artifacts") + validators = { + FORMULA_SCHEMA: validate_formula_snapshot, + TILESET_SCHEMA: validate_tileset_snapshot, + REGION_SCHEMA: validate_region_snapshot, + REDUCTION_SCHEMA: validate_reduction_explanation_snapshot, + } loaded: dict[str, dict[str, object]] = {} - for name, schema in ( - ("formula", FORMULA_SCHEMA), - ("tileset", TILESET_SCHEMA), - ("region", REGION_SCHEMA), - ): + for name, schema in artifact_schemas: reference = _require_object(artifacts[name], f"$.artifacts.{name}") artifact_name, expected_digest = _validate_reference( reference, @@ -538,13 +818,15 @@ def load_explainability_bundle( document = _load_json_bytes(encoded, str(artifact_path)) if document.get("schema") != schema: _fail(f"$.artifacts.{name}.schema", "does not match artifact") - { - FORMULA_SCHEMA: validate_formula_snapshot, - TILESET_SCHEMA: validate_tileset_snapshot, - REGION_SCHEMA: validate_region_snapshot, - }[schema](document) + validators[schema](document) loaded[name] = document + return manifest, loaded + +def _validate_base_bundle_identity( + manifest: dict[str, object], + loaded: dict[str, dict[str, object]], +) -> str: formula = loaded["formula"] region = loaded["region"] tileset = loaded["tileset"] @@ -572,7 +854,155 @@ def load_explainability_bundle( f"region.boundary[{index}].{direction}", "is absent from the referenced tileset color set", ) - return manifest, formula, tileset, region + return source_digest + + +def _validate_reduction_bundle_identity( + manifest: dict[str, object], + loaded: dict[str, dict[str, object]], + source_digest: str, +) -> None: + reduction = loaded["reduction"] + if reduction["source_formula_sha256"] != source_digest: + _fail( + "reduction.source_formula_sha256", + "does not match the manifest formula identity", + ) + artifacts = _require_object(manifest["artifacts"], "$.artifacts") + region_reference = _require_object(artifacts["region"], "$.artifacts.region") + if reduction["region_sha256"] != region_reference["sha256"]: + _fail( + "reduction.region_sha256", + "does not match the referenced region artifact", + ) + if reduction["variable_count"] != loaded["formula"]["variable_count"]: + _fail( + "reduction.variable_count", + "does not match the referenced formula", + ) + variable_count = reduction["variable_count"] + expected_source: list[tuple[str, int, int | None, int | None]] = [] + for variable in range(variable_count): + expected_source.extend( + (SIGNAL_VARIABLE, 3 * variable + occurrence, variable, occurrence) + for occurrence in range(3) + ) + if variable + 1 < variable_count: + expected_source.append( + (SIGNAL_REDUNDANT, 3 * variable_count + variable, None, None) + ) + expected_target: list[tuple[str, int, int | None, int | None]] = [] + next_occurrence = [0] * variable_count + clauses = _require_array(loaded["formula"]["clauses"], "formula.clauses") + for clause_id, raw_clause in enumerate(clauses): + clause = _require_object(raw_clause, f"formula.clauses[{clause_id}]") + variables = _require_array( + clause["variables"], + f"formula.clauses[{clause_id}].variables", + ) + for variable in variables: + occurrence = next_occurrence[variable] + next_occurrence[variable] += 1 + expected_target.append( + (SIGNAL_VARIABLE, 3 * variable + occurrence, variable, occurrence) + ) + if clause_id + 1 < variable_count: + expected_target.append( + (SIGNAL_REDUNDANT, 3 * variable_count + clause_id, None, None) + ) + signals = _require_object(reduction["signals"], "reduction.signals") + actual_sequences: list[ + tuple[tuple[str, int, int | None, int | None], ...] + ] = [] + for name in ("source", "target"): + sequence = _require_array(signals[name], f"reduction.signals.{name}") + actual_sequences.append( + tuple( + ( + item["kind"], + item["token_id"], + item["variable"], + item["occurrence"], + ) + for item in sequence + ) + ) + if actual_sequences[0] != tuple(expected_source): + _fail("reduction.signals.source", "does not match the formula variables") + if actual_sequences[1] != tuple(expected_target): + _fail("reduction.signals.target", "does not match the formula clauses") + reduction_bounds = _require_object(reduction["bounds"], "reduction.bounds") + region_bounds = _require_object(loaded["region"]["bounds"], "region.bounds") + region_width = ( + region_bounds["max_x_inclusive"] + - region_bounds["min_x_inclusive"] + + 1 + ) + region_height = ( + region_bounds["max_y_inclusive"] + - region_bounds["min_y_inclusive"] + + 1 + ) + if reduction_bounds["x_end"] != region_width: + _fail("reduction.bounds.x_end", "does not match the region width") + if reduction_bounds["y_end"] != region_height: + _fail("reduction.bounds.y_end", "does not match the region height") + + +def load_explainability_bundle( + manifest_path: str | Path, +) -> tuple[ + dict[str, object], + dict[str, object], + dict[str, object], + dict[str, object], +]: + """Load a v1 manifest and its three hash-bound artifacts.""" + artifact_schemas = ( + ("formula", FORMULA_SCHEMA), + ("tileset", TILESET_SCHEMA), + ("region", REGION_SCHEMA), + ) + manifest, loaded = _load_manifest_artifacts( + manifest_path, + manifest_schema=MANIFEST_SCHEMA, + artifact_schemas=artifact_schemas, + ) + _validate_base_bundle_identity(manifest, loaded) + return manifest, loaded["formula"], loaded["tileset"], loaded["region"] + + +def load_reduction_explainability_bundle( + manifest_path: str | Path, +) -> tuple[ + dict[str, object], + dict[str, object], + dict[str, object], + dict[str, object], + dict[str, object], +]: + """Load a v2 manifest and verify formula, region, and provenance identity.""" + artifact_schemas = ( + ("formula", FORMULA_SCHEMA), + ("tileset", TILESET_SCHEMA), + ("region", REGION_SCHEMA), + ("reduction", REDUCTION_SCHEMA), + ) + manifest, loaded = _load_manifest_artifacts( + manifest_path, + manifest_schema=REDUCTION_MANIFEST_SCHEMA, + artifact_schemas=artifact_schemas, + ) + source_digest = _validate_base_bundle_identity(manifest, loaded) + _validate_reduction_bundle_identity(manifest, loaded, source_digest) + reduction = loaded["reduction"] + return ( + manifest, + loaded["formula"], + loaded["tileset"], + loaded["region"], + reduction, + ) def build_formula_snapshot( @@ -680,6 +1110,68 @@ def build_region_snapshot( return document +def build_reduction_explanation_snapshot( + explanation: ReductionExplanation, + *, + source_formula_sha256: str, + region_sha256: str, +) -> dict[str, object]: + """Build a snapshot from copied provenance produced by the native builder.""" + if not isinstance(explanation, ReductionExplanation): + raise TypeError("explanation must be a ReductionExplanation") + _require_sha256(source_formula_sha256, "source_formula_sha256") + _require_sha256(region_sha256, "region_sha256") + + def signal_document(signal: ReductionSignal) -> dict[str, object]: + return { + "row": signal.row, + "kind": signal.kind, + "token_id": signal.token_id, + "variable": signal.variable, + "occurrence": signal.occurrence, + } + + document: dict[str, object] = { + "schema": REDUCTION_SCHEMA, + "geometry": GEOMETRY, + "source_formula_sha256": source_formula_sha256, + "region_sha256": region_sha256, + "variable_count": explanation.variable_count, + "bounds": { + "x_begin": 0, + "x_end": explanation.width, + "y_begin": 0, + "y_end": explanation.height, + }, + "signals": { + "source": [ + signal_document(signal) + for signal in explanation.source_signals + ], + "target": [ + signal_document(signal) + for signal in explanation.target_signals + ], + }, + "gadgets": [ + { + "kind": gadget.kind, + "ordinal": gadget.ordinal, + "bounds": { + "x_begin": gadget.x_begin, + "x_end": gadget.x_end, + "y_begin": gadget.y_begin, + "y_end": gadget.y_end, + }, + "swap_row": gadget.swap_row, + } + for gadget in explanation.gadgets + ], + } + validate_reduction_explanation_snapshot(document) + return document + + def _encode_document(document: dict[str, object]) -> bytes: serialized = json.dumps( document, @@ -716,17 +1208,25 @@ def _write_atomic(path: Path, encoded: bytes) -> None: pass -def dump_pipeline_snapshots( +def _dump_snapshot_bundle( manifest_path: str | Path, source_path: str | Path, formula: Formula, region: Region, *, origin: tuple[int, int] = (0, 0), + explanation: ReductionExplanation | None, ) -> Path: - """Write content-addressed artifacts, then atomically install a manifest.""" destination = Path(manifest_path) source = Path(source_path) + if explanation is not None and ( + explanation.variable_count != formula.variable_count + or explanation.width != region.width + or explanation.height != region.height + ): + raise PipelineSnapshotError( + "reduction explanation identity does not match formula and region" + ) try: source_bytes = source.read_bytes() except OSError as error: @@ -750,6 +1250,9 @@ def dump_pipeline_snapshots( "tileset": (TILESET_SCHEMA, tileset_document), "region": (REGION_SCHEMA, region_document), } + loaded_documents = { + name: document for name, (_, document) in documents.items() + } references: dict[str, object] = {} for name, (schema, document) in documents.items(): encoded = _encode_document(document) @@ -768,13 +1271,98 @@ def dump_pipeline_snapshots( "schema": schema, } + if explanation is not None: + region_reference = _require_object( + references["region"], + "references.region", + ) + explanation_document = build_reduction_explanation_snapshot( + explanation, + source_formula_sha256=source_digest, + region_sha256=region_reference["sha256"], + ) + encoded = _encode_document(explanation_document) + digest = hashlib.sha256(encoded).hexdigest() + artifact_name = f"reduction-{digest}.json" + if artifact_name == destination.name: + raise PipelineSnapshotError( + "manifest filename must not collide with a generated " + f"artifact: {artifact_name}" + ) + _write_atomic(destination.parent / artifact_name, encoded) + references["reduction"] = { + "path": artifact_name, + "sha256": digest, + "schema": REDUCTION_SCHEMA, + } + loaded_documents["reduction"] = explanation_document + + manifest_schema = ( + REDUCTION_MANIFEST_SCHEMA if explanation is not None else MANIFEST_SCHEMA + ) + stage = REDUCTION_STAGE if explanation is not None else STAGE manifest: dict[str, object] = { - "schema": MANIFEST_SCHEMA, - "stage": STAGE, + "schema": manifest_schema, + "stage": stage, "source_formula_sha256": source_digest, "artifacts": references, } - validate_explain_manifest(manifest) + if explanation is None: + validate_explain_manifest(manifest) + else: + validate_reduction_explain_manifest(manifest) + validated_source_digest = _validate_base_bundle_identity( + manifest, + loaded_documents, + ) + if explanation is not None: + _validate_reduction_bundle_identity( + manifest, + loaded_documents, + validated_source_digest, + ) _write_atomic(destination, _encode_document(manifest)) - load_explainability_bundle(destination) + if explanation is None: + load_explainability_bundle(destination) + else: + load_reduction_explainability_bundle(destination) return destination + + +def dump_pipeline_snapshots( + manifest_path: str | Path, + source_path: str | Path, + formula: Formula, + region: Region, + *, + origin: tuple[int, int] = (0, 0), +) -> Path: + """Write v1 static artifacts, then atomically install their manifest.""" + return _dump_snapshot_bundle( + manifest_path, + source_path, + formula, + region, + origin=origin, + explanation=None, + ) + + +def dump_reduction_explanation_snapshots( + manifest_path: str | Path, + source_path: str | Path, + formula: Formula, + region: Region, + explanation: ReductionExplanation, + *, + origin: tuple[int, int] = (0, 0), +) -> Path: + """Write v2 artifacts including native construction provenance.""" + return _dump_snapshot_bundle( + manifest_path, + source_path, + formula, + region, + origin=origin, + explanation=explanation, + ) diff --git a/python/model/reduction_explanation.py b/python/model/reduction_explanation.py new file mode 100644 index 0000000..2b3aac2 --- /dev/null +++ b/python/model/reduction_explanation.py @@ -0,0 +1,213 @@ +"""Immutable provenance for one native Yang-Zhang reduction build.""" + +from dataclasses import dataclass +from typing import Final + + +SIGNAL_VARIABLE: Final = "variable" +SIGNAL_REDUNDANT: Final = "redundant" +SIGNAL_KINDS: Final = frozenset({SIGNAL_VARIABLE, SIGNAL_REDUNDANT}) + +GADGET_VARIABLE: Final = "variable" +GADGET_LEFT_FORWARD: Final = "left_forward" +GADGET_CROSSOVER: Final = "crossover" +GADGET_RIGHT_FORWARD: Final = "right_forward" +GADGET_CLAUSE: Final = "clause" +GADGET_KINDS: Final = frozenset( + { + GADGET_VARIABLE, + GADGET_LEFT_FORWARD, + GADGET_CROSSOVER, + GADGET_RIGHT_FORWARD, + GADGET_CLAUSE, + } +) + + +@dataclass(frozen=True, slots=True) +class ReductionSignal: + """One logical signal token at one zero-based row.""" + + row: int + kind: str + token_id: int + variable: int | None + occurrence: int | None + + def __post_init__(self) -> None: + if type(self.row) is not int or self.row < 0: + raise ValueError("signal row must be a nonnegative integer") + if type(self.kind) is not str or self.kind not in SIGNAL_KINDS: + raise ValueError("signal kind is invalid") + if type(self.token_id) is not int or self.token_id < 0: + raise ValueError("signal token_id must be a nonnegative integer") + if self.kind == SIGNAL_VARIABLE: + if type(self.variable) is not int or self.variable < 0: + raise ValueError("variable signal must identify a variable") + if type(self.occurrence) is not int or not 0 <= self.occurrence < 3: + raise ValueError("variable occurrence must be 0, 1, or 2") + elif self.variable is not None or self.occurrence is not None: + raise ValueError("redundant signal cannot identify a variable occurrence") + + @property + def identity(self) -> tuple[str, int, int | None, int | None]: + """Return the row-independent logical identity of this token.""" + + return (self.kind, self.token_id, self.variable, self.occurrence) + + +@dataclass(frozen=True, slots=True) +class ReductionGadget: + """One semantic gadget rectangle using half-open coordinates.""" + + kind: str + ordinal: int + x_begin: int + x_end: int + y_begin: int + y_end: int + swap_row: int | None + + def __post_init__(self) -> None: + if type(self.kind) is not str or self.kind not in GADGET_KINDS: + raise ValueError("gadget kind is invalid") + if type(self.ordinal) is not int or self.ordinal < 0: + raise ValueError("gadget ordinal must be a nonnegative integer") + for name in ("x_begin", "x_end", "y_begin", "y_end"): + if type(getattr(self, name)) is not int: + raise TypeError(f"gadget {name} must be an integer") + if self.x_begin < 0 or self.x_end <= self.x_begin: + raise ValueError("gadget x interval must be nonempty and nonnegative") + if self.y_begin < 0 or self.y_end <= self.y_begin: + raise ValueError("gadget y interval must be nonempty and nonnegative") + if self.kind == GADGET_CROSSOVER: + if type(self.swap_row) is not int or self.swap_row < 0: + raise ValueError("crossover gadget must identify its swap row") + if self.x_end - self.x_begin != self.swap_row + 1: + raise ValueError("crossover width must equal swap_row + 1") + elif self.swap_row is not None: + raise ValueError("only crossover gadgets can identify a swap row") + + +@dataclass(frozen=True, slots=True) +class ReductionExplanation: + """Copied provenance with no native pointers or rendering metadata.""" + + variable_count: int + width: int + height: int + source_signals: tuple[ReductionSignal, ...] + target_signals: tuple[ReductionSignal, ...] + gadgets: tuple[ReductionGadget, ...] + + def __post_init__(self) -> None: + if type(self.variable_count) is not int or self.variable_count <= 0: + raise ValueError("variable_count must be a positive integer") + if type(self.width) is not int or self.width <= 0: + raise ValueError("width must be a positive integer") + if type(self.height) is not int or self.height <= 0: + raise ValueError("height must be a positive integer") + if type(self.source_signals) is not tuple: + raise TypeError("source_signals must be a tuple") + if type(self.target_signals) is not tuple: + raise TypeError("target_signals must be a tuple") + if type(self.gadgets) is not tuple: + raise TypeError("gadgets must be a tuple") + if self.height != 4 * self.variable_count - 1: + raise ValueError("signal height must equal 4 * variable_count - 1") + if len(self.source_signals) != self.height: + raise ValueError("source signal count must equal the region height") + if len(self.target_signals) != self.height: + raise ValueError("target signal count must equal the region height") + + source_ids = self._validate_signal_sequence( + self.source_signals, + "source", + ) + target_ids = self._validate_signal_sequence( + self.target_signals, + "target", + ) + if source_ids != target_ids: + raise ValueError("source and target must contain the same signal tokens") + + for gadget in self.gadgets: + if type(gadget) is not ReductionGadget: + raise TypeError("gadgets must contain ReductionGadget values") + if gadget.x_end > self.width or gadget.y_end > self.height: + raise ValueError("gadget rectangle must lie inside the region bounds") + + crossovers = tuple( + gadget + for gadget in self.gadgets + if gadget.kind == GADGET_CROSSOVER + ) + if tuple(gadget.ordinal for gadget in crossovers) != tuple( + range(len(crossovers)) + ): + raise ValueError("crossover ordinals must be contiguous and ordered") + replay = [signal.identity for signal in self.source_signals] + for gadget in crossovers: + swap_row = gadget.swap_row + if swap_row is None: + raise ValueError("crossover gadget is missing its swap row") + if swap_row >= self.height - 1: + raise ValueError("crossover swap row lies outside the signal rows") + replay[swap_row], replay[swap_row + 1] = ( + replay[swap_row + 1], + replay[swap_row], + ) + if tuple(replay) != tuple( + signal.identity for signal in self.target_signals + ): + raise ValueError("crossover program does not produce target signals") + + self._validate_gadget_population(GADGET_VARIABLE, self.variable_count) + self._validate_gadget_population(GADGET_CLAUSE, self.variable_count) + self._validate_gadget_population(GADGET_LEFT_FORWARD, 1) + self._validate_gadget_population(GADGET_RIGHT_FORWARD, 1) + + def _validate_signal_sequence( + self, + signals: tuple[ReductionSignal, ...], + label: str, + ) -> frozenset[tuple[str, int, int | None, int | None]]: + identities: set[tuple[str, int, int | None, int | None]] = set() + token_ids: set[int] = set() + occurrences: list[set[int]] = [set() for _ in range(self.variable_count)] + redundant = 0 + for row, signal in enumerate(signals): + if type(signal) is not ReductionSignal: + raise TypeError(f"{label} signals must contain ReductionSignal values") + if signal.row != row: + raise ValueError(f"{label} signal rows must be contiguous and ordered") + if signal.identity in identities: + raise ValueError(f"{label} signal tokens must be unique") + if signal.token_id in token_ids: + raise ValueError(f"{label} signal token IDs must be unique") + identities.add(signal.identity) + token_ids.add(signal.token_id) + if signal.kind == SIGNAL_VARIABLE: + variable = signal.variable + occurrence = signal.occurrence + if variable is None or occurrence is None: + raise ValueError(f"{label} variable signal lacks an identity") + if variable >= self.variable_count: + raise ValueError(f"{label} signal variable is outside the formula") + occurrences[variable].add(occurrence) + else: + redundant += 1 + if any(values != {0, 1, 2} for values in occurrences): + raise ValueError( + f"{label} must contain occurrences 0, 1, and 2 per variable" + ) + if redundant != self.variable_count - 1: + raise ValueError(f"{label} has an invalid redundant signal count") + return frozenset(identities) + + def _validate_gadget_population(self, kind: str, expected: int) -> None: + gadgets = tuple(gadget for gadget in self.gadgets if gadget.kind == kind) + if len(gadgets) != expected: + raise ValueError(f"expected {expected} {kind} gadgets") + if tuple(gadget.ordinal for gadget in gadgets) != tuple(range(expected)): + raise ValueError(f"{kind} gadget ordinals must be contiguous and ordered") diff --git a/python/native/reduction_adapter.py b/python/native/reduction_adapter.py index 52bbb54..bc60ef9 100644 --- a/python/native/reduction_adapter.py +++ b/python/native/reduction_adapter.py @@ -1,9 +1,10 @@ """Coordinate one native parse into Python formula and region models.""" from model.formula import Formula +from model.reduction_explanation import ReductionExplanation from model.region import Region from native.formula_adapter import PathLike, _copy_formula, _loaded_formula -from native.region_adapter import _build_region +from native.region_adapter import _build_region, _build_region_and_explanation def load_formula_and_region(path: PathLike) -> tuple[Formula, Region]: @@ -13,3 +14,14 @@ def load_formula_and_region(path: PathLike) -> tuple[Formula, Region]: formula = _copy_formula(native_formula) region = _build_region(native_formula) return formula, region + + +def load_formula_region_and_explanation( + path: PathLike, +) -> tuple[Formula, Region, ReductionExplanation]: + """Parse once and copy the native region with its actual provenance.""" + + with _loaded_formula(path) as native_formula: + formula = _copy_formula(native_formula) + region, explanation = _build_region_and_explanation(native_formula) + return formula, region, explanation diff --git a/python/native/region_adapter.py b/python/native/region_adapter.py index 50643ef..57a5383 100644 --- a/python/native/region_adapter.py +++ b/python/native/region_adapter.py @@ -7,15 +7,28 @@ Structure, byref, c_bool, + c_int, c_int32, c_size_t, + c_uint32, c_uint8, - c_void_p, ) from functools import cache from typing import Iterator from model.region import Region +from model.reduction_explanation import ( + GADGET_CLAUSE, + GADGET_CROSSOVER, + GADGET_LEFT_FORWARD, + GADGET_RIGHT_FORWARD, + GADGET_VARIABLE, + SIGNAL_REDUNDANT, + SIGNAL_VARIABLE, + ReductionExplanation, + ReductionGadget, + ReductionSignal, +) from native._lib import library from native.formula_adapter import _Cm13Formula @@ -39,14 +52,56 @@ class _Region(Structure): ] +class _AdjacentSwap(Structure): + _fields_ = [("row", c_uint32)] + + +class _SignalToken(Structure): + _fields_ = [ + ("kind", c_int), + ("token_id", c_uint32), + ("variable", c_uint32), + ("occurrence", c_uint8), + ] + + +class _ReductionGadgetSpan(Structure): + _fields_ = [ + ("kind", c_int), + ("ordinal", c_uint32), + ("x_begin", c_int32), + ("x_end", c_int32), + ("y_begin", c_int32), + ("y_end", c_int32), + ("swap_row", c_uint32), + ] + + +class _ReductionExplanation(Structure): + _fields_ = [ + ("source_signals", POINTER(_SignalToken)), + ("target_signals", POINTER(_SignalToken)), + ("signal_count", c_size_t), + ("gadgets", POINTER(_ReductionGadgetSpan)), + ("gadget_count", c_size_t), + ] + + class _YangZhangReduction(Structure): _fields_ = [ ("region", _Region), - ("swaps", c_void_p), + ("swaps", POINTER(_AdjacentSwap)), ("swap_count", c_size_t), ] +class _YangZhangExplainedReduction(Structure): + _fields_ = [ + ("reduction", _YangZhangReduction), + ("explanation", _ReductionExplanation), + ] + + class RegionBuildError(RuntimeError): """The native Yang–Zhang builder could not construct a region.""" @@ -59,10 +114,19 @@ def _region_library() -> CDLL: POINTER(_YangZhangReduction), ] lib.yang_zhang_build.restype = c_bool + lib.yang_zhang_build_explained.argtypes = [ + POINTER(_Cm13Formula), + POINTER(_YangZhangExplainedReduction), + ] + lib.yang_zhang_build_explained.restype = c_bool lib.yang_zhang_reduction_destroy.argtypes = [ POINTER(_YangZhangReduction) ] lib.yang_zhang_reduction_destroy.restype = None + lib.yang_zhang_explained_reduction_destroy.argtypes = [ + POINTER(_YangZhangExplainedReduction) + ] + lib.yang_zhang_explained_reduction_destroy.restype = None return lib @@ -100,6 +164,90 @@ def _copy_region(native_region: _Region) -> Region: ) +def _copy_signal(native_signal: _SignalToken, row: int) -> ReductionSignal: + kind = int(native_signal.kind) + if kind == 0: + return ReductionSignal( + row=row, + kind=SIGNAL_VARIABLE, + token_id=int(native_signal.token_id), + variable=int(native_signal.variable), + occurrence=int(native_signal.occurrence), + ) + if kind == 1: + return ReductionSignal( + row=row, + kind=SIGNAL_REDUNDANT, + token_id=int(native_signal.token_id), + variable=None, + occurrence=None, + ) + raise RuntimeError(f"native explanation contains unknown signal kind {kind}") + + +_GADGET_KINDS = { + 0: GADGET_VARIABLE, + 1: GADGET_LEFT_FORWARD, + 2: GADGET_CROSSOVER, + 3: GADGET_RIGHT_FORWARD, + 4: GADGET_CLAUSE, +} +_NO_SWAP_ROW = 2**32 - 1 + + +def _copy_gadget(native_gadget: _ReductionGadgetSpan) -> ReductionGadget: + kind_value = int(native_gadget.kind) + try: + kind = _GADGET_KINDS[kind_value] + except KeyError as error: + raise RuntimeError( + f"native explanation contains unknown gadget kind {kind_value}" + ) from error + swap_row_value = int(native_gadget.swap_row) + return ReductionGadget( + kind=kind, + ordinal=int(native_gadget.ordinal), + x_begin=int(native_gadget.x_begin), + x_end=int(native_gadget.x_end), + y_begin=int(native_gadget.y_begin), + y_end=int(native_gadget.y_end), + swap_row=None if swap_row_value == _NO_SWAP_ROW else swap_row_value, + ) + + +def _copy_reduction_explanation( + native_reduction: _YangZhangExplainedReduction, + variable_count: int, +) -> ReductionExplanation: + native = native_reduction.explanation + signal_count = int(native.signal_count) + gadget_count = int(native.gadget_count) + if signal_count <= 0 or not native.source_signals or not native.target_signals: + raise RuntimeError("invalid native reduction signal storage") + if gadget_count <= 0 or not native.gadgets: + raise RuntimeError("invalid native reduction gadget storage") + source = tuple( + _copy_signal(native.source_signals[row], row) + for row in range(signal_count) + ) + target = tuple( + _copy_signal(native.target_signals[row], row) + for row in range(signal_count) + ) + gadgets = tuple( + _copy_gadget(native.gadgets[index]) + for index in range(gadget_count) + ) + return ReductionExplanation( + variable_count=variable_count, + width=int(native_reduction.reduction.region.width), + height=int(native_reduction.reduction.region.height), + source_signals=source, + target_signals=target, + gadgets=gadgets, + ) + + @contextmanager def _built_reduction( native_formula: _Cm13Formula, @@ -117,6 +265,38 @@ def _built_reduction( lib.yang_zhang_reduction_destroy(byref(native_reduction)) +@contextmanager +def _built_explained_reduction( + native_formula: _Cm13Formula, +) -> Iterator[_YangZhangExplainedReduction]: + native_reduction = _YangZhangExplainedReduction() + lib = _region_library() + try: + if not lib.yang_zhang_build_explained( + byref(native_formula), + byref(native_reduction), + ): + raise RegionBuildError( + "could not build explained Yang-Zhang region" + ) + yield native_reduction + finally: + lib.yang_zhang_explained_reduction_destroy(byref(native_reduction)) + + def _build_region(native_formula: _Cm13Formula) -> Region: with _built_reduction(native_formula) as native_reduction: return _copy_region(native_reduction.region) + + +def _build_region_and_explanation( + native_formula: _Cm13Formula, +) -> tuple[Region, ReductionExplanation]: + with _built_explained_reduction(native_formula) as native_reduction: + return ( + _copy_region(native_reduction.reduction.region), + _copy_reduction_explanation( + native_reduction, + int(native_formula.variable_count), + ), + ) diff --git a/renderer/README.md b/renderer/README.md index 92edf95..8ca15be 100644 --- a/renderer/README.md +++ b/renderer/README.md @@ -118,6 +118,22 @@ square-to-hex reducer and checker before rasterization. Formula view rejects `--hex`; region view intentionally contains no assignment or partial solver state. +An opt-in `wang-explain-manifest-v2` adds the construction provenance produced +by the native Yang–Zhang builder. Render its exact source/target signals, +adjacent-swap gadget spans, formula, and unassigned region with: + +```bash +uv run --locked python wang_square.py \ + ../tests/fixtures/pipeline_sat_reduction_explain/manifest.json \ + output/reduction.png \ + --view reduction +``` + +Reduction spans describe the square construction itself, so this view rejects +`--hex`. The consumer verifies artifact hashes, formula and region identity, +the signal permutation, and gadget bounds without importing native code or +reconstructing builder geometry. + ## Input Format ### palette.json @@ -274,6 +290,7 @@ Raises `RenderingException` on pipeline errors. ├── test_data/ │ ├── wang_solution_v1_square_sat.png # Square golden for the Wang fixture │ ├── wang_solution_v1_hex_sat.png # Pointy-top hex golden for the same fixture +│ ├── pipeline_sat_reduction.png # Native reduction-provenance golden │ ├── palette_ok.json # Valid 16-color palette │ ├── palette_wrong_count.json # Only 3 colors (invalid) │ ├── palette_wrong_value.json # Component > 255 (invalid) @@ -289,8 +306,8 @@ Raises `RenderingException` on pipeline errors. uv run --locked pytest -q ``` -The complete isolated suite has 234 tests: the 144 preserved legacy tests -below, 45 Wang square tests, 24 square-to-hex/hex-raster tests, and 21 static +The complete isolated suite has 238 tests: the 144 preserved legacy tests +below, 45 Wang square tests, 24 square-to-hex/hex-raster tests, and 25 static snapshot/explainability tests. To run only the original upstream suite: diff --git a/renderer/UPSTREAM.md b/renderer/UPSTREAM.md index c488675..0405b2f 100644 --- a/renderer/UPSTREAM.md +++ b/renderer/UPSTREAM.md @@ -24,9 +24,10 @@ not an upstream file. Tiling Foundry later added its isolated Wang modules, tests, and goldens under `test_data/`, plus clearly separated usage notes in `README.md`. The default and explainable solution paths consume `wang-solution-v1`; the static formula, -tile-sheet, and unassigned-region views consume a hash-bound explainability -manifest. These additions do not modify or import the legacy PAP modules. They -also leave `pyproject.toml`, `uv.lock`, and the pinned dependencies unchanged. +tile-sheet, unassigned-region, and native reduction-provenance views consume +hash-bound explainability manifests. These additions do not modify or import +the legacy PAP modules. They also leave `pyproject.toml`, `uv.lock`, and the +pinned dependencies unchanged. ## Verification @@ -43,8 +44,8 @@ uv run --locked pytest -q ``` The import baseline remains 144 collected tests and 144 passing tests. The -combined local suite is 234 tests: 144 preserved legacy tests, 45 Wang square -tests, 24 square-to-hex/hex-raster tests, and 21 static +combined local suite is 238 tests: 144 preserved legacy tests, 45 Wang square +tests, 24 square-to-hex/hex-raster tests, and 25 static snapshot/explainability tests. Keep the renderer environment under `renderer/.venv`; its local `.gitignore` excludes that environment and generated Python/build files. diff --git a/renderer/test_data/pipeline_sat_reduction.png b/renderer/test_data/pipeline_sat_reduction.png new file mode 100644 index 0000000..0000a6c Binary files /dev/null and b/renderer/test_data/pipeline_sat_reduction.png differ diff --git a/renderer/test_wang_snapshot.py b/renderer/test_wang_snapshot.py index 3bcd880..75a2ba5 100644 --- a/renderer/test_wang_snapshot.py +++ b/renderer/test_wang_snapshot.py @@ -27,6 +27,8 @@ from wang_snapshot import ( FORMULA_SCHEMA, MANIFEST_SCHEMA, + REDUCTION_MANIFEST_SCHEMA, + REDUCTION_SCHEMA, REGION_SCHEMA, TILESET_SCHEMA, load_explainability_bundle, @@ -44,6 +46,11 @@ SOLUTION = ROOT / "tests/fixtures/wang_solution_v1_square_sat.json" SNAPSHOT_DIRECTORY = ROOT / "tests/fixtures/pipeline_sat_explain" MANIFEST = SNAPSHOT_DIRECTORY / "manifest.json" +REDUCTION_SNAPSHOT_DIRECTORY = ( + ROOT / "tests/fixtures/pipeline_sat_reduction_explain" +) +REDUCTION_MANIFEST = REDUCTION_SNAPSHOT_DIRECTORY / "manifest.json" +REDUCTION_GOLDEN = RENDERER_DIR / "test_data/pipeline_sat_reduction.png" GOLDENS = { ("formula", False): RENDERER_DIR / "test_data/pipeline_sat_formula.png", ("tileset", False): RENDERER_DIR / "test_data/pipeline_sat_tileset_square.png", @@ -85,6 +92,34 @@ def test_versioned_fixture_manifest_references_expected_closed_contracts(): assert hashlib.sha256(encoded).hexdigest() == reference["sha256"] +def test_loads_native_reduction_provenance_without_native_imports(): + bundle = load_explainability_bundle(REDUCTION_MANIFEST) + + assert bundle.reduction is not None + assert bundle.reduction.variable_count == 3 + assert (bundle.reduction.width, bundle.reduction.height) == (41, 11) + assert tuple( + signal.token_id for signal in bundle.reduction.source_signals + ) == (0, 1, 2, 9, 3, 4, 5, 10, 6, 7, 8) + assert tuple( + gadget.swap_row + for gadget in bundle.reduction.gadgets + if gadget.kind == "crossover" + ) == (3, 2, 3, 7, 6, 7) + assert "native._lib" not in sys.modules + + +def test_v2_manifest_references_the_closed_reduction_contract(): + manifest = json.loads(REDUCTION_MANIFEST.read_text(encoding="utf-8")) + + assert manifest["schema"] == REDUCTION_MANIFEST_SCHEMA + assert manifest["stage"] == "reduction" + assert manifest["artifacts"]["reduction"]["schema"] == REDUCTION_SCHEMA + for reference in manifest["artifacts"].values(): + encoded = (REDUCTION_SNAPSHOT_DIRECTORY / reference["path"]).read_bytes() + assert hashlib.sha256(encoded).hexdigest() == reference["sha256"] + + @pytest.mark.parametrize("view", ["tileset", "region"]) def test_hex_snapshot_views_require_the_independent_port_checker( tmp_path, @@ -197,6 +232,20 @@ def test_snapshot_views_match_pixel_stable_goldens(tmp_path, view, hex_mode): assert output.read_bytes() == GOLDENS[(view, hex_mode)].read_bytes() +def test_reduction_view_matches_native_provenance_golden(tmp_path): + output = tmp_path / "reduction.png" + + render_pipeline_snapshot( + REDUCTION_MANIFEST, + output, + view="reduction", + ) + + assert output.read_bytes() == REDUCTION_GOLDEN.read_bytes() + with Image.open(output) as image: + assert image.mode == "RGB" + + @pytest.mark.parametrize("hex_mode", (False, True)) def test_solution_explain_views_match_separate_goldens(tmp_path, hex_mode): output = tmp_path / "render.png" @@ -269,6 +318,22 @@ def test_formula_view_rejects_hex_and_unknown_snapshot_view(tmp_path): ) +def test_reduction_view_requires_v2_and_rejects_hex(tmp_path): + with pytest.raises(WangSquareRenderError, match="requires a.*v2"): + render_pipeline_snapshot( + MANIFEST, + tmp_path / "reduction.png", + view="reduction", + ) + with pytest.raises(WangSquareRenderError, match="not meaningful"): + render_pipeline_snapshot( + REDUCTION_MANIFEST, + tmp_path / "reduction-hex.png", + view="reduction", + hex_mode=True, + ) + + def test_cli_dispatches_snapshot_view_and_explain_solution(tmp_path): snapshot_output = tmp_path / "snapshot.png" wang_square.main( @@ -280,6 +345,12 @@ def test_cli_dispatches_snapshot_view_and_explain_solution(tmp_path): wang_square.main([str(SOLUTION), str(solution_output), "--explain"]) assert solution_output.read_bytes() == SOLUTION_GOLDENS[False].read_bytes() + reduction_output = tmp_path / "reduction.png" + wang_square.main( + [str(REDUCTION_MANIFEST), str(reduction_output), "--view", "reduction"] + ) + assert reduction_output.read_bytes() == REDUCTION_GOLDEN.read_bytes() + def test_snapshot_consumer_imports_in_isolated_renderer_process(): script = f""" diff --git a/renderer/wang_snapshot.py b/renderer/wang_snapshot.py index d88cab1..7130258 100644 --- a/renderer/wang_snapshot.py +++ b/renderer/wang_snapshot.py @@ -56,6 +56,8 @@ TILESET_SCHEMA: Final = "wang-tileset-snapshot-v1" REGION_SCHEMA: Final = "wang-region-snapshot-v1" MANIFEST_SCHEMA: Final = "wang-explain-manifest-v1" +REDUCTION_SCHEMA: Final = "wang-reduction-explanation-v1" +REDUCTION_MANIFEST_SCHEMA: Final = "wang-explain-manifest-v2" DIRECTIONS: Final = ("N", "E", "S", "W") HEX_DIRECTIONS: Final = ("E", "SE", "SW", "W", "NW", "NE") _SHA256_PATTERN: Final = re.compile(r"[0-9a-f]{64}") @@ -63,6 +65,10 @@ _LEGEND_WIDTH: Final = 190 _PANEL_GAP: Final = 20 _HEADER_HEIGHT: Final = 58 +_SIGNAL_KINDS: Final = frozenset({"variable", "redundant"}) +_GADGET_KINDS: Final = frozenset( + {"variable", "left_forward", "crossover", "right_forward", "clause"} +) @dataclass(frozen=True, slots=True) @@ -101,12 +107,49 @@ def height(self) -> int: return self.max_y - self.min_y + 1 +@dataclass(frozen=True, slots=True) +class ReductionSignalSnapshot: + row: int + kind: str + token_id: int + variable: int | None + occurrence: int | None + + @property + def identity(self) -> tuple[str, int, int | None, int | None]: + return (self.kind, self.token_id, self.variable, self.occurrence) + + +@dataclass(frozen=True, slots=True) +class ReductionGadgetSnapshot: + kind: str + ordinal: int + x_begin: int + x_end: int + y_begin: int + y_end: int + swap_row: int | None + + +@dataclass(frozen=True, slots=True) +class ReductionExplanationSnapshot: + source_formula_sha256: str + region_sha256: str + variable_count: int + width: int + height: int + source_signals: tuple[ReductionSignalSnapshot, ...] + target_signals: tuple[ReductionSignalSnapshot, ...] + gadgets: tuple[ReductionGadgetSnapshot, ...] + + @dataclass(frozen=True, slots=True) class ExplainabilityBundle: source_formula_sha256: str formula: FormulaSnapshot tileset: TilesetSnapshot region: RegionSnapshot + reduction: ReductionExplanationSnapshot | None = None def _fail(path: str, message: str) -> None: @@ -453,8 +496,247 @@ def _parse_region(document: dict[str, object]) -> RegionSnapshot: ) +def _parse_reduction_signal( + value: object, + path: str, + expected_row: int, + variable_count: int, +) -> ReductionSignalSnapshot: + signal = _object(value, path) + _fields( + signal, + frozenset({"row", "kind", "token_id", "variable", "occurrence"}), + path, + ) + row = _integer(signal["row"], f"{path}.row", nonnegative=True) + if row != expected_row: + _fail(f"{path}.row", f"must equal canonical row {expected_row}") + kind = _string(signal["kind"], f"{path}.kind") + if kind not in _SIGNAL_KINDS: + _fail(f"{path}.kind", "is not a supported signal kind") + token_id = _integer( + signal["token_id"], + f"{path}.token_id", + nonnegative=True, + ) + if kind == "variable": + variable = _integer( + signal["variable"], + f"{path}.variable", + nonnegative=True, + ) + occurrence = _integer( + signal["occurrence"], + f"{path}.occurrence", + nonnegative=True, + ) + if variable >= variable_count or occurrence >= 3: + _fail(path, "variable identity is outside the formula") + else: + if signal["variable"] is not None or signal["occurrence"] is not None: + _fail(path, "redundant signal metadata must be null") + variable = None + occurrence = None + return ReductionSignalSnapshot( + row=row, + kind=kind, + token_id=token_id, + variable=variable, + occurrence=occurrence, + ) + + +def _parse_reduction(document: dict[str, object]) -> ReductionExplanationSnapshot: + _fields( + document, + frozenset( + { + "schema", + "geometry", + "source_formula_sha256", + "region_sha256", + "variable_count", + "bounds", + "signals", + "gadgets", + } + ), + "reduction $", + ) + _literal(document["schema"], REDUCTION_SCHEMA, "reduction $.schema") + _literal(document["geometry"], "square", "reduction $.geometry") + source_digest = _sha256( + document["source_formula_sha256"], + "reduction $.source_formula_sha256", + ) + region_digest = _sha256( + document["region_sha256"], + "reduction $.region_sha256", + ) + variable_count = _integer( + document["variable_count"], + "reduction $.variable_count", + nonnegative=True, + ) + if variable_count == 0: + _fail("reduction $.variable_count", "must be positive") + bounds = _object(document["bounds"], "reduction $.bounds") + _fields( + bounds, + frozenset({"x_begin", "x_end", "y_begin", "y_end"}), + "reduction $.bounds", + ) + x_begin = _integer( + bounds["x_begin"], + "reduction $.bounds.x_begin", + nonnegative=True, + ) + width = _integer( + bounds["x_end"], + "reduction $.bounds.x_end", + nonnegative=True, + ) + y_begin = _integer( + bounds["y_begin"], + "reduction $.bounds.y_begin", + nonnegative=True, + ) + height = _integer( + bounds["y_end"], + "reduction $.bounds.y_end", + nonnegative=True, + ) + if x_begin != 0 or y_begin != 0 or width <= 0: + _fail("reduction $.bounds", "must be a nonempty zero-origin box") + if height != 4 * variable_count - 1: + _fail("reduction $.bounds.y_end", "does not match variable_count") + + signals = _object(document["signals"], "reduction $.signals") + _fields(signals, frozenset({"source", "target"}), "reduction $.signals") + projected_signals: list[tuple[ReductionSignalSnapshot, ...]] = [] + for name in ("source", "target"): + raw_sequence = _array(signals[name], f"reduction $.signals.{name}") + if len(raw_sequence) != height: + _fail(f"reduction $.signals.{name}", "length must equal height") + sequence = tuple( + _parse_reduction_signal( + raw_signal, + f"reduction $.signals.{name}[{row}]", + row, + variable_count, + ) + for row, raw_signal in enumerate(raw_sequence) + ) + if len({signal.token_id for signal in sequence}) != height: + _fail(f"reduction $.signals.{name}", "token IDs must be unique") + projected_signals.append(sequence) + source, target = projected_signals + if {signal.identity for signal in source} != { + signal.identity for signal in target + }: + _fail("reduction $.signals", "source and target tokens must match") + + raw_gadgets = _array(document["gadgets"], "reduction $.gadgets") + gadgets: list[ReductionGadgetSnapshot] = [] + populations: dict[str, list[int]] = {kind: [] for kind in _GADGET_KINDS} + for index, raw_gadget in enumerate(raw_gadgets): + path = f"reduction $.gadgets[{index}]" + gadget = _object(raw_gadget, path) + _fields( + gadget, + frozenset({"kind", "ordinal", "bounds", "swap_row"}), + path, + ) + kind = _string(gadget["kind"], f"{path}.kind") + if kind not in _GADGET_KINDS: + _fail(f"{path}.kind", "is not a supported gadget kind") + ordinal = _integer( + gadget["ordinal"], + f"{path}.ordinal", + nonnegative=True, + ) + populations[kind].append(ordinal) + raw_bounds = _object(gadget["bounds"], f"{path}.bounds") + _fields( + raw_bounds, + frozenset({"x_begin", "x_end", "y_begin", "y_end"}), + f"{path}.bounds", + ) + coordinates = tuple( + _integer( + raw_bounds[name], + f"{path}.bounds.{name}", + nonnegative=True, + ) + for name in ("x_begin", "x_end", "y_begin", "y_end") + ) + gx_begin, gx_end, gy_begin, gy_end = coordinates + if gx_end <= gx_begin or gy_end <= gy_begin: + _fail(f"{path}.bounds", "must be a nonempty half-open rectangle") + if gx_end > width or gy_end > height: + _fail(f"{path}.bounds", "lies outside the reduction bounds") + if kind == "crossover": + swap_row = _integer( + gadget["swap_row"], + f"{path}.swap_row", + nonnegative=True, + ) + if swap_row >= height - 1 or gx_end - gx_begin != swap_row + 1: + _fail(path, "crossover row or width is inconsistent") + else: + if gadget["swap_row"] is not None: + _fail(f"{path}.swap_row", "must be null outside crossovers") + swap_row = None + gadgets.append( + ReductionGadgetSnapshot( + kind, + ordinal, + gx_begin, + gx_end, + gy_begin, + gy_end, + swap_row, + ) + ) + expected_counts = { + "variable": variable_count, + "left_forward": 1, + "right_forward": 1, + "clause": variable_count, + } + for kind, count in expected_counts.items(): + if populations[kind] != list(range(count)): + _fail("reduction $.gadgets", f"invalid {kind} gadget ordinals") + crossovers = tuple(gadget for gadget in gadgets if gadget.kind == "crossover") + if tuple(gadget.ordinal for gadget in crossovers) != tuple( + range(len(crossovers)) + ): + _fail("reduction $.gadgets", "invalid crossover gadget ordinals") + replay = [signal.identity for signal in source] + for crossover in crossovers: + swap_row = crossover.swap_row + if swap_row is None: + _fail("reduction $.gadgets", "crossover is missing its swap row") + replay[swap_row], replay[swap_row + 1] = ( + replay[swap_row + 1], + replay[swap_row], + ) + if tuple(replay) != tuple(signal.identity for signal in target): + _fail("reduction $.gadgets", "crossover replay does not reach target") + return ReductionExplanationSnapshot( + source_formula_sha256=source_digest, + region_sha256=region_digest, + variable_count=variable_count, + width=width, + height=height, + source_signals=source, + target_signals=target, + gadgets=tuple(gadgets), + ) + + def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: - """Load one manifest, verify hashes, and project its three artifacts.""" + """Load a v1/v2 manifest and independently verify every referenced stage.""" manifest_path = Path(path) manifest = _load_json_bytes( _read_bytes(manifest_path, "manifest"), @@ -465,20 +747,32 @@ def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: frozenset({"schema", "stage", "source_formula_sha256", "artifacts"}), "$", ) - _literal(manifest["schema"], MANIFEST_SCHEMA, "$.schema") - _literal(manifest["stage"], "region", "$.stage") + manifest_schema = _string(manifest["schema"], "$.schema") + if manifest_schema == MANIFEST_SCHEMA: + _literal(manifest["stage"], "region", "$.stage") + expected_schemas = { + "formula": FORMULA_SCHEMA, + "tileset": TILESET_SCHEMA, + "region": REGION_SCHEMA, + } + elif manifest_schema == REDUCTION_MANIFEST_SCHEMA: + _literal(manifest["stage"], "reduction", "$.stage") + expected_schemas = { + "formula": FORMULA_SCHEMA, + "tileset": TILESET_SCHEMA, + "region": REGION_SCHEMA, + "reduction": REDUCTION_SCHEMA, + } + else: + _fail("$.schema", "must be a supported explainability manifest") source_digest = _sha256( manifest["source_formula_sha256"], "$.source_formula_sha256", ) artifacts = _object(manifest["artifacts"], "$.artifacts") - _fields(artifacts, frozenset({"formula", "tileset", "region"}), "$.artifacts") - expected_schemas = { - "formula": FORMULA_SCHEMA, - "tileset": TILESET_SCHEMA, - "region": REGION_SCHEMA, - } + _fields(artifacts, frozenset(expected_schemas), "$.artifacts") documents: dict[str, dict[str, object]] = {} + artifact_digests: dict[str, str] = {} for name, expected_schema in expected_schemas.items(): reference_path = f"$.artifacts.{name}" reference = _object(artifacts[name], reference_path) @@ -494,6 +788,7 @@ def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: if hashlib.sha256(encoded).hexdigest() != expected_digest: _fail(f"{reference_path}.sha256", f"does not match {artifact_name}") documents[name] = _load_json_bytes(encoded, str(artifact_path)) + artifact_digests[name] = expected_digest formula = _parse_formula(documents["formula"]) tileset = _parse_tileset(documents["tileset"]) @@ -502,6 +797,62 @@ def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: _fail("$.source_formula_sha256", "does not match formula snapshot") if region.source_formula_sha256 != source_digest: _fail("$.source_formula_sha256", "does not match region snapshot") + reduction: ReductionExplanationSnapshot | None = None + if "reduction" in documents: + reduction = _parse_reduction(documents["reduction"]) + if reduction.source_formula_sha256 != source_digest: + _fail("reduction $.source_formula_sha256", "does not match formula") + if reduction.region_sha256 != artifact_digests["region"]: + _fail("reduction $.region_sha256", "does not match region artifact") + if reduction.variable_count != formula.variable_count: + _fail("reduction $.variable_count", "does not match formula") + if (reduction.width, reduction.height) != (region.width, region.height): + _fail("reduction $.bounds", "does not match region dimensions") + expected_source: list[ + tuple[str, int, int | None, int | None] + ] = [] + for variable in range(formula.variable_count): + expected_source.extend( + ("variable", 3 * variable + occurrence, variable, occurrence) + for occurrence in range(3) + ) + if variable + 1 < formula.variable_count: + expected_source.append( + ( + "redundant", + 3 * formula.variable_count + variable, + None, + None, + ) + ) + expected_target: list[ + tuple[str, int, int | None, int | None] + ] = [] + next_occurrence = [0] * formula.variable_count + for clause_id, clause in enumerate(formula.clauses): + for variable in clause: + occurrence = next_occurrence[variable] + next_occurrence[variable] += 1 + expected_target.append( + ("variable", 3 * variable + occurrence, variable, occurrence) + ) + if clause_id + 1 < formula.variable_count: + expected_target.append( + ( + "redundant", + 3 * formula.variable_count + clause_id, + None, + None, + ) + ) + if tuple(expected_source) != tuple( + signal.identity for signal in reduction.source_signals + ): + _fail("reduction $.signals.source", "does not match formula") + if tuple(expected_target) != tuple( + signal.identity for signal in reduction.target_signals + ): + _fail("reduction $.signals.target", "does not match formula") colors = set(tileset.colors) for index, sides in enumerate(region.boundary): if sides is None: @@ -517,6 +868,7 @@ def load_explainability_bundle(path: str | Path) -> ExplainabilityBundle: formula=formula, tileset=tileset, region=region, + reduction=reduction, ) @@ -950,6 +1302,175 @@ def _compose_region_hex( return np.asarray(canvas, dtype=np.uint8) +def _signal_label(signal: ReductionSignalSnapshot) -> str: + if signal.kind == "redundant": + return f"r#{signal.token_id}" + return f"x{signal.variable}.{signal.occurrence}#{signal.token_id}" + + +def _compose_reduction( + bundle: ExplainabilityBundle, + pixels_per_cell: int, + margin: int, +) -> np.ndarray: + """Compose native gadget spans and signal routing over the built region.""" + reduction = bundle.reduction + if reduction is None: + raise WangSquareRenderError( + "reduction view requires a wang-explain-manifest-v2 bundle" + ) + ppc = _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, + ) + region = bundle.region + left_labels = 104 + right_labels = 150 + grid_width = region.width * ppc + grid_height = region.height * ppc + side_width = max(_FORMULA_PANEL_WIDTH, _LEGEND_WIDTH) + grid_x = checked_margin + left_labels + grid_y = checked_margin + _HEADER_HEIGHT + side_x = grid_x + grid_width + right_labels + _PANEL_GAP + width = side_x + side_width + checked_margin + palette = _palette(bundle) + formula_height = 30 + len(_formula_lines(bundle.formula)) * 20 + legend_rows = (len(palette) + 1) // 2 + side_height = formula_height + 160 + legend_rows * 22 + height = max( + grid_y + grid_height + checked_margin, + grid_y + side_height + checked_margin, + ) + _check_canvas_limits(width, height) + canvas = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB) + draw = ImageDraw.Draw(canvas) + draw_explain_heading( + draw, + (checked_margin, checked_margin), + title="Yang-Zhang reduction - native construction provenance", + subtitle=( + "half-open gadget spans and the exact source-to-clause " + "permutation; no tile is assigned" + ), + ) + + inactive = square_inactive_tile(ppc) + for index, active in enumerate(region.active): + x = grid_x + (index % region.width) * ppc + y = grid_y + (index // region.width) * ppc + if not active: + canvas.paste(inactive, (x, y)) + continue + sides = region.boundary[index] + if sides is None: + _fail("region", "active cell is missing its boundary entry") + canvas.paste(square_region_tile(ppc, sides, palette), (x, y)) + + font = explain_font(10) + for row, (source, target) in enumerate( + zip(reduction.source_signals, reduction.target_signals, strict=True) + ): + text_y = grid_y + row * ppc + max(1, (ppc - 12) // 2) + draw.text( + (checked_margin, text_y), + _signal_label(source), + font=font, + fill=EXPLAIN_TEXT_RGB, + ) + if row % 4 < 3: + destination = f"c{row // 4}[{row % 4}]" + else: + destination = "gap" + draw.text( + (grid_x + grid_width + 8, text_y), + f"{destination} <- {_signal_label(target)}", + font=font, + fill=EXPLAIN_TEXT_RGB, + ) + + gadget_colors = { + "variable": (37, 99, 235), + "left_forward": (5, 150, 105), + "crossover": (217, 119, 6), + "right_forward": (8, 145, 178), + "clause": (220, 38, 38), + } + for gadget in reduction.gadgets: + color = gadget_colors[gadget.kind] + x0 = grid_x + gadget.x_begin * ppc + y0 = grid_y + gadget.y_begin * ppc + x1 = grid_x + gadget.x_end * ppc - 1 + y1 = grid_y + gadget.y_end * ppc - 1 + draw.rectangle((x0, y0, x1, y1), outline=color, width=3) + if gadget.kind == "crossover": + label = f"X{gadget.ordinal}:s{gadget.swap_row}" + elif gadget.kind == "variable": + label = f"v{gadget.ordinal}" + elif gadget.kind == "clause": + label = f"c{gadget.ordinal}" + elif gadget.kind == "left_forward": + label = "F-in" + else: + label = "F-out" + draw.text( + (x0 + 3, y0 + 2), + label, + font=font, + fill=color, + stroke_width=2, + stroke_fill=EXPLAIN_PANEL_RGB, + ) + + formula_end = _formula_panel( + canvas, + bundle, + (side_x, grid_y), + height - checked_margin, + ) + legend_y = formula_end + 12 + draw.text( + (side_x, legend_y), + "Native gadget spans", + font=explain_font(15), + fill=EXPLAIN_TEXT_RGB, + ) + legend_y += 25 + for kind in ( + "variable", + "left_forward", + "crossover", + "right_forward", + "clause", + ): + draw.rectangle( + (side_x, legend_y + 2, side_x + 16, legend_y + 14), + outline=gadget_colors[kind], + width=3, + ) + draw.text( + (side_x + 24, legend_y), + kind.replace("_", " "), + font=explain_font(12), + fill=EXPLAIN_TEXT_RGB, + ) + legend_y += 20 + draw_palette_legend( + draw, + palette, + (side_x, legend_y + 8), + columns=2, + ) + return np.asarray(canvas, dtype=np.uint8) + + def render_pipeline_snapshot( input_path: str | Path, output_path: str | Path, @@ -977,8 +1498,14 @@ def render_pipeline_snapshot( canvas = _compose_region_hex(bundle, pixels_per_cell, margin) else: canvas = _compose_region_square(bundle, pixels_per_cell, margin) + elif view == "reduction": + if hex_mode: + raise WangSquareRenderError( + "--hex is not meaningful for square reduction provenance" + ) + canvas = _compose_reduction(bundle, pixels_per_cell, margin) else: raise WangSquareRenderError( - "snapshot view must be one of formula, tileset, or region" + "snapshot view must be one of formula, tileset, region, or reduction" ) _save_png_atomic(canvas, output_path) diff --git a/renderer/wang_square.py b/renderer/wang_square.py index 2567b34..dda119a 100644 --- a/renderer/wang_square.py +++ b/renderer/wang_square.py @@ -945,7 +945,9 @@ def _parser() -> argparse.ArgumentParser: ) parser.add_argument( "input", - help="path to wang-solution-v1 JSON or a wang-explain-manifest-v1 file", + help=( + "path to wang-solution-v1 JSON or a wang-explain-manifest-v1/v2 file" + ), ) parser.add_argument("output", help="path to the output PNG") parser.add_argument( @@ -975,7 +977,7 @@ def _parser() -> argparse.ArgumentParser: ) parser.add_argument( "--view", - choices=("solution", "formula", "tileset", "region"), + choices=("solution", "formula", "tileset", "region", "reduction"), default="solution", help="input stage to render (default: solution)", ) diff --git a/schemas/wang-explain-manifest-v2.schema.json b/schemas/wang-explain-manifest-v2.schema.json new file mode 100644 index 0000000..afb671c --- /dev/null +++ b/schemas/wang-explain-manifest-v2.schema.json @@ -0,0 +1,64 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "urn:tiling-foundry:schema:wang-explain-manifest-v2", + "title": "Tiling Foundry reduction explainability manifest v2", + "type": "object", + "additionalProperties": false, + "required": ["schema", "stage", "source_formula_sha256", "artifacts"], + "properties": { + "schema": {"const": "wang-explain-manifest-v2"}, + "stage": {"const": "reduction"}, + "source_formula_sha256": {"$ref": "#/$defs/sha256"}, + "artifacts": { + "type": "object", + "additionalProperties": false, + "required": ["formula", "tileset", "region", "reduction"], + "properties": { + "formula": {"$ref": "#/$defs/formula_reference"}, + "tileset": {"$ref": "#/$defs/tileset_reference"}, + "region": {"$ref": "#/$defs/region_reference"}, + "reduction": {"$ref": "#/$defs/reduction_reference"} + } + } + }, + "$defs": { + "sha256": { + "type": "string", + "pattern": "^[0-9a-f]{64}$" + }, + "artifact_path": { + "type": "string", + "minLength": 1, + "pattern": "^[^/\\]+$", + "not": {"enum": [".", ".."]} + }, + "formula_reference": { + "$ref": "#/$defs/reference", + "properties": {"schema": {"const": "cm13-formula-snapshot-v1"}} + }, + "tileset_reference": { + "$ref": "#/$defs/reference", + "properties": {"schema": {"const": "wang-tileset-snapshot-v1"}} + }, + "region_reference": { + "$ref": "#/$defs/reference", + "properties": {"schema": {"const": "wang-region-snapshot-v1"}} + }, + "reduction_reference": { + "$ref": "#/$defs/reference", + "properties": { + "schema": {"const": "wang-reduction-explanation-v1"} + } + }, + "reference": { + "type": "object", + "additionalProperties": false, + "required": ["path", "sha256", "schema"], + "properties": { + "path": {"$ref": "#/$defs/artifact_path"}, + "sha256": {"$ref": "#/$defs/sha256"}, + "schema": {"type": "string"} + } + } + } +} diff --git a/schemas/wang-reduction-explanation-v1.schema.json b/schemas/wang-reduction-explanation-v1.schema.json new file mode 100644 index 0000000..509ecd5 --- /dev/null +++ b/schemas/wang-reduction-explanation-v1.schema.json @@ -0,0 +1,119 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "urn:tiling-foundry:schema:wang-reduction-explanation-v1", + "title": "Tiling Foundry Yang-Zhang reduction explanation v1", + "type": "object", + "additionalProperties": false, + "required": [ + "schema", + "geometry", + "source_formula_sha256", + "region_sha256", + "variable_count", + "bounds", + "signals", + "gadgets" + ], + "properties": { + "schema": {"const": "wang-reduction-explanation-v1"}, + "geometry": {"const": "square"}, + "source_formula_sha256": {"$ref": "#/$defs/sha256"}, + "region_sha256": {"$ref": "#/$defs/sha256"}, + "variable_count": {"type": "integer", "minimum": 1}, + "bounds": {"$ref": "#/$defs/bounds"}, + "signals": { + "type": "object", + "additionalProperties": false, + "required": ["source", "target"], + "properties": { + "source": { + "type": "array", + "minItems": 3, + "items": {"$ref": "#/$defs/signal"} + }, + "target": { + "type": "array", + "minItems": 3, + "items": {"$ref": "#/$defs/signal"} + } + } + }, + "gadgets": { + "type": "array", + "minItems": 4, + "items": {"$ref": "#/$defs/gadget"} + } + }, + "$defs": { + "sha256": { + "type": "string", + "pattern": "^[0-9a-f]{64}$" + }, + "bounds": { + "type": "object", + "additionalProperties": false, + "required": ["x_begin", "x_end", "y_begin", "y_end"], + "properties": { + "x_begin": {"type": "integer", "minimum": 0}, + "x_end": {"type": "integer", "minimum": 1}, + "y_begin": {"type": "integer", "minimum": 0}, + "y_end": {"type": "integer", "minimum": 1} + } + }, + "signal": { + "type": "object", + "additionalProperties": false, + "required": ["row", "kind", "token_id", "variable", "occurrence"], + "properties": { + "row": {"type": "integer", "minimum": 0}, + "kind": {"enum": ["variable", "redundant"]}, + "token_id": {"type": "integer", "minimum": 0}, + "variable": {"type": ["integer", "null"], "minimum": 0}, + "occurrence": {"type": ["integer", "null"], "minimum": 0, "maximum": 2} + }, + "allOf": [ + { + "if": {"properties": {"kind": {"const": "variable"}}}, + "then": { + "properties": { + "variable": {"type": "integer"}, + "occurrence": {"type": "integer"} + } + }, + "else": { + "properties": { + "variable": {"type": "null"}, + "occurrence": {"type": "null"} + } + } + } + ] + }, + "gadget": { + "type": "object", + "additionalProperties": false, + "required": ["kind", "ordinal", "bounds", "swap_row"], + "properties": { + "kind": { + "enum": [ + "variable", + "left_forward", + "crossover", + "right_forward", + "clause" + ] + }, + "ordinal": {"type": "integer", "minimum": 0}, + "bounds": {"$ref": "#/$defs/bounds"}, + "swap_row": {"type": ["integer", "null"], "minimum": 0} + }, + "allOf": [ + { + "if": {"properties": {"kind": {"const": "crossover"}}}, + "then": {"properties": {"swap_row": {"type": "integer"}}}, + "else": {"properties": {"swap_row": {"type": "null"}}} + } + ] + } + } +} diff --git a/src/builder/yang_zhang.c b/src/builder/yang_zhang.c index dd9af91..e4b87e8 100644 --- a/src/builder/yang_zhang.c +++ b/src/builder/yang_zhang.c @@ -13,6 +13,140 @@ static bool reduction_is_destroyed(const YangZhangReduction *reduction) && reduction->swap_count == 0; } +static bool explanation_is_destroyed( + const ReductionExplanation *explanation +) +{ + return explanation != NULL + && explanation->source_signals == NULL + && explanation->target_signals == NULL + && explanation->signal_count == 0 + && explanation->gadgets == NULL + && explanation->gadget_count == 0; +} + +static bool build_reduction_explanation( + const Cm13Formula *formula, + SignalToken *source, + SignalToken *target, + size_t signal_count, + const AdjacentSwap *swaps, + size_t swap_count, + int32_t width, + int32_t height, + ReductionExplanation *out_explanation +) +{ + const size_t variable_count = formula->variable_count; + + if (variable_count > (SIZE_MAX - 2u) / 2u) { + return false; + } + + const size_t fixed_gadget_count = 2u * variable_count + 2u; + if (swap_count > SIZE_MAX - fixed_gadget_count) { + return false; + } + + const size_t gadget_count = fixed_gadget_count + swap_count; + if (gadget_count > SIZE_MAX / sizeof(*out_explanation->gadgets)) { + return false; + } + + ReductionGadgetSpan *gadgets = malloc( + gadget_count * sizeof(*gadgets) + ); + if (gadgets == NULL) { + return false; + } + + size_t gadget_index = 0; + for (uint32_t variable = 0; + variable < formula->variable_count; + ++variable) { + const int32_t first_y = (int32_t)(4u * variable); + gadgets[gadget_index++] = (ReductionGadgetSpan){ + .kind = REDUCTION_GADGET_VARIABLE, + .ordinal = variable, + .x_begin = 0, + .x_end = (int32_t)YANG_ZHANG_VARIABLE_WIDTH, + .y_begin = first_y, + .y_end = first_y + 3, + .swap_row = REDUCTION_NO_SWAP_ROW + }; + } + + const int32_t left_begin = (int32_t)YANG_ZHANG_VARIABLE_WIDTH; + const int32_t crossover_begin = left_begin + + (int32_t)YANG_ZHANG_LEFT_FORWARD_WIDTH; + gadgets[gadget_index++] = (ReductionGadgetSpan){ + .kind = REDUCTION_GADGET_LEFT_FORWARD, + .ordinal = 0, + .x_begin = left_begin, + .x_end = crossover_begin, + .y_begin = 0, + .y_end = height, + .swap_row = REDUCTION_NO_SWAP_ROW + }; + + int32_t block_x = crossover_begin; + for (size_t swap = 0; swap < swap_count; ++swap) { + const int32_t block_width = (int32_t)swaps[swap].row + 1; + gadgets[gadget_index++] = (ReductionGadgetSpan){ + .kind = REDUCTION_GADGET_CROSSOVER, + .ordinal = (uint32_t)swap, + .x_begin = block_x, + .x_end = block_x + block_width, + .y_begin = 0, + .y_end = height, + .swap_row = swaps[swap].row + }; + block_x += block_width; + } + + const int32_t right_end = block_x + + (int32_t)YANG_ZHANG_RIGHT_FORWARD_WIDTH; + gadgets[gadget_index++] = (ReductionGadgetSpan){ + .kind = REDUCTION_GADGET_RIGHT_FORWARD, + .ordinal = 0, + .x_begin = block_x, + .x_end = right_end, + .y_begin = 0, + .y_end = height, + .swap_row = REDUCTION_NO_SWAP_ROW + }; + + for (size_t clause = 0; clause < formula->clause_count; ++clause) { + const int32_t first_y = (int32_t)(4u * clause); + const int32_t y_end = clause + 1u < formula->clause_count + ? first_y + 4 + : height; + gadgets[gadget_index++] = (ReductionGadgetSpan){ + .kind = REDUCTION_GADGET_CLAUSE, + .ordinal = (uint32_t)clause, + .x_begin = right_end, + .x_end = width, + .y_begin = first_y, + .y_end = y_end, + .swap_row = REDUCTION_NO_SWAP_ROW + }; + } + + if (gadget_index != gadget_count) { + free(gadgets); + return false; + } + + *out_explanation = (ReductionExplanation){ + .source_signals = source, + .target_signals = target, + .signal_count = signal_count, + .gadgets = gadgets, + .gadget_count = gadget_count + }; + return true; +} + static bool formula_is_in_reduction_domain(const Cm13Formula *formula) { if (formula == NULL || @@ -312,9 +446,10 @@ static bool paint_crossover_boundaries( return true; } -bool yang_zhang_build( +static bool yang_zhang_build_internal( const Cm13Formula *formula, - YangZhangReduction *out_reduction + YangZhangReduction *out_reduction, + ReductionExplanation *out_explanation ) { SignalToken *source = NULL; @@ -325,8 +460,11 @@ bool yang_zhang_build( int32_t height = 0; int32_t width = 0; Region region = {0}; + ReductionExplanation explanation = {0}; if (!reduction_is_destroyed(out_reduction) || + (out_explanation != NULL && + !explanation_is_destroyed(out_explanation)) || !formula_is_in_reduction_domain(formula)) { return false; } @@ -349,8 +487,12 @@ bool yang_zhang_build( return false; } - free(target); - free(source); + if (out_explanation == NULL) { + free(target); + target = NULL; + free(source); + source = NULL; + } if (!yang_zhang_compute_dimensions( formula->variable_count, @@ -370,18 +512,57 @@ bool yang_zhang_build( YANG_ZHANG_LEFT_FORWARD_WIDTH), swaps, swap_count - )) { + ) || + (out_explanation != NULL && !build_reduction_explanation( + formula, + source, + target, + signal_count, + swaps, + swap_count, + width, + height, + &explanation + ))) { region_destroy(®ion); free(swaps); + free(target); + free(source); return false; } out_reduction->region = region; out_reduction->swaps = swaps; out_reduction->swap_count = swap_count; + if (out_explanation != NULL) { + *out_explanation = explanation; + } return true; } +bool yang_zhang_build( + const Cm13Formula *formula, + YangZhangReduction *out_reduction +) +{ + return yang_zhang_build_internal(formula, out_reduction, NULL); +} + +bool yang_zhang_build_explained( + const Cm13Formula *formula, + YangZhangExplainedReduction *out_reduction +) +{ + if (out_reduction == NULL) { + return false; + } + return yang_zhang_build_internal( + formula, + &out_reduction->reduction, + &out_reduction->explanation + ); +} + void yang_zhang_reduction_destroy(YangZhangReduction *reduction) { if (reduction == NULL) { @@ -394,6 +575,21 @@ void yang_zhang_reduction_destroy(YangZhangReduction *reduction) reduction->swap_count = 0; } +void yang_zhang_explained_reduction_destroy( + YangZhangExplainedReduction *reduction +) +{ + if (reduction == NULL) { + return; + } + + yang_zhang_reduction_destroy(&reduction->reduction); + free(reduction->explanation.gadgets); + free(reduction->explanation.target_signals); + free(reduction->explanation.source_signals); + reduction->explanation = (ReductionExplanation){0}; +} + bool yang_zhang_compute_dimensions( uint32_t variable_count, const AdjacentSwap *swaps, diff --git a/tests/c/test_yang_zhang.c b/tests/c/test_yang_zhang.c index d40ed62..5871bf8 100644 --- a/tests/c/test_yang_zhang.c +++ b/tests/c/test_yang_zhang.c @@ -8,6 +8,24 @@ #define ARRAY_COUNT(array) (sizeof(array) / sizeof((array)[0])) +typedef struct { + Region region; + AdjacentSwap *swaps; + size_t swap_count; +} LegacyYangZhangReduction; + +_Static_assert(sizeof(YangZhangReduction) == sizeof(LegacyYangZhangReduction), + "YangZhangReduction ABI size changed"); +_Static_assert(offsetof(YangZhangReduction, region) == + offsetof(LegacyYangZhangReduction, region), + "YangZhangReduction.region ABI offset changed"); +_Static_assert(offsetof(YangZhangReduction, swaps) == + offsetof(LegacyYangZhangReduction, swaps), + "YangZhangReduction.swaps ABI offset changed"); +_Static_assert(offsetof(YangZhangReduction, swap_count) == + offsetof(LegacyYangZhangReduction, swap_count), + "YangZhangReduction.swap_count ABI offset changed"); + static void test_reduction_destroy_accepts_null_and_empty(void) { YangZhangReduction reduction = {0}; @@ -32,7 +50,6 @@ static void test_reduction_destroy_releases_and_resets_owned_storage(void) reduction.swaps = malloc(2 * sizeof(*reduction.swaps)); assert(reduction.swaps != NULL); reduction.swap_count = 2; - yang_zhang_reduction_destroy(&reduction); assert(reduction.region.width == 0); @@ -41,11 +58,49 @@ static void test_reduction_destroy_releases_and_resets_owned_storage(void) assert(reduction.region.cells == NULL); assert(reduction.swaps == NULL); assert(reduction.swap_count == 0); - /* A destroyed reduction can be destroyed repeatedly. */ yang_zhang_reduction_destroy(&reduction); } +static void test_explained_reduction_destroy_releases_all_storage(void) +{ + YangZhangExplainedReduction explained = {0}; + + assert(region_init(&explained.reduction.region, 2, 3)); + explained.reduction.swaps = malloc( + 2 * sizeof(*explained.reduction.swaps) + ); + explained.explanation.source_signals = malloc( + 3 * sizeof(*explained.explanation.source_signals) + ); + explained.explanation.target_signals = malloc( + 3 * sizeof(*explained.explanation.target_signals) + ); + explained.explanation.gadgets = malloc( + 4 * sizeof(*explained.explanation.gadgets) + ); + assert(explained.reduction.swaps != NULL); + assert(explained.explanation.source_signals != NULL); + assert(explained.explanation.target_signals != NULL); + assert(explained.explanation.gadgets != NULL); + explained.reduction.swap_count = 2; + explained.explanation.signal_count = 3; + explained.explanation.gadget_count = 4; + + yang_zhang_explained_reduction_destroy(&explained); + + assert(explained.reduction.region.cells == NULL); + assert(explained.reduction.swaps == NULL); + assert(explained.reduction.swap_count == 0); + assert(explained.explanation.source_signals == NULL); + assert(explained.explanation.target_signals == NULL); + assert(explained.explanation.signal_count == 0); + assert(explained.explanation.gadgets == NULL); + assert(explained.explanation.gadget_count == 0); + yang_zhang_explained_reduction_destroy(&explained); + yang_zhang_explained_reduction_destroy(NULL); +} + static Cm13Formula one_variable_formula(Cm13Clause clauses[1]) { clauses[0] = (Cm13Clause){ .variable_index = { 0, 0, 0 } }; @@ -67,6 +122,18 @@ static void assert_reduction_destroyed(const YangZhangReduction *reduction) assert(reduction->swap_count == 0); } +static void assert_explained_reduction_destroyed( + const YangZhangExplainedReduction *reduction +) +{ + assert_reduction_destroyed(&reduction->reduction); + assert(reduction->explanation.source_signals == NULL); + assert(reduction->explanation.target_signals == NULL); + assert(reduction->explanation.signal_count == 0); + assert(reduction->explanation.gadgets == NULL); + assert(reduction->explanation.gadget_count == 0); +} + static ColorId expected_clause_color(int32_t y) { switch (y % 4) { @@ -193,6 +260,26 @@ static bool tokens_equal(const SignalToken *left, const SignalToken *right) left->occurrence == right->occurrence)); } +static void assert_gadget_span( + const ReductionGadgetSpan *gadget, + ReductionGadgetKind kind, + uint32_t ordinal, + int32_t x_begin, + int32_t x_end, + int32_t y_begin, + int32_t y_end, + uint32_t swap_row +) +{ + assert(gadget->kind == kind); + assert(gadget->ordinal == ordinal); + assert(gadget->x_begin == x_begin); + assert(gadget->x_end == x_end); + assert(gadget->y_begin == y_begin); + assert(gadget->y_end == y_end); + assert(gadget->swap_row == swap_row); +} + static void assert_build_rejected(const Cm13Formula *formula) { YangZhangReduction reduction = {0}; @@ -294,23 +381,104 @@ static void test_build_rejects_non_destroyed_output(void) assert(reduction.region.width == 1); } -static void test_build_minimal_valid_formula(void) +static void test_explained_build_rejects_non_destroyed_output(void) +{ + Cm13Clause clauses[1]; + Cm13Formula formula = one_variable_formula(clauses); + YangZhangExplainedReduction reduction = { + .explanation = { .signal_count = 1 } + }; + + assert(!yang_zhang_build_explained(&formula, &reduction)); + assert_reduction_destroyed(&reduction.reduction); + assert(reduction.explanation.signal_count == 1); +} + +static void test_build_minimal_valid_formula_with_explanation(void) { Cm13Clause clauses[1]; Cm13Formula formula = one_variable_formula(clauses); const Cm13Clause clauses_before[1] = { clauses[0] }; - YangZhangReduction reduction = {0}; + YangZhangExplainedReduction reduction = {0}; const bool top_is_r[7] = {false}; const bool bottom_is_l[7] = {false}; + assert(yang_zhang_build_explained(&formula, &reduction)); + assert(reduction.reduction.region.width == 7); + assert(reduction.reduction.region.height == 3); + assert(reduction.reduction.swaps == NULL); + assert(reduction.reduction.swap_count == 0); + assert(reduction.explanation.signal_count == 3); + assert(reduction.explanation.source_signals != NULL); + assert(reduction.explanation.target_signals != NULL); + for (uint8_t occurrence = 0; occurrence < 3; ++occurrence) { + const SignalToken expected = variable_token(0, occurrence); + assert(tokens_equal( + &reduction.explanation.source_signals[occurrence], + &expected + )); + assert(tokens_equal( + &reduction.explanation.target_signals[occurrence], + &expected + )); + } + assert(reduction.explanation.gadget_count == 4); + assert_gadget_span( + &reduction.explanation.gadgets[0], + REDUCTION_GADGET_VARIABLE, + 0, + 0, + 1, + 0, + 3, + REDUCTION_NO_SWAP_ROW + ); + assert_gadget_span( + &reduction.explanation.gadgets[1], + REDUCTION_GADGET_LEFT_FORWARD, + 0, + 1, + 3, + 0, + 3, + REDUCTION_NO_SWAP_ROW + ); + assert_gadget_span( + &reduction.explanation.gadgets[2], + REDUCTION_GADGET_RIGHT_FORWARD, + 0, + 3, + 5, + 0, + 3, + REDUCTION_NO_SWAP_ROW + ); + assert_gadget_span( + &reduction.explanation.gadgets[3], + REDUCTION_GADGET_CLAUSE, + 0, + 5, + 7, + 0, + 3, + REDUCTION_NO_SWAP_ROW + ); + assert_region_encoding(&reduction.reduction.region, top_is_r, bottom_is_l); + assert(memcmp(clauses, clauses_before, sizeof(clauses)) == 0); + + yang_zhang_explained_reduction_destroy(&reduction); + assert_explained_reduction_destroyed(&reduction); +} + +static void test_standard_build_preserves_compact_result(void) +{ + Cm13Clause clauses[1]; + Cm13Formula formula = one_variable_formula(clauses); + YangZhangReduction reduction = {0}; + assert(yang_zhang_build(&formula, &reduction)); assert(reduction.region.width == 7); assert(reduction.region.height == 3); - assert(reduction.swaps == NULL); - assert(reduction.swap_count == 0); - assert_region_encoding(&reduction.region, top_is_r, bottom_is_l); - assert(memcmp(clauses, clauses_before, sizeof(clauses)) == 0); - yang_zhang_reduction_destroy(&reduction); assert_reduction_destroyed(&reduction); } @@ -389,23 +557,70 @@ static void test_build_paper_example(void) redundant_token(3, 1), variable_token(0, 2), variable_token(1, 2), variable_token(2, 2) }; - YangZhangReduction reduction = {0}; + YangZhangExplainedReduction reduction = {0}; bool top_is_r[96] = {false}; bool bottom_is_l[96] = {false}; - assert(yang_zhang_build(&formula, &reduction)); - assert(reduction.region.height == 11); - assert(reduction.region.width == 96); - assert(reduction.swap_count == ARRAY_COUNT(expected_rows)); + assert(yang_zhang_build_explained(&formula, &reduction)); + assert(reduction.reduction.region.height == 11); + assert(reduction.reduction.region.width == 96); + assert(reduction.reduction.swap_count == ARRAY_COUNT(expected_rows)); + assert(reduction.explanation.signal_count == ARRAY_COUNT(source)); + assert(reduction.explanation.gadget_count == + 2u * formula.variable_count + 2u + ARRAY_COUNT(expected_rows)); + for (size_t i = 0; i < ARRAY_COUNT(source); ++i) { + assert(tokens_equal( + &reduction.explanation.source_signals[i], + &source[i] + )); + assert(tokens_equal( + &reduction.explanation.target_signals[i], + &target[i] + )); + } + for (uint32_t variable = 0; + variable < formula.variable_count; + ++variable) { + assert_gadget_span( + &reduction.explanation.gadgets[variable], + REDUCTION_GADGET_VARIABLE, + variable, + 0, + 1, + (int32_t)(4u * variable), + (int32_t)(4u * variable + 3u), + REDUCTION_NO_SWAP_ROW + ); + } + assert_gadget_span( + &reduction.explanation.gadgets[formula.variable_count], + REDUCTION_GADGET_LEFT_FORWARD, + 0, + 1, + 3, + 0, + 11, + REDUCTION_NO_SWAP_ROW + ); int32_t block_x = (int32_t)(YANG_ZHANG_VARIABLE_WIDTH + YANG_ZHANG_LEFT_FORWARD_WIDTH); size_t crossover_width = 0; - for (size_t i = 0; i < reduction.swap_count; ++i) { + for (size_t i = 0; i < reduction.reduction.swap_count; ++i) { const uint32_t row = expected_rows[i]; const int32_t block_width = (int32_t)row + 1; - assert(reduction.swaps[i].row == row); + assert(reduction.reduction.swaps[i].row == row); + assert_gadget_span( + &reduction.explanation.gadgets[formula.variable_count + 1u + i], + REDUCTION_GADGET_CROSSOVER, + (uint32_t)i, + block_x, + block_x + block_width, + 0, + 11, + row + ); top_is_r[block_x + block_width - 1] = true; bottom_is_l[block_x] = true; block_x += block_width; @@ -414,21 +629,50 @@ static void test_build_paper_example(void) assert(crossover_width == 89); assert(block_x == 92); + const size_t right_index = + formula.variable_count + 1u + ARRAY_COUNT(expected_rows); + assert_gadget_span( + &reduction.explanation.gadgets[right_index], + REDUCTION_GADGET_RIGHT_FORWARD, + 0, + 92, + 94, + 0, + 11, + REDUCTION_NO_SWAP_ROW + ); + for (uint32_t clause = 0; clause < formula.clause_count; ++clause) { + const int32_t first_y = (int32_t)(4u * clause); + const int32_t y_end = clause + 1u < formula.clause_count + ? first_y + 4 + : reduction.reduction.region.height; + assert_gadget_span( + &reduction.explanation.gadgets[right_index + 1u + clause], + REDUCTION_GADGET_CLAUSE, + clause, + 94, + 96, + first_y, + y_end, + REDUCTION_NO_SWAP_ROW + ); + } + assert(yang_zhang_permutation_apply( source, ARRAY_COUNT(source), - reduction.swaps, - reduction.swap_count + reduction.reduction.swaps, + reduction.reduction.swap_count )); for (size_t i = 0; i < ARRAY_COUNT(source); ++i) { assert(tokens_equal(&source[i], &target[i])); } - assert_region_encoding(&reduction.region, top_is_r, bottom_is_l); + assert_region_encoding(&reduction.reduction.region, top_is_r, bottom_is_l); assert(memcmp(clauses, clauses_before, sizeof(clauses)) == 0); - yang_zhang_reduction_destroy(&reduction); - assert_reduction_destroyed(&reduction); + yang_zhang_explained_reduction_destroy(&reduction); + assert_explained_reduction_destroyed(&reduction); } static void test_paper_dimensions_from_known_swaps(void) @@ -714,12 +958,15 @@ int main(void) { test_reduction_destroy_accepts_null_and_empty(); test_reduction_destroy_releases_and_resets_owned_storage(); + test_explained_reduction_destroy_releases_all_storage(); test_build_rejects_null_arguments(); test_build_rejects_invalid_formula_domain(); test_build_rejects_variable_count_overflow(); test_failed_build_does_not_modify_formula_storage(); test_build_rejects_non_destroyed_output(); - test_build_minimal_valid_formula(); + test_explained_build_rejects_non_destroyed_output(); + test_build_minimal_valid_formula_with_explanation(); + test_standard_build_preserves_compact_result(); test_dimensions_normal(); test_build_paper_example(); diff --git a/tests/fixtures/pipeline_sat_reduction_explain/formula-5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815.json b/tests/fixtures/pipeline_sat_reduction_explain/formula-5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815.json new file mode 100644 index 0000000..e7775ba --- /dev/null +++ b/tests/fixtures/pipeline_sat_reduction_explain/formula-5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815.json @@ -0,0 +1,34 @@ +{ + "schema": "cm13-formula-snapshot-v1", + "source": { + "name": "pipeline_sat.cm13", + "sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542" + }, + "variable_count": 3, + "clauses": [ + { + "clause_id": 0, + "variables": [ + 0, + 0, + 1 + ] + }, + { + "clause_id": 1, + "variables": [ + 0, + 1, + 2 + ] + }, + { + "clause_id": 2, + "variables": [ + 1, + 2, + 2 + ] + } + ] +} diff --git a/tests/fixtures/pipeline_sat_reduction_explain/manifest.json b/tests/fixtures/pipeline_sat_reduction_explain/manifest.json new file mode 100644 index 0000000..e1cdc6b --- /dev/null +++ b/tests/fixtures/pipeline_sat_reduction_explain/manifest.json @@ -0,0 +1,27 @@ +{ + "schema": "wang-explain-manifest-v2", + "stage": "reduction", + "source_formula_sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542", + "artifacts": { + "formula": { + "path": "formula-5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815.json", + "sha256": "5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815", + "schema": "cm13-formula-snapshot-v1" + }, + "tileset": { + "path": "tileset-462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa.json", + "sha256": "462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa", + "schema": "wang-tileset-snapshot-v1" + }, + "region": { + "path": "region-aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a.json", + "sha256": "aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a", + "schema": "wang-region-snapshot-v1" + }, + "reduction": { + "path": "reduction-6abbea9333509f852d59ed9be943d76380a49bfbdcf0f1c13e923e9ec4c4f3e2.json", + "sha256": "6abbea9333509f852d59ed9be943d76380a49bfbdcf0f1c13e923e9ec4c4f3e2", + "schema": "wang-reduction-explanation-v1" + } + } +} diff --git a/tests/fixtures/pipeline_sat_reduction_explain/reduction-6abbea9333509f852d59ed9be943d76380a49bfbdcf0f1c13e923e9ec4c4f3e2.json b/tests/fixtures/pipeline_sat_reduction_explain/reduction-6abbea9333509f852d59ed9be943d76380a49bfbdcf0f1c13e923e9ec4c4f3e2.json new file mode 100644 index 0000000..995a489 --- /dev/null +++ b/tests/fixtures/pipeline_sat_reduction_explain/reduction-6abbea9333509f852d59ed9be943d76380a49bfbdcf0f1c13e923e9ec4c4f3e2.json @@ -0,0 +1,329 @@ +{ + "schema": "wang-reduction-explanation-v1", + "geometry": "square", + "source_formula_sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542", + "region_sha256": "aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a", + "variable_count": 3, + "bounds": { + "x_begin": 0, + "x_end": 41, + "y_begin": 0, + "y_end": 11 + }, + "signals": { + "source": [ + { + "row": 0, + "kind": "variable", + "token_id": 0, + "variable": 0, + "occurrence": 0 + }, + { + "row": 1, + "kind": "variable", + "token_id": 1, + "variable": 0, + "occurrence": 1 + }, + { + "row": 2, + "kind": "variable", + "token_id": 2, + "variable": 0, + "occurrence": 2 + }, + { + "row": 3, + "kind": "redundant", + "token_id": 9, + "variable": null, + "occurrence": null + }, + { + "row": 4, + "kind": "variable", + "token_id": 3, + "variable": 1, + "occurrence": 0 + }, + { + "row": 5, + "kind": "variable", + "token_id": 4, + "variable": 1, + "occurrence": 1 + }, + { + "row": 6, + "kind": "variable", + "token_id": 5, + "variable": 1, + "occurrence": 2 + }, + { + "row": 7, + "kind": "redundant", + "token_id": 10, + "variable": null, + "occurrence": null + }, + { + "row": 8, + "kind": "variable", + "token_id": 6, + "variable": 2, + "occurrence": 0 + }, + { + "row": 9, + "kind": "variable", + "token_id": 7, + "variable": 2, + "occurrence": 1 + }, + { + "row": 10, + "kind": "variable", + "token_id": 8, + "variable": 2, + "occurrence": 2 + } + ], + "target": [ + { + "row": 0, + "kind": "variable", + "token_id": 0, + "variable": 0, + "occurrence": 0 + }, + { + "row": 1, + "kind": "variable", + "token_id": 1, + "variable": 0, + "occurrence": 1 + }, + { + "row": 2, + "kind": "variable", + "token_id": 3, + "variable": 1, + "occurrence": 0 + }, + { + "row": 3, + "kind": "redundant", + "token_id": 9, + "variable": null, + "occurrence": null + }, + { + "row": 4, + "kind": "variable", + "token_id": 2, + "variable": 0, + "occurrence": 2 + }, + { + "row": 5, + "kind": "variable", + "token_id": 4, + "variable": 1, + "occurrence": 1 + }, + { + "row": 6, + "kind": "variable", + "token_id": 6, + "variable": 2, + "occurrence": 0 + }, + { + "row": 7, + "kind": "redundant", + "token_id": 10, + "variable": null, + "occurrence": null + }, + { + "row": 8, + "kind": "variable", + "token_id": 5, + "variable": 1, + "occurrence": 2 + }, + { + "row": 9, + "kind": "variable", + "token_id": 7, + "variable": 2, + "occurrence": 1 + }, + { + "row": 10, + "kind": "variable", + "token_id": 8, + "variable": 2, + "occurrence": 2 + } + ] + }, + "gadgets": [ + { + "kind": "variable", + "ordinal": 0, + "bounds": { + "x_begin": 0, + "x_end": 1, + "y_begin": 0, + "y_end": 3 + }, + "swap_row": null + }, + { + "kind": "variable", + "ordinal": 1, + "bounds": { + "x_begin": 0, + "x_end": 1, + "y_begin": 4, + "y_end": 7 + }, + "swap_row": null + }, + { + "kind": "variable", + "ordinal": 2, + "bounds": { + "x_begin": 0, + "x_end": 1, + "y_begin": 8, + "y_end": 11 + }, + "swap_row": null + }, + { + "kind": "left_forward", + "ordinal": 0, + "bounds": { + "x_begin": 1, + "x_end": 3, + "y_begin": 0, + "y_end": 11 + }, + "swap_row": null + }, + { + "kind": "crossover", + "ordinal": 0, + "bounds": { + "x_begin": 3, + "x_end": 7, + "y_begin": 0, + "y_end": 11 + }, + "swap_row": 3 + }, + { + "kind": "crossover", + "ordinal": 1, + "bounds": { + "x_begin": 7, + "x_end": 10, + "y_begin": 0, + "y_end": 11 + }, + "swap_row": 2 + }, + { + "kind": "crossover", + "ordinal": 2, + "bounds": { + "x_begin": 10, + "x_end": 14, + "y_begin": 0, + "y_end": 11 + }, + "swap_row": 3 + }, + { + "kind": "crossover", + "ordinal": 3, + "bounds": { + "x_begin": 14, + "x_end": 22, + "y_begin": 0, + "y_end": 11 + }, + "swap_row": 7 + }, + { + "kind": "crossover", + "ordinal": 4, + "bounds": { + "x_begin": 22, + "x_end": 29, + "y_begin": 0, + "y_end": 11 + }, + "swap_row": 6 + }, + { + "kind": "crossover", + "ordinal": 5, + "bounds": { + "x_begin": 29, + "x_end": 37, + "y_begin": 0, + "y_end": 11 + }, + "swap_row": 7 + }, + { + "kind": "right_forward", + "ordinal": 0, + "bounds": { + "x_begin": 37, + "x_end": 39, + "y_begin": 0, + "y_end": 11 + }, + "swap_row": null + }, + { + "kind": "clause", + "ordinal": 0, + "bounds": { + "x_begin": 39, + "x_end": 41, + "y_begin": 0, + "y_end": 4 + }, + "swap_row": null + }, + { + "kind": "clause", + "ordinal": 1, + "bounds": { + "x_begin": 39, + "x_end": 41, + "y_begin": 4, + "y_end": 8 + }, + "swap_row": null + }, + { + "kind": "clause", + "ordinal": 2, + "bounds": { + "x_begin": 39, + "x_end": 41, + "y_begin": 8, + "y_end": 11 + }, + "swap_row": null + } + ] +} diff --git a/tests/fixtures/pipeline_sat_reduction_explain/region-aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a.json b/tests/fixtures/pipeline_sat_reduction_explain/region-aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a.json new file mode 100644 index 0000000..fa245cd --- /dev/null +++ b/tests/fixtures/pipeline_sat_reduction_explain/region-aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a.json @@ -0,0 +1,3137 @@ +{ + "schema": "wang-region-snapshot-v1", + "geometry": "square", + "source_formula_sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542", + "bounds": { + "min_x_inclusive": 0, + "min_y_inclusive": 0, + "max_x_inclusive": 40, + "max_y_inclusive": 10 + }, + "active": [ + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + false, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true, + true + ], + "boundary": [ + { + "N": 0, + "E": null, + "S": null, + "W": 1 + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 6, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": 3, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": 2 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": 2, + "S": null, + "W": null + }, + null, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": 3, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": 2 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": 2, + "S": null, + "W": null + }, + null, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + null, + { + "N": null, + "E": null, + "S": null, + "W": 1 + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": null, + "W": null + }, + { + "N": 0, + "E": 4, + "S": null, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": 1 + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 5, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": null, + "S": 0, + "W": null + }, + { + "N": null, + "E": 3, + "S": 0, + "W": null + } + ] +} diff --git a/tests/fixtures/pipeline_sat_reduction_explain/tileset-462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa.json b/tests/fixtures/pipeline_sat_reduction_explain/tileset-462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa.json new file mode 100644 index 0000000..41d70c7 --- /dev/null +++ b/tests/fixtures/pipeline_sat_reduction_explain/tileset-462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa.json @@ -0,0 +1,237 @@ +{ + "schema": "wang-tileset-snapshot-v1", + "geometry": "square", + "directions": [ + "N", + "E", + "S", + "W" + ], + "colors": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15 + ], + "tiles": [ + { + "tile_id": 0, + "edges": { + "N": 0, + "E": 2, + "S": 7, + "W": 1 + } + }, + { + "tile_id": 1, + "edges": { + "N": 7, + "E": 2, + "S": 8, + "W": 1 + } + }, + { + "tile_id": 2, + "edges": { + "N": 8, + "E": 2, + "S": 0, + "W": 1 + } + }, + { + "tile_id": 3, + "edges": { + "N": 0, + "E": 3, + "S": 0, + "W": 1 + } + }, + { + "tile_id": 4, + "edges": { + "N": 0, + "E": 4, + "S": 0, + "W": 2 + } + }, + { + "tile_id": 5, + "edges": { + "N": 0, + "E": 4, + "S": 9, + "W": 3 + } + }, + { + "tile_id": 6, + "edges": { + "N": 9, + "E": 3, + "S": 0, + "W": 2 + } + }, + { + "tile_id": 7, + "edges": { + "N": 0, + "E": 2, + "S": 0, + "W": 2 + } + }, + { + "tile_id": 8, + "edges": { + "N": 0, + "E": 3, + "S": 0, + "W": 3 + } + }, + { + "tile_id": 9, + "edges": { + "N": 5, + "E": 2, + "S": 5, + "W": 2 + } + }, + { + "tile_id": 10, + "edges": { + "N": 5, + "E": 3, + "S": 5, + "W": 3 + } + }, + { + "tile_id": 11, + "edges": { + "N": 0, + "E": 10, + "S": 6, + "W": 2 + } + }, + { + "tile_id": 12, + "edges": { + "N": 6, + "E": 2, + "S": 0, + "W": 10 + } + }, + { + "tile_id": 13, + "edges": { + "N": 0, + "E": 11, + "S": 6, + "W": 3 + } + }, + { + "tile_id": 14, + "edges": { + "N": 6, + "E": 3, + "S": 0, + "W": 11 + } + }, + { + "tile_id": 15, + "edges": { + "N": 6, + "E": 2, + "S": 12, + "W": 2 + } + }, + { + "tile_id": 16, + "edges": { + "N": 12, + "E": 2, + "S": 5, + "W": 2 + } + }, + { + "tile_id": 17, + "edges": { + "N": 6, + "E": 2, + "S": 13, + "W": 3 + } + }, + { + "tile_id": 18, + "edges": { + "N": 13, + "E": 3, + "S": 5, + "W": 2 + } + }, + { + "tile_id": 19, + "edges": { + "N": 6, + "E": 3, + "S": 14, + "W": 2 + } + }, + { + "tile_id": 20, + "edges": { + "N": 14, + "E": 2, + "S": 5, + "W": 3 + } + }, + { + "tile_id": 21, + "edges": { + "N": 6, + "E": 3, + "S": 15, + "W": 3 + } + }, + { + "tile_id": 22, + "edges": { + "N": 15, + "E": 3, + "S": 5, + "W": 3 + } + } + ] +} diff --git a/tests/python/test_native_region.py b/tests/python/test_native_region.py index b39e405..e484281 100644 --- a/tests/python/test_native_region.py +++ b/tests/python/test_native_region.py @@ -12,7 +12,10 @@ _build_region, _copy_region, ) -from native.reduction_adapter import load_formula_and_region +from native.reduction_adapter import ( + load_formula_and_region, + load_formula_region_and_explanation, +) INSTANCE_DIRECTORY = Path(__file__).resolve().parents[1] / "instances" @@ -64,6 +67,33 @@ def test_loads_formula_and_builds_region_from_one_native_parse(self) -> None: 112, ) + def test_copies_native_reduction_explanation_before_cleanup(self) -> None: + formula, region, explanation = load_formula_region_and_explanation( + INSTANCE_DIRECTORY / "pipeline_sat.cm13" + ) + + self.assertEqual(explanation.variable_count, formula.variable_count) + self.assertEqual( + (explanation.width, explanation.height), + (region.width, region.height), + ) + self.assertEqual( + tuple(signal.token_id for signal in explanation.source_signals), + (0, 1, 2, 9, 3, 4, 5, 10, 6, 7, 8), + ) + self.assertEqual( + tuple(signal.token_id for signal in explanation.target_signals), + (0, 1, 3, 9, 2, 4, 6, 10, 5, 7, 8), + ) + crossovers = tuple( + gadget + for gadget in explanation.gadgets + if gadget.kind == "crossover" + ) + self.assertEqual(len(crossovers), 6) + self.assertEqual(crossovers[0].x_begin, 3) + self.assertEqual(crossovers[-1].x_end, 37) + def test_rejects_invalid_native_extent_before_copying(self) -> None: cells = (_RegionCell * 1)() invalid_regions = ( diff --git a/tests/python/test_pipeline_snapshot.py b/tests/python/test_pipeline_snapshot.py index e392c22..e626b76 100644 --- a/tests/python/test_pipeline_snapshot.py +++ b/tests/python/test_pipeline_snapshot.py @@ -11,22 +11,29 @@ from formats.pipeline_snapshot import ( FORMULA_SCHEMA, MANIFEST_SCHEMA, + REDUCTION_MANIFEST_SCHEMA, + REDUCTION_SCHEMA, REGION_SCHEMA, TILESET_SCHEMA, PipelineSnapshotError, build_formula_snapshot, + build_reduction_explanation_snapshot, build_region_snapshot, build_tileset_snapshot, dump_pipeline_snapshots, + dump_reduction_explanation_snapshots, load_explainability_bundle, load_pipeline_snapshot, + load_reduction_explainability_bundle, validate_explain_manifest, validate_formula_snapshot, + validate_reduction_explanation_snapshot, validate_region_snapshot, validate_tileset_snapshot, ) +from model.formula import Formula from model.tileset import TILESET -from native.reduction_adapter import load_formula_and_region +from native.reduction_adapter import load_formula_region_and_explanation ROOT = Path(__file__).resolve().parents[2] @@ -38,6 +45,8 @@ TILESET_SCHEMA: ROOT / "schemas/wang-tileset-snapshot-v1.schema.json", REGION_SCHEMA: ROOT / "schemas/wang-region-snapshot-v1.schema.json", MANIFEST_SCHEMA: ROOT / "schemas/wang-explain-manifest-v1.schema.json", + REDUCTION_SCHEMA: ROOT / "schemas/wang-reduction-explanation-v1.schema.json", + REDUCTION_MANIFEST_SCHEMA: ROOT / "schemas/wang-explain-manifest-v2.schema.json", } @@ -47,7 +56,7 @@ def _snapshot_paths(manifest_path: Path) -> dict[str, Path]: "manifest": manifest_path, **{ name: manifest_path.parent / manifest["artifacts"][name]["path"] - for name in ("formula", "tileset", "region") + for name in manifest["artifacts"] }, } @@ -55,7 +64,11 @@ def _snapshot_paths(manifest_path: Path) -> dict[str, Path]: class PipelineSnapshotTests(unittest.TestCase): @classmethod def setUpClass(cls) -> None: - cls.formula, cls.region = load_formula_and_region(SAT_PATH) + ( + cls.formula, + cls.region, + cls.explanation, + ) = load_formula_region_and_explanation(SAT_PATH) def test_builders_create_closed_valid_snapshots(self) -> None: formula = build_formula_snapshot( @@ -88,7 +101,7 @@ def test_builders_create_closed_valid_snapshots(self) -> None: with self.assertRaisesRegex(TypeError, "immutable N/E/S/W"): build_tileset_snapshot(((0, 1),)) - def test_publishes_four_closed_draft_2020_12_schemas(self) -> None: + def test_publishes_six_closed_draft_2020_12_schemas(self) -> None: for contract, path in SCHEMA_PATHS.items(): with self.subTest(contract=contract): schema = json.loads(path.read_text(encoding="utf-8")) @@ -138,6 +151,145 @@ def test_dump_is_deterministic_and_manifest_is_hash_bound(self) -> None: self.assertEqual(len(tileset["tiles"]), 23) self.assertEqual(sum(region["active"]), 444) + def test_reduction_snapshot_records_native_signals_and_gadgets(self) -> None: + document = build_reduction_explanation_snapshot( + self.explanation, + source_formula_sha256=SOURCE_SHA256, + region_sha256="0" * 64, + ) + + validate_reduction_explanation_snapshot(document) + self.assertEqual(document["schema"], REDUCTION_SCHEMA) + self.assertEqual(document["bounds"]["x_end"], self.region.width) + self.assertEqual( + [signal["token_id"] for signal in document["signals"]["target"]], + [0, 1, 3, 9, 2, 4, 6, 10, 5, 7, 8], + ) + self.assertEqual( + [ + gadget["swap_row"] + for gadget in document["gadgets"] + if gadget["kind"] == "crossover" + ], + [3, 2, 3, 7, 6, 7], + ) + + wrong_target = copy.deepcopy(document) + first = wrong_target["signals"]["target"][0] + second = wrong_target["signals"]["target"][1] + for field in ("kind", "token_id", "variable", "occurrence"): + first[field], second[field] = second[field], first[field] + with self.assertRaisesRegex(PipelineSnapshotError, "does not produce target"): + validate_reduction_explanation_snapshot(wrong_target) + + bool_ordinal = copy.deepcopy(document) + bool_ordinal["gadgets"][0]["ordinal"] = True + with self.assertRaisesRegex(PipelineSnapshotError, "must be an integer"): + validate_reduction_explanation_snapshot(bool_ordinal) + + duplicate_occurrence = copy.deepcopy(document) + duplicate_occurrence["signals"]["source"][1]["occurrence"] = 0 + with self.assertRaisesRegex( + PipelineSnapshotError, + "must contain occurrences 0, 1, and 2", + ): + validate_reduction_explanation_snapshot(duplicate_occurrence) + + def test_v2_bundle_is_deterministic_and_cross_stage_hash_bound(self) -> None: + snapshots: list[dict[str, bytes]] = [] + for _ in range(2): + with tempfile.TemporaryDirectory() as directory: + manifest_path = dump_reduction_explanation_snapshots( + Path(directory) / "pipeline.explain.json", + SAT_PATH, + self.formula, + self.region, + self.explanation, + origin=(-2, 4), + ) + snapshots.append( + { + name: path.read_bytes() + for name, path in _snapshot_paths(manifest_path).items() + } + ) + bundle = load_reduction_explainability_bundle(manifest_path) + + self.assertEqual(snapshots[0], snapshots[1]) + manifest, formula, tileset, region, reduction = bundle + self.assertEqual(manifest["schema"], REDUCTION_MANIFEST_SCHEMA) + self.assertEqual(formula["source"]["sha256"], SOURCE_SHA256) + self.assertEqual(len(tileset["tiles"]), 23) + self.assertEqual(region["bounds"]["min_x_inclusive"], -2) + self.assertEqual(reduction["variable_count"], 3) + + def test_v2_bundle_rejects_rebound_reduction_with_wrong_region(self) -> None: + with tempfile.TemporaryDirectory() as directory: + manifest_path = dump_reduction_explanation_snapshots( + Path(directory) / "pipeline.explain.json", + SAT_PATH, + self.formula, + self.region, + self.explanation, + ) + manifest = json.loads(manifest_path.read_text(encoding="utf-8")) + reference = manifest["artifacts"]["reduction"] + reduction_path = manifest_path.parent / reference["path"] + reduction = json.loads(reduction_path.read_text(encoding="utf-8")) + reduction["region_sha256"] = "0" * 64 + serialized = json.dumps( + reduction, + ensure_ascii=False, + indent=2, + ) + encoded = f"{serialized}\n".encode() + digest = hashlib.sha256(encoded).hexdigest() + replacement = manifest_path.parent / f"reduction-{digest}.json" + replacement.write_bytes(encoded) + reference["path"] = replacement.name + reference["sha256"] = digest + manifest_path.write_text( + f"{json.dumps(manifest, ensure_ascii=False, indent=2)}\n", + encoding="utf-8", + ) + + with self.assertRaisesRegex( + PipelineSnapshotError, + "does not match the referenced region", + ): + load_reduction_explainability_bundle(manifest_path) + + def test_v2_cross_validation_failure_preserves_existing_manifest(self) -> None: + mismatched_formula = Formula( + variable_count=self.formula.variable_count, + clauses=tuple(reversed(self.formula.clauses)), + ) + with tempfile.TemporaryDirectory() as directory: + manifest_path = Path(directory) / "pipeline.explain.json" + dump_reduction_explanation_snapshots( + manifest_path, + SAT_PATH, + self.formula, + self.region, + self.explanation, + ) + original_manifest = manifest_path.read_bytes() + + with self.assertRaisesRegex( + PipelineSnapshotError, + "does not match the formula clauses", + ): + dump_reduction_explanation_snapshots( + manifest_path, + SAT_PATH, + mismatched_formula, + self.region, + self.explanation, + ) + + self.assertEqual(manifest_path.read_bytes(), original_manifest) + load_reduction_explainability_bundle(manifest_path) + def test_manifest_rejects_changed_artifact_bytes(self) -> None: with tempfile.TemporaryDirectory() as directory: manifest_path = dump_pipeline_snapshots( @@ -358,6 +510,29 @@ def test_cli_exports_the_real_formula_to_region_pipeline(self) -> None: self.assertEqual(bundle[3]["bounds"]["min_x_inclusive"], -7) self.assertEqual(bundle[3]["bounds"]["min_y_inclusive"], 4) + def test_cli_opt_in_exports_native_reduction_provenance(self) -> None: + with tempfile.TemporaryDirectory() as directory: + manifest_path = Path(directory) / "nested" / "manifest.json" + completed = subprocess.run( + [ + sys.executable, + str(ROOT / "tools/export_pipeline_snapshots.py"), + str(SAT_PATH), + str(manifest_path), + "--reduction-explanation", + ], + cwd=ROOT, + capture_output=True, + text=True, + check=False, + ) + bundle = load_reduction_explainability_bundle(manifest_path) + + self.assertEqual(completed.returncode, 0, completed.stderr) + self.assertIn("reduction=", completed.stdout) + self.assertEqual(bundle[0]["schema"], REDUCTION_MANIFEST_SCHEMA) + self.assertEqual(bundle[4]["schema"], REDUCTION_SCHEMA) + if __name__ == "__main__": unittest.main() diff --git a/tests/python/test_reduction_explanation_model.py b/tests/python/test_reduction_explanation_model.py new file mode 100644 index 0000000..0916991 --- /dev/null +++ b/tests/python/test_reduction_explanation_model.py @@ -0,0 +1,160 @@ +from dataclasses import FrozenInstanceError, replace +import unittest + +from model.reduction_explanation import ( + GADGET_CLAUSE, + GADGET_CROSSOVER, + GADGET_LEFT_FORWARD, + GADGET_RIGHT_FORWARD, + GADGET_VARIABLE, + SIGNAL_VARIABLE, + ReductionExplanation, + ReductionGadget, + ReductionSignal, +) + + +def _signal(row: int, occurrence: int) -> ReductionSignal: + return ReductionSignal( + row=row, + kind=SIGNAL_VARIABLE, + token_id=occurrence, + variable=0, + occurrence=occurrence, + ) + + +def _explanation(*, crossover: bool = False) -> ReductionExplanation: + source = tuple(_signal(row, row) for row in range(3)) + if crossover: + target = ( + _signal(0, 1), + _signal(1, 0), + _signal(2, 2), + ) + crossover_gadgets = ( + ReductionGadget( + kind=GADGET_CROSSOVER, + ordinal=0, + x_begin=3, + x_end=4, + y_begin=0, + y_end=3, + swap_row=0, + ), + ) + right_begin = 4 + else: + target = source + crossover_gadgets = () + right_begin = 3 + gadgets = ( + ReductionGadget(GADGET_VARIABLE, 0, 0, 1, 0, 3, None), + ReductionGadget(GADGET_LEFT_FORWARD, 0, 1, 3, 0, 3, None), + *crossover_gadgets, + ReductionGadget( + GADGET_RIGHT_FORWARD, + 0, + right_begin, + right_begin + 2, + 0, + 3, + None, + ), + ReductionGadget( + GADGET_CLAUSE, + 0, + right_begin + 2, + right_begin + 4, + 0, + 3, + None, + ), + ) + return ReductionExplanation( + variable_count=1, + width=right_begin + 4, + height=3, + source_signals=source, + target_signals=target, + gadgets=gadgets, + ) + + +class ReductionExplanationModelTests(unittest.TestCase): + def test_is_immutable_and_replays_the_recorded_crossover(self) -> None: + explanation = _explanation(crossover=True) + + self.assertEqual(explanation.target_signals[0].occurrence, 1) + with self.assertRaises(FrozenInstanceError): + explanation.width = 99 # type: ignore[misc] + + def test_rejects_target_not_produced_by_the_crossover_program(self) -> None: + explanation = _explanation() + target = ( + _signal(0, 1), + _signal(1, 0), + _signal(2, 2), + ) + + with self.assertRaisesRegex(ValueError, "does not produce target"): + replace(explanation, target_signals=target) + + def test_requires_half_open_gadget_bounds_inside_the_region(self) -> None: + with self.assertRaisesRegex(ValueError, "x interval"): + ReductionGadget(GADGET_VARIABLE, 0, 1, 1, 0, 3, None) + + explanation = _explanation() + invalid = replace(explanation.gadgets[0], x_end=explanation.width + 1) + with self.assertRaisesRegex(ValueError, "inside the region"): + replace(explanation, gadgets=(invalid, *explanation.gadgets[1:])) + + def test_crossover_width_is_bound_to_its_swap_row(self) -> None: + with self.assertRaisesRegex(ValueError, "width must equal"): + ReductionGadget(GADGET_CROSSOVER, 0, 3, 5, 0, 3, 0) + + def test_rejects_missing_semantic_gadget_populations(self) -> None: + explanation = _explanation() + without_clause = tuple( + gadget + for gadget in explanation.gadgets + if gadget.kind != GADGET_CLAUSE + ) + + with self.assertRaisesRegex(ValueError, "expected 1 clause"): + replace(explanation, gadgets=without_clause) + + def test_rejects_bool_where_an_integer_is_required(self) -> None: + with self.assertRaises(ValueError): + ReductionSignal(True, SIGNAL_VARIABLE, 0, 0, 0) + + def test_requires_unique_token_ids_and_all_three_occurrences(self) -> None: + explanation = _explanation() + duplicate_id = replace(explanation.source_signals[1], token_id=0) + with self.assertRaisesRegex(ValueError, "token IDs must be unique"): + replace( + explanation, + source_signals=( + explanation.source_signals[0], + duplicate_id, + explanation.source_signals[2], + ), + ) + + repeated_occurrence = replace( + explanation.source_signals[1], + occurrence=0, + ) + with self.assertRaisesRegex(ValueError, "occurrences 0, 1, and 2"): + replace( + explanation, + source_signals=( + explanation.source_signals[0], + repeated_occurrence, + explanation.source_signals[2], + ), + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/export_pipeline_snapshots.py b/tools/export_pipeline_snapshots.py index 79febe8..81529b5 100644 --- a/tools/export_pipeline_snapshots.py +++ b/tools/export_pipeline_snapshots.py @@ -13,9 +13,13 @@ from formats.pipeline_snapshot import ( # noqa: E402 dump_pipeline_snapshots, + dump_reduction_explanation_snapshots, load_pipeline_snapshot, ) -from native.reduction_adapter import load_formula_and_region # noqa: E402 +from native.reduction_adapter import ( # noqa: E402 + load_formula_and_region, + load_formula_region_and_explanation, +) def _parser() -> argparse.ArgumentParser: @@ -29,24 +33,45 @@ def _parser() -> argparse.ArgumentParser: parser.add_argument("manifest", type=Path, help="output manifest JSON") parser.add_argument("--origin-x", type=int, default=0) parser.add_argument("--origin-y", type=int, default=0) + parser.add_argument( + "--reduction-explanation", + action="store_true", + help="include native signal, permutation, and gadget provenance", + ) return parser def main(arguments: list[str] | None = None) -> int: args = _parser().parse_args(arguments) args.manifest.parent.mkdir(parents=True, exist_ok=True) - formula, region = load_formula_and_region(args.source) - manifest_path = dump_pipeline_snapshots( - args.manifest, - args.source, - formula, - region, - origin=(args.origin_x, args.origin_y), - ) + if args.reduction_explanation: + formula, region, explanation = load_formula_region_and_explanation( + args.source + ) + manifest_path = dump_reduction_explanation_snapshots( + args.manifest, + args.source, + formula, + region, + explanation, + origin=(args.origin_x, args.origin_y), + ) + else: + formula, region = load_formula_and_region(args.source) + manifest_path = dump_pipeline_snapshots( + args.manifest, + args.source, + formula, + region, + origin=(args.origin_x, args.origin_y), + ) manifest = load_pipeline_snapshot(manifest_path) artifacts = manifest["artifacts"] print(f"manifest={manifest_path}") - for name in ("formula", "tileset", "region"): + artifact_names = ["formula", "tileset", "region"] + if "reduction" in artifacts: + artifact_names.append("reduction") + for name in artifact_names: artifact_path = manifest_path.parent / artifacts[name]["path"] print(f"{name}={artifact_path}") return 0