Skip to content

Add static explainability snapshots and views #15

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
xtraid merged 1 commit into from
Aug 26, 2026
Merged

Add static explainability snapshots and views #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
68 changes: 39 additions & 29 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ solving remains future work.
| Verified square solution export | Implemented as the closed `wang-solution-v1` contract and deterministic exporter |
| 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 |
| 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 |

Expand All @@ -89,29 +90,32 @@ The implemented paths are:

```text
.cm13 --> C parser --> native Formula
| \
| +--> copied Formula --> Boolean Z3
| |
| v
| Boolean witness checker
| |\
| | +--> formula snapshot --> formula view
| +----> copied Formula ----> Boolean Z3
| |
| v
| Boolean witness checker
v
Yang–Zhang builder --> Region
| \
| +--> copied Region + TILESET
| |
| v
native reference/ Wang Z3
optimized solver |
| v
v Python tiling checker
native verifier
|
copied tiling + Python checker
|
v
wang-solution-v1 --> square PNG (default)
\
+--> pure hex port/check --> hex PNG (--hex)
| |\
| | +--> static manifest --> region view
| | + tile sheet
| +----> copied Region + TILESET
| |
| v
native reference/ Wang Z3
optimized solver |
| v
v Python tiling checker
native verifier
|
copied tiling + Python checker
|
v
wang-solution-v1 --> square PNG (default/explain)
\
+--> pure hex port/check --> hex PNG (--hex)
```

The witness bridge relates exact Boolean assignments to the variable cells of
Expand Down Expand Up @@ -144,12 +148,15 @@ diagram.

## Next milestones

Planned work remains separated into independently reviewed changes:
Planned work remains separated into independently reviewed changes. The new
priority is explainability across the deterministic pipeline:

1. evaluate MRV indexing on weakly constrained search and build a separate
hard-UNSAT corpus before making parallelism claims;
2. harden allocation and cleanup failure paths before concurrent execution;
3. define and validate a minimal serial `TaskPlan` before implementing OpenMP.
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
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.

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
Expand All @@ -172,7 +179,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 213-test combined suite independently:
`make check`. Run its 234-test combined suite independently:

```sh
cd renderer
Expand Down Expand Up @@ -206,6 +213,9 @@ The [square solution contract](docs/wang_solution_v1.md) includes the producer
API for exporting a verified native result before rendering it. The
[square-to-hex reference](docs/wang_square_to_hex.md) defines the mapping,
inverse proof, checker boundary, and integer axial raster convention.
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.

Useful individual targets:

Expand Down Expand Up @@ -285,11 +295,11 @@ src/verify/ independent tiling verification
src/io/ formula parsing and native JSON placeholder
python/model/ pure Python data contracts
python/native/ C ABI adapters and ownership boundaries
python/formats/ versioned solution validation and deterministic export
python/formats/ versioned solution and static-snapshot validation/export
python/crosscheck/ scoped native/Z3 witness orchestration
python/oracles/ independent Z3 oracles and witness checks
python/hex/ deliberately unused empty hex-core placeholders
renderer/ isolated legacy and square/default, hex/explicit Wang rendering
renderer/ isolated legacy and explainable square/hex Wang rendering
tests/ C, Python, and instance regressions
benchmarks/ fixed reference corpus and profiling runner
docs/ theory and architecture references
Expand Down
14 changes: 12 additions & 2 deletions docs/development_principles.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,9 +95,10 @@ A module is implemented when it has:
| `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` | Square solution validation and deterministic export | Native lifetimes, solving, and presentation |
| `python/formats` | Solution and static pipeline snapshot 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_square.py` | Structural presentation projection and square/default or hex/explicit rasterization | 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_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
under `python/hex/` are placeholders. `src/io/json.c` is also a placeholder;
Expand Down Expand Up @@ -201,6 +202,15 @@ instances, and its tests verify that construction.

### Downstream solution and renderer boundary

Before solving, `python/formats/pipeline_snapshot.py` can project copied
`Formula`, canonical `TILESET`, and unassigned `Region` values into three
closed, versioned documents referenced by a hash-bound manifest. These are
presentation-neutral snapshots: they preserve source identity, ordered formula
positions, positional tile IDs, active cells, bounds, and exposed boundary
constraints without adding fields to the core models. The
[static snapshot contract]({{ '/wang-explainability-snapshots/' | relative_url }})
defines their failure and rendering behavior.

The native-only solve coordinator copies a verified SAT tiling out of native
storage and applies the independent Python Wang checker. The exporter then
produces the closed square-only `wang-solution-v1` document. The
Expand Down
136 changes: 136 additions & 0 deletions docs/wang_explainability_snapshots.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,136 @@
---
layout: page
title: Static pipeline snapshots and explainable Wang views
permalink: /wang-explainability-snapshots/
description: Versioned formula, tileset, and unassigned-region snapshots consumed by the isolated Wang renderer.
section: Architecture and correctness
document_kind: Data and rendering contract
status: Current implementation
updated: 2026-08-26
nav_order: 33
---

# Static pipeline snapshots and explainable Wang views

The pipeline can export its state after parsing and region construction without
running a solver. The isolated renderer turns that state into three diagnostic
views: the parsed formula, the canonical tile sheet, and the unassigned region
with the formula beside it. A verified solution can additionally be rendered
with colored edge bands, tile IDs, emphasized boundary constraints, and a
palette legend.

These views explain data that already exists at a module boundary. They do not
add presentation fields to `Formula` or `Region`, expose native pointers, or
make a PNG part of the correctness argument.

## Contracts and identity

The exporter writes four closed JSON documents:

| Schema | Meaning |
| --- | --- |
| `cm13-formula-snapshot-v1` | Source basename and digest, ordered clauses, and all three variable positions, including repeats |
| `wang-tileset-snapshot-v1` | Canonical positional tile IDs and their square `N,E,S,W` colors |
| `wang-region-snapshot-v1` | Inclusive bounds, dense active mask, exposed boundary constraints, and no assignment |
| `wang-explain-manifest-v1` | Stage identity plus a basename, schema, and full SHA-256 digest for each artifact |

The manifest is installed atomically only after its content-addressed artifacts
have been installed. Both the producer and the renderer reject duplicate JSON
members, non-finite numbers, unknown fields, invalid types, path traversal,
hash drift, mismatched formula identity, and region colors absent from the
referenced tileset.

The committed example was produced from `tests/instances/pipeline_sat.cm13` and
lives in `tests/fixtures/pipeline_sat_explain/`. It is data, not a hand-edited
diagram.

## Export from the real construction pipeline

Build the shared native library, then parse and reduce one formula:

```sh
make shared
uv run --frozen python tools/export_pipeline_snapshots.py \
tests/instances/pipeline_sat.cm13 \
/tmp/pipeline-sat-explain/manifest.json
```

The command loads the formula and constructs the real Yang–Zhang `Region`
through the scoped native adapter. It prints the manifest and three generated
artifact paths. It performs no solving.

## Render each static stage

From `renderer/`, pass the manifest to the existing Wang command and select a
view:

```sh
uv run --locked python wang_square.py \
../tests/fixtures/pipeline_sat_explain/manifest.json \
output/formula.png --view formula

uv run --locked python wang_square.py \
../tests/fixtures/pipeline_sat_explain/manifest.json \
output/tileset-square.png --view tileset

uv run --locked python wang_square.py \
../tests/fixtures/pipeline_sat_explain/manifest.json \
output/region-square.png --view region
```

The tile sheet and region also accept the explicit `--hex` flag. Their hex
data is not stored in JSON: the renderer applies the same pure Basire/Culik
port and raster-independent checker used for verified solutions.

```sh
uv run --locked python wang_square.py \
../tests/fixtures/pipeline_sat_explain/manifest.json \
output/tileset-hex.png --view tileset --hex

uv run --locked python wang_square.py \
../tests/fixtures/pipeline_sat_explain/manifest.json \
output/region-hex.png --view region --hex
```

The region view deliberately contains no tiles: pale cells are active
positions, crossed cells are outside the region, and colored bands are exposed
boundary constraints. The adjacent formula panel states exactly which parsed
formula the region simulates.

## Render the final verified witness

The default solution image remains byte-for-byte compatible. Explainability is
opt-in:

```sh
uv run --locked python wang_square.py \
../tests/fixtures/wang_solution_v1_square_sat.json \
output/solution-explain.png --explain

uv run --locked python wang_square.py \
../tests/fixtures/wang_solution_v1_square_sat.json \
output/solution-explain-hex.png --explain --hex
```

Every tile shows its positional ID. Each logical edge color has a deterministic
RGB band, exposed constraints receive a heavier outer stroke, and the legend
retains the numeric color identity. The hex view also labels the fresh
presentation color `kappa = max(C) + 1`.

## Correctness and current scope

The static contracts stop at the constructed region. They contain neither
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 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
and both explainable final-solution modes. The old square and hex solution
goldens remain unchanged when `--explain` is absent.

Rendering still does not prove SAT, region validity, or witness validity. Those
obligations remain with construction tests, the independent verifier, the
solution exporter, and the square-to-hex checker described by their respective
contracts.
Loading