diff --git a/README.md b/README.md
index 2a3b54e..09027e0 100644
--- a/README.md
+++ b/README.md
@@ -78,7 +78,7 @@ solving remains future work.
| Native solver event trace | Implemented as separate opt-in reference/optimized entry points with bounded observed events, full initial state, checkpoints, manifest v3, independent offline replay, and deterministic PNG/GIF views |
| Reproducible Z3 summaries | Implemented for fixed seed/thread settings and explicit Boolean/Wang encoding order, result/model, and stable project-owned counts; no internal Z3 trace claim |
| Observed-run dossier | Implemented as one opt-in generator of closed raw run metadata, fixed LaTeX, PDF, and reused trace/square/hex assets; four versioned SAT/UNSAT case definitions cover distinct execution shapes |
-| Full-pipeline multi-engine capture | Implemented as separate closed v2 case/run contracts and one atomic raw capture over Boolean Z3, one native reduction, reference, optimized, Wang Z3, and existing independent checkers; narrative assets and PDF v2 remain downstream work |
+| Full-pipeline multi-engine capture | Implemented as separate closed v2 case/run contracts and one atomic capture over Boolean Z3, one native reduction, reference, optimized, Wang Z3, and existing independent checkers; a closed shared-asset pass now binds semantic milestones and static square/generalized/hex presentations, while PDF v2 remains downstream work |
| 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 |
@@ -234,6 +234,16 @@ The [observed-run dossier contract](docs/run_dossiers.md) defines the four
versioned case classes, authoritative raw metadata, fixed TeX scaffolding,
asset reuse, atomic output, and UNSAT evidence boundary.
+The v2 shared-asset pass is also opt-in through the same dossier command. It
+validates the raw multi-engine capture, renders Boolean/Wang encoding order,
+Yang--Zhang construction, both observed traces, verification receipts, the
+checked witness presentation, and the six-mechanism didactic overview, then
+records every GIF, reduced-motion fallback, contact sheet, frame, caption, alt
+text, semantic label, owner, and source hash in
+`wang-narrative-assets-v1`. The same generator can target a temporary
+`canonical-pages` bundle; tests require all compositor-produced bytes to match
+the run-specific bundle for identical inputs and parameters.
+
To export one observed reference run and render selected replay states:
```sh
diff --git a/docs/assets/images/builder-routing/contact-sheet.png b/docs/assets/images/builder-routing/contact-sheet.png
index 9d94383..905d9d9 100644
Binary files a/docs/assets/images/builder-routing/contact-sheet.png and b/docs/assets/images/builder-routing/contact-sheet.png differ
diff --git a/docs/assets/images/builder-routing/frame-00.png b/docs/assets/images/builder-routing/frame-00.png
index 03af137..84101a5 100644
Binary files a/docs/assets/images/builder-routing/frame-00.png and b/docs/assets/images/builder-routing/frame-00.png differ
diff --git a/docs/assets/images/builder-routing/frame-01.png b/docs/assets/images/builder-routing/frame-01.png
index a220f8c..b1121f9 100644
Binary files a/docs/assets/images/builder-routing/frame-01.png and b/docs/assets/images/builder-routing/frame-01.png differ
diff --git a/docs/assets/images/builder-routing/frame-02.png b/docs/assets/images/builder-routing/frame-02.png
index 3b599b7..83315f9 100644
Binary files a/docs/assets/images/builder-routing/frame-02.png and b/docs/assets/images/builder-routing/frame-02.png differ
diff --git a/docs/assets/images/builder-routing/frame-03.png b/docs/assets/images/builder-routing/frame-03.png
index b0e1ba5..0e0e1de 100644
Binary files a/docs/assets/images/builder-routing/frame-03.png and b/docs/assets/images/builder-routing/frame-03.png differ
diff --git a/docs/assets/images/builder-routing/frame-04.png b/docs/assets/images/builder-routing/frame-04.png
index 87a6656..e352835 100644
Binary files a/docs/assets/images/builder-routing/frame-04.png and b/docs/assets/images/builder-routing/frame-04.png differ
diff --git a/docs/assets/images/builder-routing/frame-05.png b/docs/assets/images/builder-routing/frame-05.png
index ddd6eed..5340377 100644
Binary files a/docs/assets/images/builder-routing/frame-05.png and b/docs/assets/images/builder-routing/frame-05.png differ
diff --git a/docs/assets/images/builder-routing/trace.gif b/docs/assets/images/builder-routing/trace.gif
index 5f3067a..7319b30 100644
Binary files a/docs/assets/images/builder-routing/trace.gif and b/docs/assets/images/builder-routing/trace.gif differ
diff --git a/docs/assets/images/optimized-mechanisms/contact-sheet.png b/docs/assets/images/optimized-mechanisms/contact-sheet.png
index 9bf0212..0a9d187 100644
Binary files a/docs/assets/images/optimized-mechanisms/contact-sheet.png and b/docs/assets/images/optimized-mechanisms/contact-sheet.png differ
diff --git a/docs/assets/images/optimized-mechanisms/frame-00.png b/docs/assets/images/optimized-mechanisms/frame-00.png
index 016ce02..c0d4f16 100644
Binary files a/docs/assets/images/optimized-mechanisms/frame-00.png and b/docs/assets/images/optimized-mechanisms/frame-00.png differ
diff --git a/docs/assets/images/optimized-mechanisms/frame-01.png b/docs/assets/images/optimized-mechanisms/frame-01.png
index c651553..1ad49a3 100644
Binary files a/docs/assets/images/optimized-mechanisms/frame-01.png and b/docs/assets/images/optimized-mechanisms/frame-01.png differ
diff --git a/docs/assets/images/optimized-mechanisms/frame-02.png b/docs/assets/images/optimized-mechanisms/frame-02.png
index 6aa6b84..6f4ae6f 100644
Binary files a/docs/assets/images/optimized-mechanisms/frame-02.png and b/docs/assets/images/optimized-mechanisms/frame-02.png differ
diff --git a/docs/assets/images/optimized-mechanisms/frame-03.png b/docs/assets/images/optimized-mechanisms/frame-03.png
index b5d66f8..ea61b52 100644
Binary files a/docs/assets/images/optimized-mechanisms/frame-03.png and b/docs/assets/images/optimized-mechanisms/frame-03.png differ
diff --git a/docs/assets/images/optimized-mechanisms/frame-04.png b/docs/assets/images/optimized-mechanisms/frame-04.png
index 325bd02..3e1af5d 100644
Binary files a/docs/assets/images/optimized-mechanisms/frame-04.png and b/docs/assets/images/optimized-mechanisms/frame-04.png differ
diff --git a/docs/assets/images/optimized-mechanisms/frame-05.png b/docs/assets/images/optimized-mechanisms/frame-05.png
index 32bb622..36aca68 100644
Binary files a/docs/assets/images/optimized-mechanisms/frame-05.png and b/docs/assets/images/optimized-mechanisms/frame-05.png differ
diff --git a/docs/assets/images/optimized-mechanisms/frame-06.png b/docs/assets/images/optimized-mechanisms/frame-06.png
new file mode 100644
index 0000000..02a2de2
Binary files /dev/null and b/docs/assets/images/optimized-mechanisms/frame-06.png differ
diff --git a/docs/assets/images/optimized-mechanisms/trace.gif b/docs/assets/images/optimized-mechanisms/trace.gif
index 18f0064..b4e93ad 100644
Binary files a/docs/assets/images/optimized-mechanisms/trace.gif and b/docs/assets/images/optimized-mechanisms/trace.gif differ
diff --git a/docs/assets/images/solver-trace/contact-sheet.png b/docs/assets/images/solver-trace/contact-sheet.png
index ba28522..425e409 100644
Binary files a/docs/assets/images/solver-trace/contact-sheet.png and b/docs/assets/images/solver-trace/contact-sheet.png differ
diff --git a/docs/assets/images/solver-trace/frame-000001.png b/docs/assets/images/solver-trace/frame-000001.png
new file mode 100644
index 0000000..21fefb3
Binary files /dev/null and b/docs/assets/images/solver-trace/frame-000001.png differ
diff --git a/docs/assets/images/solver-trace/frame-000413.png b/docs/assets/images/solver-trace/frame-000413.png
deleted file mode 100644
index f3158e3..0000000
Binary files a/docs/assets/images/solver-trace/frame-000413.png and /dev/null differ
diff --git a/docs/assets/images/solver-trace/frame-000827.png b/docs/assets/images/solver-trace/frame-000827.png
deleted file mode 100644
index 6e359e2..0000000
Binary files a/docs/assets/images/solver-trace/frame-000827.png and /dev/null differ
diff --git a/docs/assets/images/solver-trace/frame-001240.png b/docs/assets/images/solver-trace/frame-001240.png
deleted file mode 100644
index 26fb825..0000000
Binary files a/docs/assets/images/solver-trace/frame-001240.png and /dev/null differ
diff --git a/docs/assets/images/solver-trace/frame-001654.png b/docs/assets/images/solver-trace/frame-001654.png
deleted file mode 100644
index 9322ced..0000000
Binary files a/docs/assets/images/solver-trace/frame-001654.png and /dev/null differ
diff --git a/docs/assets/images/solver-trace/frame-002518.png b/docs/assets/images/solver-trace/frame-002518.png
new file mode 100644
index 0000000..8b4a6f6
Binary files /dev/null and b/docs/assets/images/solver-trace/frame-002518.png differ
diff --git a/docs/assets/images/solver-trace/frame-002893.png b/docs/assets/images/solver-trace/frame-002893.png
new file mode 100644
index 0000000..ef8ea34
Binary files /dev/null and b/docs/assets/images/solver-trace/frame-002893.png differ
diff --git a/docs/assets/images/solver-trace/frame-002894.png b/docs/assets/images/solver-trace/frame-002894.png
new file mode 100644
index 0000000..2b8bb0d
Binary files /dev/null and b/docs/assets/images/solver-trace/frame-002894.png differ
diff --git a/docs/assets/images/solver-trace/trace.gif b/docs/assets/images/solver-trace/trace.gif
index e48e51d..16ec2f6 100644
Binary files a/docs/assets/images/solver-trace/trace.gif and b/docs/assets/images/solver-trace/trace.gif differ
diff --git a/docs/assets/images/square-to-hex/contact-sheet.png b/docs/assets/images/square-to-hex/contact-sheet.png
index 9d37d82..0ec26e6 100644
Binary files a/docs/assets/images/square-to-hex/contact-sheet.png and b/docs/assets/images/square-to-hex/contact-sheet.png differ
diff --git a/docs/assets/images/square-to-hex/frame-00.png b/docs/assets/images/square-to-hex/frame-00.png
index e211ed0..cbb9ae0 100644
Binary files a/docs/assets/images/square-to-hex/frame-00.png and b/docs/assets/images/square-to-hex/frame-00.png differ
diff --git a/docs/assets/images/square-to-hex/frame-01.png b/docs/assets/images/square-to-hex/frame-01.png
index 41d7ef9..798240e 100644
Binary files a/docs/assets/images/square-to-hex/frame-01.png and b/docs/assets/images/square-to-hex/frame-01.png differ
diff --git a/docs/assets/images/square-to-hex/frame-02.png b/docs/assets/images/square-to-hex/frame-02.png
index b544431..7312ff5 100644
Binary files a/docs/assets/images/square-to-hex/frame-02.png and b/docs/assets/images/square-to-hex/frame-02.png differ
diff --git a/docs/assets/images/square-to-hex/frame-03.png b/docs/assets/images/square-to-hex/frame-03.png
index a0df31b..36f1917 100644
Binary files a/docs/assets/images/square-to-hex/frame-03.png and b/docs/assets/images/square-to-hex/frame-03.png differ
diff --git a/docs/assets/images/square-to-hex/trace.gif b/docs/assets/images/square-to-hex/trace.gif
index f8f054d..02824a6 100644
Binary files a/docs/assets/images/square-to-hex/trace.gif and b/docs/assets/images/square-to-hex/trace.gif differ
diff --git a/docs/plans/2026-08-31-narrative-migration-checklist.md b/docs/plans/2026-08-31-narrative-migration-checklist.md
index 9327972..c5374cb 100644
--- a/docs/plans/2026-08-31-narrative-migration-checklist.md
+++ b/docs/plans/2026-08-31-narrative-migration-checklist.md
@@ -140,6 +140,7 @@ checks prove the old files are unreferenced before deletion.
| `wang-explain-manifest-v3` | `/wang-solver-trace/` | Retain trace-stage meaning |
| `wang-run-case-v1` | `/run-dossiers/` | Preserve exact diagnostic case meaning and initial-domain override support |
| `wang-run-dossier-v1` | `/run-dossiers/` | Preserve exact single-native-run report meaning and output shape |
+| `wang-narrative-assets-v1` | `/run-dossiers/` and `renderer/README.md` | Closed downstream record for fixed component assets, accessibility metadata, source identities, semantic milestones, and static PDF inputs |
- [x] Add separate closed v2 case and dossier contracts; do not extend or
loosen either v1 schema.
@@ -175,11 +176,11 @@ checks prove the old files are unreferenced before deletion.
the atomic tileset or standard square/hex output.
2. [x] Capture the explicit v2 multi-engine fields once per engine and bind all
component identities by SHA-256.
-3. [ ] Produce shared assets through the existing validators, replay, and
+3. [x] Produce shared assets through the existing validators, replay, and
compositor, including static semantic milestones.
-4. [ ] Update the optimized didactic asset to all six accepted mechanisms,
+4. [x] Update the optimized didactic asset to all six accepted mechanisms,
keeping it secondary to observed trace output.
-5. [ ] Generate reduced-motion fallback, contact sheet, caption, alt text, and
+5. [x] Generate reduced-motion fallback, contact sheet, caption, alt text, and
semantic record for every GIF.
6. [ ] Move public ownership to component pages without duplicating files or
explanations; update old pages to links in the same change.
diff --git a/docs/run_dossiers.md b/docs/run_dossiers.md
index e731a5a..9415840 100644
--- a/docs/run_dossiers.md
+++ b/docs/run_dossiers.md
@@ -120,7 +120,7 @@ once each. SAT assignments and tilings are checked with the existing pure
Python checkers; native tilings also retain the assignment extracted by the
existing Yang--Zhang witness bridge.
-The raw v2 directory contains `run.json`, the copied CM1-in-3 input, two
+The v2 directory contains `run.json`, the copied CM1-in-3 input, two
existing trace-v3 manifests, their content-addressed snapshots, and the two
existing Z3 summary documents. Both native manifests bind the same formula,
tileset, region, and construction-provenance hashes. Agreement means equal
@@ -128,11 +128,28 @@ SAT/UNSAT status plus independently valid SAT witnesses; different valid
witnesses are not required to be byte-equal. UNKNOWN, mismatch, a truncated
trace, or a failed checker aborts the capture before installation.
-The raw-capture implementation intentionally produces no v2 PDF or narrative
-raster. The closed run contract names the square, generalized, and hex
-relationships and leaves their artifact references null for the shared-asset
-pass. A later PDF formatter will consume those validated static assets without
-solving, checking, replaying, or rendering again.
+The downstream shared-asset pass then consumes only that validated capture.
+Its closed `wang-narrative-assets-v1` manifest names fixed component assets,
+not generic stages: Boolean and Wang Z3 encoding order, canonical region
+construction, observed reference and optimized traces, the six checker
+records, the checked square/generalized/hex witness sequence, the six retained
+optimized mechanisms, and the complete pipeline overview. Every GIF record
+contains one reduced-motion PNG, contact sheet, caption, alt text, semantic
+label, source identity, completeness/selection scope, and all static frame
+hashes.
+
+Trace frames use `semantic-milestones-v1`, which selects event and phase
+transitions before deterministic gap filling; it is distinct from uniform
+sampling and reuses the same single replay as PNG, contact-sheet, and GIF
+encoding. For SAT, `run.json` binds the three reserved static presentation
+artifacts and their hashes. For UNSAT they remain null, while the asset bundle
+records an explicit not-applicable panel and never fabricates a witness or
+certificate. The separate example is versioned at
+`examples/run-cases-v2/pipeline-unsat-search.json`.
+
+No v2 PDF is produced yet. Its later formatter will consume only the validated
+static milestone PNGs already named by the asset manifest, without solving,
+checking, replaying, or rendering again.
All v2 durations use one monotonic nanosecond clock and are labelled
`run-specific-observation-not-a-benchmark`. They are raw facts about that
diff --git a/docs/solver_byte_support_2026-08-20.md b/docs/solver_byte_support_2026-08-20.md
index 00f958e..ed11f29 100644
--- a/docs/solver_byte_support_2026-08-20.md
+++ b/docs/solver_byte_support_2026-08-20.md
@@ -14,10 +14,10 @@ nav_order: 60
-
- 
+
+
- Didactic replay. This shared animation locates byte-wise support aggregation among the five isolated mechanisms; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
+ Didactic. This shared animation locates byte-wise support aggregation among the six isolated mechanisms, including the later lazy MRV index; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
This report evaluates only the union of compatible neighbor tiles during
diff --git a/docs/solver_dynamic_stack_2026-08-17.md b/docs/solver_dynamic_stack_2026-08-17.md
index f033135..22fa709 100644
--- a/docs/solver_dynamic_stack_2026-08-17.md
+++ b/docs/solver_dynamic_stack_2026-08-17.md
@@ -14,10 +14,10 @@ nav_order: 30
-
-
+
+
- Didactic replay. This shared animation locates the dynamic stack among the five isolated mechanisms; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
+ Didactic. This shared animation locates the dynamic stack among the six isolated mechanisms, including the later lazy MRV index; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
This report evaluates only DFS stack storage. The reference path still
diff --git a/docs/solver_initial_trail_2026-08-17.md b/docs/solver_initial_trail_2026-08-17.md
index 558b806..6e743c2 100644
--- a/docs/solver_initial_trail_2026-08-17.md
+++ b/docs/solver_initial_trail_2026-08-17.md
@@ -14,10 +14,10 @@ nav_order: 40
-
-
+
+
- Didactic replay. This shared animation locates initial-trail omission among the five isolated mechanisms; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
+ Didactic. This shared animation locates initial-trail omission among the six isolated mechanisms, including the later lazy MRV index; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
This report evaluates undo-trail recording during initial propagation. The
diff --git a/docs/solver_queue_dedup_2026-08-20.md b/docs/solver_queue_dedup_2026-08-20.md
index 13c9a90..ce0876f 100644
--- a/docs/solver_queue_dedup_2026-08-20.md
+++ b/docs/solver_queue_dedup_2026-08-20.md
@@ -14,10 +14,10 @@ nav_order: 80
-
-
+
+
- Didactic replay. This shared animation locates queue deduplication among the five isolated mechanisms; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
+ Didactic. This shared animation locates queue deduplication among the six isolated mechanisms, including the later lazy MRV index; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
This accepted mechanism changes only the optimized propagation queue. An
diff --git a/docs/solver_sat_ownership_2026-08-20.md b/docs/solver_sat_ownership_2026-08-20.md
index cb84837..47448ee 100644
--- a/docs/solver_sat_ownership_2026-08-20.md
+++ b/docs/solver_sat_ownership_2026-08-20.md
@@ -14,10 +14,10 @@ nav_order: 50
-
-
+
+
- Didactic replay. This shared animation locates SAT ownership transfer among the five isolated mechanisms; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
+ Didactic. This shared animation locates SAT ownership transfer among the six isolated mechanisms, including the later lazy MRV index; the measurements below, not the animation, establish its effect. The static contact sheet shows all stages.
This report evaluates only construction of a successful solver result. The
diff --git a/docs/wang_square_to_hex.md b/docs/wang_square_to_hex.md
index 3e1c09e..9df4b6b 100644
--- a/docs/wang_square_to_hex.md
+++ b/docs/wang_square_to_hex.md
@@ -37,9 +37,9 @@ construction. They are not attributed to either source's diagram notation.
- 
+
- Canonical example. The pure renderer-side port and its raster-independent checker produce this mapping; the animation itself is not a proof. The static contact sheet shows all four stages.
+ Verified transformation. The pure renderer-side port and its raster-independent checker produce this mapping; the animation itself is not a proof. The static contact sheet shows all four stages.
## Project convention
diff --git a/docs/yang_zhang_builder_design.md b/docs/yang_zhang_builder_design.md
index 8309720..fe460b0 100644
--- a/docs/yang_zhang_builder_design.md
+++ b/docs/yang_zhang_builder_design.md
@@ -47,9 +47,9 @@ transport, and rendering have separate contracts.
- 
+
- Canonical example. The frames reveal spans from the versioned native construction sidecar; they are not timestamps from an instrumented builder. The static contact sheet shows all six stages.
+ Canonical construction. The frames reveal spans from the versioned native construction sidecar; they are not timestamps from an instrumented builder. The static contact sheet shows all six stages.
## 1. Module boundary
diff --git a/examples/run-cases-v2/pipeline-unsat-search.json b/examples/run-cases-v2/pipeline-unsat-search.json
new file mode 100644
index 0000000..d0c09a3
--- /dev/null
+++ b/examples/run-cases-v2/pipeline-unsat-search.json
@@ -0,0 +1,18 @@
+{
+ "schema": "wang-run-case-v2",
+ "id": "pipeline-unsat-search-v2",
+ "title": "Separate UNSAT full-pipeline search capture",
+ "purpose": "Capture the named engines and observed native search for pipeline_unsat_search.cm13 without presenting it as part of the canonical SAT worked example.",
+ "source": "tests/instances/pipeline_unsat_search.cm13",
+ "expected_status": "unsat",
+ "reference_trace": {
+ "event_capacity": 8192,
+ "checkpoint_interval": 128,
+ "checkpoint_capacity": 64
+ },
+ "optimized_trace": {
+ "event_capacity": 8192,
+ "checkpoint_interval": 128,
+ "checkpoint_capacity": 64
+ }
+}
diff --git a/python/dossier/multi_engine.py b/python/dossier/multi_engine.py
index d6b0432..8e3413c 100644
--- a/python/dossier/multi_engine.py
+++ b/python/dossier/multi_engine.py
@@ -271,7 +271,7 @@ def generate_multi_engine_dossier(
case_path: str | Path,
output_directory: str | Path,
) -> Path:
- """Capture all named engines once and atomically install the raw v2 dossier."""
+ """Capture all named engines once and atomically install the complete v2 dossier."""
case: MultiEngineRunCase = load_run_case_v2(case_path, ROOT)
destination = Path(output_directory).resolve()
if destination.exists():
@@ -410,8 +410,32 @@ def generate_multi_engine_dossier(
timings_ns=timings_ns,
artifacts=artifacts,
)
- _write_atomic(staging / "run.json", _encode_document(run_document))
- load_run_dossier_v2(staging / "run.json")
+ run_path = staging / "run.json"
+ _write_atomic(run_path, _encode_document(run_document))
+ load_run_dossier_v2(run_path)
+ from dossier.narrative_assets import (
+ NarrativeAssetError,
+ attach_narrative_assets,
+ generate_narrative_assets,
+ )
+
+ try:
+ narrative_manifest = generate_narrative_assets(
+ run_path,
+ staging / "assets/narrative",
+ product="run-specific",
+ )
+ run_document = attach_narrative_assets(
+ run_document,
+ staging,
+ narrative_manifest,
+ )
+ except NarrativeAssetError as error:
+ raise MultiEngineDossierError(
+ f"shared narrative asset pass failed: {error}"
+ ) from error
+ _write_atomic(run_path, _encode_document(run_document))
+ load_run_dossier_v2(run_path)
_install_directory(staging, destination)
return destination
except Exception:
diff --git a/python/dossier/narrative_assets.py b/python/dossier/narrative_assets.py
new file mode 100644
index 0000000..b560a2a
--- /dev/null
+++ b/python/dossier/narrative_assets.py
@@ -0,0 +1,754 @@
+"""Generate one fixed shared-asset bundle from a validated v2 dossier."""
+
+from __future__ import annotations
+
+import argparse
+import copy
+import hashlib
+import os
+from pathlib import Path
+import shutil
+import subprocess
+import tempfile
+
+
+ROOT = Path(__file__).resolve().parents[2]
+RENDERER = ROOT / "renderer"
+MECHANISM_SOURCE = RENDERER / "data/optimized-mechanisms-v1.json"
+
+from formats.narrative_assets import (
+ ANIMATION_NAMES,
+ CANONICAL_PAGES_CASE,
+ GENERALIZED_SPECIFICATION_SHA256,
+ IDENTITY_NAMES,
+ OPTIMIZED_MECHANISMS_SHA256,
+ SCHEMA_NAME,
+ STATIC_NAMES,
+ composite_source_sha256,
+ generalized_source_sha256,
+ generalized_presentation_source_sha256,
+ hex_presentation_source_sha256,
+ load_narrative_assets,
+ pipeline_source_sha256,
+ verification_source_sha256,
+ witness_presentation_source_sha256,
+)
+from formats.pipeline_snapshot import _encode_document, _write_atomic
+from formats.run_dossier_v2 import validate_run_dossier_v2
+from formats.run_dossier_v2_bundle import load_run_dossier_v2
+
+
+class NarrativeAssetError(RuntimeError):
+ """The downstream shared-asset pass failed before atomic installation."""
+
+
+def _verification_receipts(run: dict[str, object]) -> dict[str, object]:
+ return {
+ "schema": "wang-verification-receipts-v1",
+ "expected_status": run["case"]["expected_status"],
+ "verification": run["verification"],
+ "agreement": run["agreement"],
+ "source_sha256": verification_source_sha256(run),
+ }
+
+
+def _run_renderer(
+ arguments: list[str], *, required_outputs: tuple[str, ...] = ()
+) -> dict[str, Path]:
+ uv = shutil.which("uv")
+ if uv is None:
+ raise NarrativeAssetError("uv is required to run the isolated renderer")
+ try:
+ completed = subprocess.run(
+ [uv, "run", "--locked", "python", *arguments],
+ cwd=RENDERER,
+ check=True,
+ capture_output=True,
+ text=True,
+ timeout=180,
+ )
+ except (OSError, subprocess.SubprocessError) as error:
+ detail = getattr(error, "stderr", "") or getattr(error, "stdout", "") or str(error)
+ raise NarrativeAssetError(f"narrative renderer failed: {detail.strip()}") from error
+ outputs: dict[str, Path] = {}
+ for line in completed.stdout.splitlines():
+ if "=" not in line:
+ continue
+ name, value = line.split("=", 1)
+ outputs[name] = Path(value)
+ missing = tuple(name for name in required_outputs if name not in outputs)
+ if missing:
+ raise NarrativeAssetError(
+ "narrative renderer omitted required output keys: " + ", ".join(missing)
+ )
+ return outputs
+
+
+def _artifact(root: Path, path: Path, media_type: str) -> dict[str, str]:
+ try:
+ encoded = path.read_bytes()
+ relative = path.relative_to(root).as_posix()
+ except (OSError, ValueError) as error:
+ raise NarrativeAssetError(f"cannot bind narrative artifact {path!s}: {error}") from error
+ return {
+ "path": relative,
+ "sha256": hashlib.sha256(encoded).hexdigest(),
+ "media_type": media_type,
+ }
+
+
+def _metadata(
+ *,
+ owner: str,
+ semantic_label: str,
+ caption: str,
+ alt_text: str,
+ source_contract: str,
+ source_sha256: str,
+ producer: str,
+ validator: str,
+ compositor: str,
+) -> dict[str, str]:
+ return {
+ "owner": owner,
+ "semantic_label": semantic_label,
+ "caption": caption,
+ "alt_text": alt_text,
+ "source_contract": source_contract,
+ "source_sha256": source_sha256,
+ "producer": producer,
+ "validator": validator,
+ "compositor": compositor,
+ }
+
+
+def _animation_record(
+ root: Path,
+ directory: Path,
+ fallback: Path,
+ metadata: dict[str, str],
+ *,
+ complete: bool,
+ selected: bool,
+) -> dict[str, object]:
+ frames = tuple(sorted(directory.glob("frame-*.png")))
+ if not frames or fallback not in frames:
+ raise NarrativeAssetError("renderer did not publish a selected fallback frame")
+ animation = directory / "trace.gif"
+ contact_sheet = directory / "contact-sheet.png"
+ return {
+ **metadata,
+ "scope": {
+ "complete": complete,
+ "selected": selected,
+ "truncated": False,
+ },
+ "animation": _artifact(root, animation, "image/gif"),
+ "fallback": _artifact(root, fallback, "image/png"),
+ "contact_sheet": _artifact(root, contact_sheet, "image/png"),
+ "frames": [_artifact(root, frame, "image/png") for frame in frames],
+ }
+
+
+def _static_record(
+ root: Path,
+ path: Path,
+ metadata: dict[str, str],
+) -> dict[str, object]:
+ return {**metadata, "artifact": _artifact(root, path, "image/png")}
+
+
+def _run_artifact(
+ run_root: Path, run: dict[str, object], name: str
+) -> Path | None:
+ record = run["artifacts"][name]
+ if record is None:
+ return None
+ return run_root / record["path"]
+
+
+def _identities(run: dict[str, object]) -> dict[str, str | None]:
+ identities: dict[str, str | None] = {
+ "source_formula": run["source"]["sha256"],
+ "formula_snapshot": run["reduction"]["formula_sha256"],
+ "tileset": run["reduction"]["tileset_sha256"],
+ "region": run["reduction"]["region_sha256"],
+ "provenance": run["reduction"]["provenance_sha256"],
+ "boolean_z3_summary": run["boolean_z3"]["encoding_summary_sha256"],
+ "reference_trace_manifest": run["reference"]["trace"]["manifest_sha256"],
+ "reference_trace": run["reference"]["trace"]["trace_sha256"],
+ "reference_solution": run["reference"]["solution_sha256"],
+ "optimized_trace_manifest": run["optimized"]["trace"]["manifest_sha256"],
+ "optimized_trace": run["optimized"]["trace"]["trace_sha256"],
+ "optimized_solution": run["optimized"]["solution_sha256"],
+ "wang_z3_summary": run["wang_z3"]["encoding_summary_sha256"],
+ }
+ if tuple(identities) != IDENTITY_NAMES:
+ raise NarrativeAssetError("narrative identity order diverged from contract")
+ return identities
+
+
+def _animation_metadata(
+ identities: dict[str, str | None],
+ run: dict[str, object],
+) -> dict[str, dict[str, str]]:
+ pipeline_digest = pipeline_source_sha256(identities, run)
+ mechanism_digest = hashlib.sha256(MECHANISM_SOURCE.read_bytes()).hexdigest()
+ if mechanism_digest != OPTIMIZED_MECHANISMS_SHA256:
+ raise NarrativeAssetError(
+ "optimized mechanism source changed without a narrative contract version"
+ )
+ return {
+ "pipeline_overview": _metadata(
+ owner="/pipeline/",
+ semantic_label="observed",
+ caption="One validated v2 capture in fixed component order.",
+ alt_text="The captured formula moves through Boolean Z3, Yang-Zhang reduction, both native solvers, Wang Z3, verification, and presentation.",
+ source_contract="wang-run-dossier-v2#named-components",
+ source_sha256=pipeline_digest,
+ producer="dossier.narrative_assets",
+ validator="formats.run_dossier_v2_bundle.load_run_dossier_v2",
+ compositor="renderer.wang_narrative.render_overview_assets",
+ ),
+ "boolean_z3": _metadata(
+ owner="/components/boolean-z3/",
+ semantic_label="encoding-order",
+ caption="Project-owned Boolean constraint construction and returned assignment.",
+ alt_text="Four frames add Boolean variables and source-order exactly-one clauses before showing the copied result.",
+ source_contract="z3-encoding-summary-v1",
+ source_sha256=str(identities["boolean_z3_summary"]),
+ producer="formats.z3_encoding_summary.build_boolean_z3_summary",
+ validator="renderer.wang_z3_summary.load_z3_encoding_summary",
+ compositor="renderer.wang_z3_summary.render_boolean_z3_assets",
+ ),
+ "region_construction": _metadata(
+ owner="/components/yang-zhang/",
+ semantic_label="canonical-construction",
+ caption="Native Yang-Zhang gadget spans accumulated over the observed region.",
+ alt_text="Six frames reveal variable, forwarding, crossover, and clause gadget spans on the same region.",
+ source_contract="wang-reduction-explanation-v1",
+ source_sha256=str(identities["provenance"]),
+ producer="formats.solver_trace_snapshot.dump_solver_trace_bundle",
+ validator="renderer.wang_snapshot.load_explainability_bundle",
+ compositor="renderer.wang_algorithm_animation.render_builder_assets",
+ ),
+ "reference_trace": _metadata(
+ owner="/components/reference-solver/",
+ semantic_label="observed",
+ caption="Selected semantic milestones from the complete reference trace.",
+ alt_text="Observed reference domain states at root, propagation, decision, search, and result milestones.",
+ source_contract="wang-explain-manifest-v3",
+ source_sha256=str(identities["reference_trace_manifest"]),
+ producer="formats.solver_trace_snapshot.dump_solver_trace_bundle",
+ validator="renderer.wang_trace.load_trace_bundle",
+ compositor="renderer.wang_trace_render.render_trace_assets",
+ ),
+ "optimized_trace": _metadata(
+ owner="/components/optimized-solver/",
+ semantic_label="observed",
+ caption="Selected semantic milestones from the complete optimized trace.",
+ alt_text="Observed optimized domain states at root, propagation, decision, search, and result milestones.",
+ source_contract="wang-explain-manifest-v3",
+ source_sha256=str(identities["optimized_trace_manifest"]),
+ producer="formats.solver_trace_snapshot.dump_solver_trace_bundle",
+ validator="renderer.wang_trace.load_trace_bundle",
+ compositor="renderer.wang_trace_render.render_trace_assets",
+ ),
+ "wang_z3": _metadata(
+ owner="/components/wang-z3/",
+ semantic_label="encoding-order",
+ caption="Project-owned Wang edge-term construction and returned model.",
+ alt_text="Five frames add edge terms, shared internal edges, tile relations, boundaries, and the copied result.",
+ source_contract="z3-encoding-summary-v1",
+ source_sha256=str(identities["wang_z3_summary"]),
+ producer="formats.z3_encoding_summary.build_wang_z3_summary",
+ validator="renderer.wang_z3_summary.load_z3_encoding_summary",
+ compositor="renderer.wang_z3_summary.render_wang_z3_assets",
+ ),
+ "verification": _metadata(
+ owner="/components/verification/",
+ semantic_label="observed",
+ caption="The six named independent checker records from the captured run.",
+ alt_text="Six frames report Boolean, native, and Wang Z3 witness checks without rerunning a verifier.",
+ source_contract="wang-run-dossier-v2#verification",
+ source_sha256=verification_source_sha256(run),
+ producer="formats.run_dossier_v2_builder.build_run_dossier_v2",
+ validator="formats.run_dossier_v2.validate_run_dossier_v2+renderer.wang_narrative._load_verification",
+ compositor="renderer.wang_narrative.render_verification_assets",
+ ),
+ "witness_presentation": _metadata(
+ owner="/components/visualization/",
+ semantic_label="verified-transformation",
+ caption="Verified square witness, exact generalized overlay, and checked hex port.",
+ alt_text="Four frames move from the verified square witness through generalized recognition to the checked hex presentation.",
+ source_contract="wang-solution-v1+wang-generalized-tiles-v1+checked-square-to-hex",
+ source_sha256=witness_presentation_source_sha256(
+ str(identities["reference_solution"])
+ ),
+ producer="formats.solver_trace_snapshot.dump_solver_trace_bundle",
+ validator="renderer.wang_square.load_wang_presentation+renderer.wang_generalized.recognize_generalized_tiles+renderer.wang_hex_port.check_square_to_hex",
+ compositor="renderer.wang_narrative.render_witness_assets",
+ ),
+ "optimized_mechanisms": _metadata(
+ owner="/components/optimized-solver/",
+ semantic_label="didactic",
+ caption="The six retained serial mechanisms, including the lazy MRV index.",
+ alt_text="Seven didactic frames contrast the reference baseline with six measured optimized mechanisms.",
+ source_contract="wang-optimized-mechanisms-v1",
+ source_sha256=mechanism_digest,
+ producer="renderer/data/optimized-mechanisms-v1.json",
+ validator="renderer.wang_algorithm_animation._load_optimizations",
+ compositor="renderer.wang_algorithm_animation.render_optimized_assets",
+ ),
+ }
+
+
+def _static_metadata(
+ identities: dict[str, str | None],
+ run: dict[str, object],
+) -> dict[str, dict[str, str]]:
+ generalized_digest = generalized_source_sha256(str(identities["tileset"]))
+ solution_digest = str(identities["reference_solution"])
+ common = {"producer": "dossier.narrative_assets"}
+ return {
+ "home_preview": _metadata(
+ owner="/",
+ semantic_label="observed",
+ caption="Selected verified SAT square output for the captured instance.",
+ alt_text="A compact square Wang witness preview for the captured SAT source.",
+ source_contract="wang-solution-v1",
+ source_sha256=solution_digest,
+ validator="formats.run_dossier_v2_bundle.load_run_dossier_v2",
+ compositor="renderer.wang_narrative.render_overview_assets",
+ **common,
+ ),
+ "worked_example": _metadata(
+ owner="/worked-example/",
+ semantic_label="observed",
+ caption="Static t0 through tn component milestones for one SAT run.",
+ alt_text="Eight static panels follow the captured source from formula to checked presentation.",
+ source_contract="wang-run-dossier-v2#named-components",
+ source_sha256=pipeline_source_sha256(identities, run),
+ validator="formats.run_dossier_v2_bundle.load_run_dossier_v2",
+ compositor="renderer.wang_narrative.render_overview_assets",
+ **common,
+ ),
+ "formula": _metadata(
+ owner="/worked-example/",
+ semantic_label="observed",
+ caption="Parsed formula snapshot for the named canonical source.",
+ alt_text="The parsed CM1-in-3 formula and its source-order clauses.",
+ source_contract="cm13-formula-snapshot-v1",
+ source_sha256=str(identities["formula_snapshot"]),
+ validator="renderer.wang_snapshot.load_explainability_bundle",
+ compositor="renderer.wang_snapshot.render_pipeline_snapshot",
+ **common,
+ ),
+ "generalized_sheet": _metadata(
+ owner="/components/tileset/",
+ semantic_label="canonical-construction",
+ caption="The exact 14 generalized tiles decomposed into 23 positional atomic IDs.",
+ alt_text="A sheet of fourteen Yang-Zhang generalized tiles with internal seams and atomic identifiers.",
+ source_contract="wang-generalized-tiles-v1+wang-tileset-snapshot-v1",
+ source_sha256=generalized_digest,
+ validator="renderer.wang_snapshot.load_explainability_bundle+renderer.wang_generalized.check_canonical_atomic_tileset",
+ compositor="renderer.wang_narrative.render_generalized_assets",
+ **common,
+ ),
+ "atomic_legend": _metadata(
+ owner="/components/tileset/",
+ semantic_label="canonical-construction",
+ caption="All 23 atomic IDs with symbolic paper colors and generalized roles.",
+ alt_text="A semantic legend for twenty-three positional Wang tiles and their edge colors.",
+ source_contract="wang-generalized-tiles-v1+wang-tileset-snapshot-v1",
+ source_sha256=generalized_digest,
+ validator="renderer.wang_snapshot.load_explainability_bundle+renderer.wang_generalized.check_canonical_atomic_tileset",
+ compositor="renderer.wang_narrative.render_generalized_assets",
+ **common,
+ ),
+ "square_presentation": _metadata(
+ owner="/components/visualization/",
+ semantic_label="observed",
+ caption="The independently verified square witness with atomic IDs and boundaries.",
+ alt_text="The complete square Wang witness for the captured SAT source.",
+ source_contract="wang-solution-v1",
+ source_sha256=solution_digest,
+ validator="renderer.wang_square.load_wang_presentation",
+ compositor="renderer.wang_narrative.render_witness_assets",
+ **common,
+ ),
+ "generalized_presentation": _metadata(
+ owner="/components/visualization/",
+ semantic_label="canonical-construction",
+ caption="Exact generalized contours over the same verified square witness.",
+ alt_text="The square witness grouped into exact Yang-Zhang generalized tile occurrences.",
+ source_contract="wang-solution-v1+wang-generalized-tiles-v1",
+ source_sha256=generalized_presentation_source_sha256(solution_digest),
+ validator="renderer.wang_square.load_wang_presentation+renderer.wang_generalized.recognize_generalized_tiles",
+ compositor="renderer.wang_narrative.render_witness_assets",
+ **common,
+ ),
+ "hex_presentation": _metadata(
+ owner="/components/visualization/",
+ semantic_label="verified-transformation",
+ caption="The checked Basire/Culik square-to-hex port of the same witness.",
+ alt_text="A pointy-top hex presentation preserving the square witness cells, edges, and boundary.",
+ source_contract="wang-solution-v1+checked-square-to-hex",
+ source_sha256=hex_presentation_source_sha256(solution_digest),
+ validator="renderer.wang_square.load_wang_presentation+renderer.wang_hex_port.check_square_to_hex",
+ compositor="renderer.wang_narrative.render_witness_assets",
+ **common,
+ ),
+ "presentation_status": _metadata(
+ owner="/run-dossiers/",
+ semantic_label="observed",
+ caption="UNSAT has no witness-only presentation artifacts.",
+ alt_text="A notice that square, generalized, and hex witness views are not applicable to the UNSAT run.",
+ source_contract="wang-run-dossier-v2#agreement",
+ source_sha256=verification_source_sha256(run),
+ validator="formats.run_dossier_v2_bundle.load_run_dossier_v2",
+ compositor="renderer.wang_narrative.render_presentation_status",
+ **common,
+ ),
+ }
+
+
+def _install_directory(staging: Path, destination: Path) -> None:
+ os.replace(staging, destination)
+
+
+def attach_narrative_assets(
+ run: dict[str, object],
+ dossier_root: str | Path,
+ manifest_path: str | Path,
+) -> dict[str, object]:
+ """Bind selected milestones and the three reserved static presentations."""
+ updated = copy.deepcopy(run)
+ root = Path(dossier_root).resolve()
+ manifest_file = Path(manifest_path).resolve()
+ manifest = load_narrative_assets(manifest_file, updated)
+ if manifest["product"] != "run-specific":
+ raise NarrativeAssetError("only run-specific assets can be attached to run.json")
+ for solver, animation_name in (
+ ("reference", "reference_trace"),
+ ("optimized", "optimized_trace"),
+ ):
+ selected = len(manifest["animations"][animation_name]["frames"])
+ updated[solver]["trace"]["selection"] = {
+ "performed": True,
+ "selected_event_count": selected,
+ }
+
+ if updated["case"]["expected_status"] == "sat":
+ specifications = {
+ "square": (
+ "observed verified square witness presentation",
+ "observed",
+ ),
+ "generalized": (
+ "exact generalized overlay on the verified square witness",
+ "canonical-construction",
+ ),
+ "hex": (
+ "checked square-to-hex witness presentation",
+ "verified-transformation",
+ ),
+ }
+ for name, (role, semantics) in specifications.items():
+ static = manifest["statics"][f"{name}_presentation"]["artifact"]
+ absolute = manifest_file.parent / static["path"]
+ try:
+ relative = absolute.relative_to(root).as_posix()
+ except ValueError as error:
+ raise NarrativeAssetError(
+ f"{name} presentation lies outside dossier"
+ ) from error
+ artifact_name = f"{name}_presentation"
+ updated["artifacts"][artifact_name] = {
+ "path": relative,
+ "sha256": static["sha256"],
+ "media_type": "image/png",
+ "schema": None,
+ "role": role,
+ "semantics": semantics,
+ "form": "static",
+ "source_sha256": updated["source"]["sha256"],
+ }
+ updated["presentation"][name]["artifact"] = artifact_name
+ validate_run_dossier_v2(updated)
+ return updated
+
+
+def generate_narrative_assets(
+ run_path: str | Path,
+ output_directory: str | Path,
+ *,
+ product: str = "run-specific",
+) -> Path:
+ """Render one fixed asset pass and atomically install its closed manifest."""
+ run_file = Path(run_path).resolve()
+ run = load_run_dossier_v2(run_file)
+ if product not in {"run-specific", "canonical-pages"}:
+ raise NarrativeAssetError(f"unsupported asset product: {product}")
+ if product == "canonical-pages" and {
+ "id": run["case"]["id"],
+ "expected_status": run["case"]["expected_status"],
+ "source_sha256": run["source"]["sha256"],
+ } != CANONICAL_PAGES_CASE:
+ raise NarrativeAssetError(
+ "canonical-pages is reserved for the canonical pipeline SAT case"
+ )
+ destination = Path(output_directory).resolve()
+ if destination.exists():
+ raise NarrativeAssetError(f"output directory already exists: {destination!s}")
+ destination.parent.mkdir(parents=True, exist_ok=True)
+ staging = Path(tempfile.mkdtemp(prefix=f".{destination.name}.", dir=destination.parent))
+ try:
+ run_root = run_file.parent
+ reference_manifest = _run_artifact(run_root, run, "reference_trace_manifest")
+ optimized_manifest = _run_artifact(run_root, run, "optimized_trace_manifest")
+ boolean_summary = _run_artifact(run_root, run, "boolean_z3_summary")
+ wang_summary = _run_artifact(run_root, run, "wang_z3_summary")
+ if None in (reference_manifest, optimized_manifest, boolean_summary, wang_summary):
+ raise NarrativeAssetError("v2 run is missing a required narrative source")
+
+ formula_path = staging / "formula.png"
+ _run_renderer(
+ ["wang_square.py", str(reference_manifest), str(formula_path), "--view", "formula"]
+ )
+ boolean_outputs = _run_renderer(
+ ["wang_z3_summary.py", str(boolean_summary), str(staging / "boolean-z3")],
+ required_outputs=("fallback",),
+ )
+ region_outputs = _run_renderer(
+ [
+ "wang_algorithm_animation.py",
+ "builder",
+ str(reference_manifest),
+ str(staging / "region-construction"),
+ ],
+ required_outputs=("fallback",),
+ )
+ reference_outputs = _run_renderer(
+ [
+ "wang_trace_render.py",
+ str(reference_manifest),
+ str(staging / "reference-trace"),
+ "--max-frames",
+ "10",
+ ],
+ required_outputs=("fallback",),
+ )
+ optimized_outputs = _run_renderer(
+ [
+ "wang_trace_render.py",
+ str(optimized_manifest),
+ str(staging / "optimized-trace"),
+ "--max-frames",
+ "10",
+ ],
+ required_outputs=("fallback",),
+ )
+ wang_outputs = _run_renderer(
+ ["wang_z3_summary.py", str(wang_summary), str(staging / "wang-z3")],
+ required_outputs=("fallback",),
+ )
+ verification_receipts = staging / ".verification-receipts.json"
+ _write_atomic(
+ verification_receipts,
+ _encode_document(_verification_receipts(run)),
+ )
+ verification_outputs = _run_renderer(
+ [
+ "wang_narrative.py",
+ "verification",
+ str(verification_receipts),
+ str(staging / "verification"),
+ ],
+ required_outputs=("fallback",),
+ )
+ verification_receipts.unlink()
+ mechanism_outputs = _run_renderer(
+ ["wang_algorithm_animation.py", "optimized", str(staging / "optimized-mechanisms")],
+ required_outputs=("fallback",),
+ )
+ generalized_outputs = _run_renderer(
+ [
+ "wang_narrative.py",
+ "generalized",
+ str(reference_manifest),
+ str(staging / "generalized-tiles"),
+ ],
+ required_outputs=("spec_sha256",),
+ )
+ if str(generalized_outputs.get("spec_sha256", "")) != GENERALIZED_SPECIFICATION_SHA256:
+ raise NarrativeAssetError(
+ "renderer generalized specification disagrees with the narrative contract"
+ )
+
+ status = run["case"]["expected_status"]
+ witness_outputs: dict[str, Path] | None = None
+ if status == "sat":
+ solution = _run_artifact(run_root, run, "reference_solution")
+ if solution is None:
+ raise NarrativeAssetError("SAT narrative assets require a reference solution")
+ witness_outputs = _run_renderer(
+ ["wang_narrative.py", "witness", str(solution), str(staging / "presentation")],
+ required_outputs=("square", "generalized", "hex", "fallback"),
+ )
+ presentation_source = witness_outputs["hex"]
+ home_source = witness_outputs["square"]
+ else:
+ presentation_source = staging / "presentation-status.png"
+ _run_renderer(
+ ["wang_narrative.py", "status", "unsat", str(presentation_source)]
+ )
+ home_source = presentation_source
+
+ overview_arguments = [
+ "wang_narrative.py",
+ "overview",
+ str(staging / "pipeline-overview"),
+ str(formula_path),
+ str(boolean_outputs["fallback"]),
+ str(region_outputs["fallback"]),
+ str(reference_outputs["fallback"]),
+ str(optimized_outputs["fallback"]),
+ str(wang_outputs["fallback"]),
+ str(verification_outputs["fallback"]),
+ str(presentation_source),
+ "--home-source",
+ str(home_source),
+ ]
+ if status == "unsat":
+ overview_arguments.append("--omit-sat-story")
+ overview_required = ("fallback",)
+ if status == "sat":
+ overview_required += ("home_preview", "worked_example")
+ overview_outputs = _run_renderer(
+ overview_arguments, required_outputs=overview_required
+ )
+
+ identities = _identities(run)
+ animation_metadata = _animation_metadata(identities, run)
+ animation_directories = {
+ "pipeline_overview": (staging / "pipeline-overview", overview_outputs),
+ "boolean_z3": (staging / "boolean-z3", boolean_outputs),
+ "region_construction": (staging / "region-construction", region_outputs),
+ "reference_trace": (staging / "reference-trace", reference_outputs),
+ "optimized_trace": (staging / "optimized-trace", optimized_outputs),
+ "wang_z3": (staging / "wang-z3", wang_outputs),
+ "verification": (staging / "verification", verification_outputs),
+ "witness_presentation": (
+ None if witness_outputs is None else staging / "presentation",
+ witness_outputs,
+ ),
+ "optimized_mechanisms": (staging / "optimized-mechanisms", mechanism_outputs),
+ }
+ animations: dict[str, dict[str, object] | None] = {}
+ for name in ANIMATION_NAMES:
+ directory, outputs = animation_directories[name]
+ if directory is None or outputs is None:
+ animations[name] = None
+ continue
+ animations[name] = _animation_record(
+ staging,
+ directory,
+ outputs["fallback"],
+ animation_metadata[name],
+ complete=True,
+ selected=name
+ in {
+ "pipeline_overview",
+ "region_construction",
+ "reference_trace",
+ "optimized_trace",
+ },
+ )
+
+ static_metadata = _static_metadata(identities, run)
+ static_paths: dict[str, Path | None] = {
+ "home_preview": overview_outputs.get("home_preview"),
+ "worked_example": overview_outputs.get("worked_example"),
+ "formula": formula_path,
+ "generalized_sheet": staging / "generalized-tiles/sheet.png",
+ "atomic_legend": staging / "generalized-tiles/atomic-legend.png",
+ "square_presentation": None if witness_outputs is None else witness_outputs["square"],
+ "generalized_presentation": None
+ if witness_outputs is None
+ else witness_outputs["generalized"],
+ "hex_presentation": None if witness_outputs is None else witness_outputs["hex"],
+ "presentation_status": presentation_source if status == "unsat" else None,
+ }
+ statics: dict[str, dict[str, object] | None] = {
+ name: None
+ if static_paths[name] is None
+ else _static_record(staging, static_paths[name], static_metadata[name])
+ for name in STATIC_NAMES
+ }
+ manifest = {
+ "schema": SCHEMA_NAME,
+ "product": product,
+ "case": {
+ "id": run["case"]["id"],
+ "expected_status": status,
+ "source_sha256": run["source"]["sha256"],
+ },
+ "identities": identities,
+ "animations": animations,
+ "statics": statics,
+ "pdf_milestones": {
+ "selector": "semantic-milestones-v1",
+ "region_construction": [
+ item["path"] for item in animations["region_construction"]["frames"]
+ ],
+ "reference_trace": [
+ item["path"] for item in animations["reference_trace"]["frames"]
+ ],
+ "optimized_trace": [
+ item["path"] for item in animations["optimized_trace"]["frames"]
+ ],
+ "end_to_end": [
+ item["path"] for item in animations["pipeline_overview"]["frames"]
+ ],
+ },
+ }
+ manifest_path = staging / "manifest.json"
+ _write_atomic(manifest_path, _encode_document(manifest))
+ load_narrative_assets(manifest_path, run)
+ _install_directory(staging, destination)
+ return destination / "manifest.json"
+ except Exception:
+ shutil.rmtree(staging, ignore_errors=True)
+ raise
+
+
+def _parser() -> argparse.ArgumentParser:
+ parser = argparse.ArgumentParser(
+ description="generate one closed shared narrative asset bundle from a v2 run"
+ )
+ parser.add_argument("run", type=Path)
+ parser.add_argument("output_directory", type=Path)
+ parser.add_argument(
+ "--product",
+ choices=("run-specific", "canonical-pages"),
+ default="run-specific",
+ )
+ return parser
+
+
+def main(arguments: list[str] | None = None) -> int:
+ parser = _parser()
+ args = parser.parse_args(arguments)
+ try:
+ manifest = generate_narrative_assets(
+ args.run, args.output_directory, product=args.product
+ )
+ except (NarrativeAssetError, OSError, ValueError) as error:
+ parser.error(str(error))
+ print(f"manifest={manifest}")
+ return 0
+
+
+if __name__ == "__main__":
+ raise SystemExit(main())
diff --git a/python/formats/narrative_assets.py b/python/formats/narrative_assets.py
new file mode 100644
index 0000000..27e69b0
--- /dev/null
+++ b/python/formats/narrative_assets.py
@@ -0,0 +1,692 @@
+"""Closed manifest for shared narrative assets derived from one v2 run."""
+
+from __future__ import annotations
+
+import hashlib
+from pathlib import Path
+from typing import Final
+
+from formats.pipeline_snapshot import (
+ PipelineSnapshotError,
+ _encode_document,
+ _load_json_bytes,
+ _require_exact_fields,
+ _require_literal,
+ _require_object,
+ _require_sha256,
+)
+from formats.run_contract import _boolean, _nonempty_string, _relative_path
+from formats.run_dossier_v2 import validate_run_dossier_v2
+
+
+SCHEMA_NAME: Final = "wang-narrative-assets-v1"
+OPTIMIZED_MECHANISMS_SHA256: Final = (
+ "5f0c6e1f80601f6112ae8e358fe8029fa3d94fd260693edf0b37ea474419f212"
+)
+GENERALIZED_SPECIFICATION_SHA256: Final = (
+ "5e8e6589271f9059b5ed81df00db4e303b338d5243caa475ed09135b129e3cf2"
+)
+HEX_TRANSFORMATION_ID: Final = "basire-culik-square-to-hex-v1"
+CANONICAL_PAGES_CASE: Final = {
+ "id": "pipeline-sat-v2",
+ "expected_status": "sat",
+ "source_sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542",
+}
+PRODUCTS: Final = frozenset({"run-specific", "canonical-pages"})
+SEMANTIC_LABELS: Final = frozenset(
+ {
+ "observed",
+ "canonical-construction",
+ "encoding-order",
+ "verified-transformation",
+ "didactic",
+ }
+)
+ANIMATION_NAMES: Final = (
+ "pipeline_overview",
+ "boolean_z3",
+ "region_construction",
+ "reference_trace",
+ "optimized_trace",
+ "wang_z3",
+ "verification",
+ "witness_presentation",
+ "optimized_mechanisms",
+)
+STATIC_NAMES: Final = (
+ "home_preview",
+ "worked_example",
+ "formula",
+ "generalized_sheet",
+ "atomic_legend",
+ "square_presentation",
+ "generalized_presentation",
+ "hex_presentation",
+ "presentation_status",
+)
+IDENTITY_NAMES: Final = (
+ "source_formula",
+ "formula_snapshot",
+ "tileset",
+ "region",
+ "provenance",
+ "boolean_z3_summary",
+ "reference_trace_manifest",
+ "reference_trace",
+ "reference_solution",
+ "optimized_trace_manifest",
+ "optimized_trace",
+ "optimized_solution",
+ "wang_z3_summary",
+)
+_ARTIFACT_FIELDS = frozenset({"path", "sha256", "media_type"})
+_ANIMATION_FIELDS = frozenset(
+ {
+ "owner",
+ "semantic_label",
+ "caption",
+ "alt_text",
+ "source_contract",
+ "source_sha256",
+ "producer",
+ "validator",
+ "compositor",
+ "scope",
+ "animation",
+ "fallback",
+ "contact_sheet",
+ "frames",
+ }
+)
+_STATIC_FIELDS = frozenset(
+ {
+ "owner",
+ "semantic_label",
+ "caption",
+ "alt_text",
+ "source_contract",
+ "source_sha256",
+ "producer",
+ "validator",
+ "compositor",
+ "artifact",
+ }
+)
+_ANIMATION_POLICY: Final = {
+ "pipeline_overview": ("/pipeline/", "observed"),
+ "boolean_z3": ("/components/boolean-z3/", "encoding-order"),
+ "region_construction": ("/components/yang-zhang/", "canonical-construction"),
+ "reference_trace": ("/components/reference-solver/", "observed"),
+ "optimized_trace": ("/components/optimized-solver/", "observed"),
+ "wang_z3": ("/components/wang-z3/", "encoding-order"),
+ "verification": ("/components/verification/", "observed"),
+ "witness_presentation": (
+ "/components/visualization/",
+ "verified-transformation",
+ ),
+ "optimized_mechanisms": ("/components/optimized-solver/", "didactic"),
+}
+_STATIC_POLICY: Final = {
+ "home_preview": ("/", "observed"),
+ "worked_example": ("/worked-example/", "observed"),
+ "formula": ("/worked-example/", "observed"),
+ "generalized_sheet": ("/components/tileset/", "canonical-construction"),
+ "atomic_legend": ("/components/tileset/", "canonical-construction"),
+ "square_presentation": ("/components/visualization/", "observed"),
+ "generalized_presentation": (
+ "/components/visualization/",
+ "canonical-construction",
+ ),
+ "hex_presentation": (
+ "/components/visualization/",
+ "verified-transformation",
+ ),
+ "presentation_status": ("/run-dossiers/", "observed"),
+}
+_SELECTED_ANIMATIONS: Final = frozenset(
+ {
+ "pipeline_overview",
+ "region_construction",
+ "reference_trace",
+ "optimized_trace",
+ }
+)
+_ANIMATION_TOOLCHAIN: Final = {
+ "pipeline_overview": (
+ "dossier.narrative_assets",
+ "formats.run_dossier_v2_bundle.load_run_dossier_v2",
+ "renderer.wang_narrative.render_overview_assets",
+ ),
+ "boolean_z3": (
+ "formats.z3_encoding_summary.build_boolean_z3_summary",
+ "renderer.wang_z3_summary.load_z3_encoding_summary",
+ "renderer.wang_z3_summary.render_boolean_z3_assets",
+ ),
+ "region_construction": (
+ "formats.solver_trace_snapshot.dump_solver_trace_bundle",
+ "renderer.wang_snapshot.load_explainability_bundle",
+ "renderer.wang_algorithm_animation.render_builder_assets",
+ ),
+ "reference_trace": (
+ "formats.solver_trace_snapshot.dump_solver_trace_bundle",
+ "renderer.wang_trace.load_trace_bundle",
+ "renderer.wang_trace_render.render_trace_assets",
+ ),
+ "optimized_trace": (
+ "formats.solver_trace_snapshot.dump_solver_trace_bundle",
+ "renderer.wang_trace.load_trace_bundle",
+ "renderer.wang_trace_render.render_trace_assets",
+ ),
+ "wang_z3": (
+ "formats.z3_encoding_summary.build_wang_z3_summary",
+ "renderer.wang_z3_summary.load_z3_encoding_summary",
+ "renderer.wang_z3_summary.render_wang_z3_assets",
+ ),
+ "verification": (
+ "formats.run_dossier_v2_builder.build_run_dossier_v2",
+ "formats.run_dossier_v2.validate_run_dossier_v2+renderer.wang_narrative._load_verification",
+ "renderer.wang_narrative.render_verification_assets",
+ ),
+ "witness_presentation": (
+ "formats.solver_trace_snapshot.dump_solver_trace_bundle",
+ "renderer.wang_square.load_wang_presentation+renderer.wang_generalized.recognize_generalized_tiles+renderer.wang_hex_port.check_square_to_hex",
+ "renderer.wang_narrative.render_witness_assets",
+ ),
+ "optimized_mechanisms": (
+ "renderer/data/optimized-mechanisms-v1.json",
+ "renderer.wang_algorithm_animation._load_optimizations",
+ "renderer.wang_algorithm_animation.render_optimized_assets",
+ ),
+}
+_STATIC_TOOLCHAIN: Final = {
+ "home_preview": (
+ "dossier.narrative_assets",
+ "formats.run_dossier_v2_bundle.load_run_dossier_v2",
+ "renderer.wang_narrative.render_overview_assets",
+ ),
+ "worked_example": (
+ "dossier.narrative_assets",
+ "formats.run_dossier_v2_bundle.load_run_dossier_v2",
+ "renderer.wang_narrative.render_overview_assets",
+ ),
+ "formula": (
+ "dossier.narrative_assets",
+ "renderer.wang_snapshot.load_explainability_bundle",
+ "renderer.wang_snapshot.render_pipeline_snapshot",
+ ),
+ "generalized_sheet": (
+ "dossier.narrative_assets",
+ "renderer.wang_snapshot.load_explainability_bundle+renderer.wang_generalized.check_canonical_atomic_tileset",
+ "renderer.wang_narrative.render_generalized_assets",
+ ),
+ "atomic_legend": (
+ "dossier.narrative_assets",
+ "renderer.wang_snapshot.load_explainability_bundle+renderer.wang_generalized.check_canonical_atomic_tileset",
+ "renderer.wang_narrative.render_generalized_assets",
+ ),
+ "square_presentation": (
+ "dossier.narrative_assets",
+ "renderer.wang_square.load_wang_presentation",
+ "renderer.wang_narrative.render_witness_assets",
+ ),
+ "generalized_presentation": (
+ "dossier.narrative_assets",
+ "renderer.wang_square.load_wang_presentation+renderer.wang_generalized.recognize_generalized_tiles",
+ "renderer.wang_narrative.render_witness_assets",
+ ),
+ "hex_presentation": (
+ "dossier.narrative_assets",
+ "renderer.wang_square.load_wang_presentation+renderer.wang_hex_port.check_square_to_hex",
+ "renderer.wang_narrative.render_witness_assets",
+ ),
+ "presentation_status": (
+ "dossier.narrative_assets",
+ "formats.run_dossier_v2_bundle.load_run_dossier_v2",
+ "renderer.wang_narrative.render_presentation_status",
+ ),
+}
+
+
+def verification_source_sha256(run: dict[str, object]) -> str:
+ return hashlib.sha256(
+ _encode_document(
+ {
+ "verification": run["verification"],
+ "agreement": run["agreement"],
+ }
+ )
+ ).hexdigest()
+
+
+def composite_source_sha256(values: dict[str, str]) -> str:
+ return hashlib.sha256(_encode_document(values)).hexdigest()
+
+
+def generalized_source_sha256(tileset_sha256: str) -> str:
+ return composite_source_sha256(
+ {
+ "tileset": tileset_sha256,
+ "generalized_specification": GENERALIZED_SPECIFICATION_SHA256,
+ }
+ )
+
+
+def generalized_presentation_source_sha256(solution_sha256: str) -> str:
+ return composite_source_sha256(
+ {
+ "solution": solution_sha256,
+ "generalized_specification": GENERALIZED_SPECIFICATION_SHA256,
+ }
+ )
+
+
+def hex_presentation_source_sha256(solution_sha256: str) -> str:
+ return composite_source_sha256(
+ {
+ "solution": solution_sha256,
+ "transformation": HEX_TRANSFORMATION_ID,
+ }
+ )
+
+
+def witness_presentation_source_sha256(solution_sha256: str) -> str:
+ return composite_source_sha256(
+ {
+ "solution": solution_sha256,
+ "generalized_specification": GENERALIZED_SPECIFICATION_SHA256,
+ "transformation": HEX_TRANSFORMATION_ID,
+ }
+ )
+
+
+def pipeline_source_sha256(
+ identities: dict[str, str | None], run: dict[str, object]
+) -> str:
+ sources = {
+ name: digest for name, digest in identities.items() if digest is not None
+ }
+ sources["verification"] = verification_source_sha256(run)
+ sources["generalized_specification"] = GENERALIZED_SPECIFICATION_SHA256
+ sources["square_to_hex_transformation"] = HEX_TRANSFORMATION_ID
+ return composite_source_sha256(sources)
+
+
+def _artifact(
+ value: object,
+ path: str,
+ root: Path,
+ *,
+ media_type: str,
+) -> str:
+ artifact = _require_object(value, path)
+ _require_exact_fields(artifact, _ARTIFACT_FIELDS, path)
+ relative = _relative_path(artifact["path"], f"{path}.path")
+ _require_sha256(artifact["sha256"], f"{path}.sha256")
+ _require_literal(artifact["media_type"], media_type, f"{path}.media_type")
+ try:
+ unresolved = root / relative
+ cursor = root
+ for component in Path(relative).parts:
+ cursor /= component
+ if cursor.is_symlink():
+ raise PipelineSnapshotError(f"{path}.path: symlinks are forbidden")
+ candidate = unresolved.resolve(strict=True)
+ if not candidate.is_relative_to(root) or not candidate.is_file():
+ raise PipelineSnapshotError(f"{path}.path: escapes asset bundle")
+ encoded = candidate.read_bytes()
+ except PipelineSnapshotError:
+ raise
+ except OSError as error:
+ raise PipelineSnapshotError(f"{path}.path: cannot read artifact: {error}") from error
+ if hashlib.sha256(encoded).hexdigest() != artifact["sha256"]:
+ raise PipelineSnapshotError(f"{path}.sha256: does not match file")
+ return relative
+
+
+def _metadata(
+ value: dict[str, object],
+ path: str,
+ policy: tuple[str, str],
+ toolchain: tuple[str, str, str],
+) -> None:
+ owner, semantic_label = policy
+ _require_literal(value["owner"], owner, f"{path}.owner")
+ label = _nonempty_string(value["semantic_label"], f"{path}.semantic_label")
+ if label not in SEMANTIC_LABELS or label != semantic_label:
+ raise PipelineSnapshotError(f"{path}.semantic_label: disagrees with policy")
+ for name in ("caption", "alt_text", "source_contract"):
+ _nonempty_string(value[name], f"{path}.{name}")
+ for name, expected in zip(
+ ("producer", "validator", "compositor"), toolchain, strict=True
+ ):
+ _require_literal(value[name], expected, f"{path}.{name}")
+ _require_sha256(value["source_sha256"], f"{path}.source_sha256")
+
+
+def validate_narrative_assets(
+ document: object,
+ manifest_path: str | Path,
+) -> dict[str, set[str]]:
+ manifest = _require_object(document, "$")
+ _require_exact_fields(
+ manifest,
+ frozenset(
+ {
+ "schema",
+ "product",
+ "case",
+ "identities",
+ "animations",
+ "statics",
+ "pdf_milestones",
+ }
+ ),
+ "$",
+ )
+ _require_literal(manifest["schema"], SCHEMA_NAME, "$.schema")
+ product = _nonempty_string(manifest["product"], "$.product")
+ if product not in PRODUCTS:
+ raise PipelineSnapshotError("$.product: is unsupported")
+ case = _require_object(manifest["case"], "$.case")
+ _require_exact_fields(
+ case, frozenset({"id", "expected_status", "source_sha256"}), "$.case"
+ )
+ _nonempty_string(case["id"], "$.case.id")
+ status = _nonempty_string(case["expected_status"], "$.case.expected_status")
+ if status not in {"sat", "unsat"}:
+ raise PipelineSnapshotError("$.case.expected_status: is unsupported")
+ _require_sha256(case["source_sha256"], "$.case.source_sha256")
+ if product == "canonical-pages" and case != CANONICAL_PAGES_CASE:
+ raise PipelineSnapshotError(
+ "$.case: canonical-pages is reserved for the canonical SAT run"
+ )
+
+ identities = _require_object(manifest["identities"], "$.identities")
+ _require_exact_fields(identities, frozenset(IDENTITY_NAMES), "$.identities")
+ for name in IDENTITY_NAMES:
+ value = identities[name]
+ if value is None:
+ if status == "sat" or not name.endswith("_solution"):
+ raise PipelineSnapshotError(f"$.identities.{name}: may not be null")
+ else:
+ _require_sha256(value, f"$.identities.{name}")
+
+ root = Path(manifest_path).parent.resolve(strict=True)
+ animations = _require_object(manifest["animations"], "$.animations")
+ _require_exact_fields(animations, frozenset(ANIMATION_NAMES), "$.animations")
+ owned_paths: set[str] = set()
+ frame_paths: dict[str, tuple[str, ...]] = {}
+ for name in ANIMATION_NAMES:
+ path = f"$.animations.{name}"
+ raw = animations[name]
+ if raw is None:
+ if name != "witness_presentation" or status != "unsat":
+ raise PipelineSnapshotError(f"{path}: is required")
+ frame_paths[name] = ()
+ continue
+ record = _require_object(raw, path)
+ _require_exact_fields(record, _ANIMATION_FIELDS, path)
+ _metadata(record, path, _ANIMATION_POLICY[name], _ANIMATION_TOOLCHAIN[name])
+ scope = _require_object(record["scope"], f"{path}.scope")
+ _require_exact_fields(
+ scope, frozenset({"complete", "selected", "truncated"}), f"{path}.scope"
+ )
+ if not _boolean(scope["complete"], f"{path}.scope.complete"):
+ raise PipelineSnapshotError(f"{path}.scope.complete: must remain true")
+ selected = _boolean(scope["selected"], f"{path}.scope.selected")
+ if selected != (name in _SELECTED_ANIMATIONS):
+ raise PipelineSnapshotError(f"{path}.scope.selected: disagrees with policy")
+ if _boolean(scope["truncated"], f"{path}.scope.truncated"):
+ raise PipelineSnapshotError(f"{path}.scope.truncated: must remain false")
+ animation_path = _artifact(
+ record["animation"], f"{path}.animation", root, media_type="image/gif"
+ )
+ contact_path = _artifact(
+ record["contact_sheet"],
+ f"{path}.contact_sheet",
+ root,
+ media_type="image/png",
+ )
+ raw_frames = record["frames"]
+ if type(raw_frames) is not list or not raw_frames:
+ raise PipelineSnapshotError(f"{path}.frames: must be a nonempty array")
+ ordered_paths = tuple(
+ _artifact(item, f"{path}.frames[{index}]", root, media_type="image/png")
+ for index, item in enumerate(raw_frames)
+ )
+ paths = set(ordered_paths)
+ if len(paths) != len(ordered_paths):
+ raise PipelineSnapshotError(f"{path}.frames: contains duplicate paths")
+ fallback_path = _artifact(
+ record["fallback"], f"{path}.fallback", root, media_type="image/png"
+ )
+ if fallback_path not in paths:
+ raise PipelineSnapshotError(f"{path}.fallback: must select one frame")
+ newly_owned = paths | {animation_path, contact_path}
+ overlap = owned_paths & newly_owned
+ if overlap:
+ raise PipelineSnapshotError(f"{path}: reuses files owned by another asset")
+ owned_paths.update(newly_owned)
+ frame_paths[name] = ordered_paths
+
+ statics = _require_object(manifest["statics"], "$.statics")
+ _require_exact_fields(statics, frozenset(STATIC_NAMES), "$.statics")
+ sat_only = {
+ "home_preview",
+ "worked_example",
+ "square_presentation",
+ "generalized_presentation",
+ "hex_presentation",
+ }
+ for name in STATIC_NAMES:
+ path = f"$.statics.{name}"
+ raw = statics[name]
+ if raw is None:
+ allowed = (status == "unsat" and name in sat_only) or (
+ status == "sat" and name == "presentation_status"
+ )
+ if not allowed:
+ raise PipelineSnapshotError(f"{path}: is required")
+ continue
+ if (status == "sat" and name == "presentation_status") or (
+ status == "unsat" and name in sat_only
+ ):
+ raise PipelineSnapshotError(f"{path}: disagrees with SAT applicability")
+ record = _require_object(raw, path)
+ _require_exact_fields(record, _STATIC_FIELDS, path)
+ _metadata(record, path, _STATIC_POLICY[name], _STATIC_TOOLCHAIN[name])
+ artifact_path = _artifact(
+ record["artifact"], f"{path}.artifact", root, media_type="image/png"
+ )
+ if artifact_path in owned_paths:
+ raise PipelineSnapshotError(f"{path}: reuses a file owned by another asset")
+ owned_paths.add(artifact_path)
+
+ milestones = _require_object(manifest["pdf_milestones"], "$.pdf_milestones")
+ _require_exact_fields(
+ milestones,
+ frozenset(
+ {
+ "selector",
+ "region_construction",
+ "reference_trace",
+ "optimized_trace",
+ "end_to_end",
+ }
+ ),
+ "$.pdf_milestones",
+ )
+ _require_literal(
+ milestones["selector"], "semantic-milestones-v1", "$.pdf_milestones.selector"
+ )
+ milestone_sources = {
+ "region_construction": "region_construction",
+ "reference_trace": "reference_trace",
+ "optimized_trace": "optimized_trace",
+ "end_to_end": "pipeline_overview",
+ }
+ for name, animation_name in milestone_sources.items():
+ values = milestones[name]
+ if type(values) is not list or not values:
+ raise PipelineSnapshotError(f"$.pdf_milestones.{name}: must be nonempty")
+ if any(type(value) is not str for value in values):
+ raise PipelineSnapshotError(f"$.pdf_milestones.{name}: paths must be strings")
+ if tuple(values) != frame_paths[animation_name]:
+ raise PipelineSnapshotError(
+ f"$.pdf_milestones.{name}: must exactly preserve the shared frame order"
+ )
+ if any(not value.endswith(".png") for value in values):
+ raise PipelineSnapshotError(f"$.pdf_milestones.{name}: GIF is forbidden")
+ return frame_paths
+
+
+def load_narrative_assets(
+ manifest_path: str | Path,
+ run_document: dict[str, object],
+) -> dict[str, object]:
+ validate_run_dossier_v2(run_document)
+ path = Path(manifest_path)
+ if path.is_symlink():
+ raise PipelineSnapshotError("narrative manifest may not be a symlink")
+ try:
+ document = _load_json_bytes(path.read_bytes(), str(path))
+ except OSError as error:
+ raise PipelineSnapshotError(f"cannot read narrative manifest: {error}") from error
+ validate_narrative_assets(document, path)
+ if document["case"] != {
+ "id": run_document["case"]["id"],
+ "expected_status": run_document["case"]["expected_status"],
+ "source_sha256": run_document["source"]["sha256"],
+ }:
+ raise PipelineSnapshotError("narrative case identity disagrees with run")
+ expected_identities = {
+ "source_formula": run_document["source"]["sha256"],
+ "formula_snapshot": run_document["reduction"]["formula_sha256"],
+ "tileset": run_document["reduction"]["tileset_sha256"],
+ "region": run_document["reduction"]["region_sha256"],
+ "provenance": run_document["reduction"]["provenance_sha256"],
+ "boolean_z3_summary": run_document["boolean_z3"]["encoding_summary_sha256"],
+ "reference_trace_manifest": run_document["reference"]["trace"]["manifest_sha256"],
+ "reference_trace": run_document["reference"]["trace"]["trace_sha256"],
+ "reference_solution": run_document["reference"]["solution_sha256"],
+ "optimized_trace_manifest": run_document["optimized"]["trace"]["manifest_sha256"],
+ "optimized_trace": run_document["optimized"]["trace"]["trace_sha256"],
+ "optimized_solution": run_document["optimized"]["solution_sha256"],
+ "wang_z3_summary": run_document["wang_z3"]["encoding_summary_sha256"],
+ }
+ if document["identities"] != expected_identities:
+ raise PipelineSnapshotError("narrative component identities disagree with run")
+ animations = document["animations"]
+ pipeline_digest = pipeline_source_sha256(expected_identities, run_document)
+ generalized_digest = generalized_source_sha256(
+ expected_identities["tileset"]
+ )
+ expected_sources = {
+ "pipeline_overview": (
+ "wang-run-dossier-v2#named-components",
+ pipeline_digest,
+ ),
+ "boolean_z3": ("z3-encoding-summary-v1", expected_identities["boolean_z3_summary"]),
+ "region_construction": (
+ "wang-reduction-explanation-v1",
+ expected_identities["provenance"],
+ ),
+ "reference_trace": (
+ "wang-explain-manifest-v3",
+ expected_identities["reference_trace_manifest"],
+ ),
+ "optimized_trace": (
+ "wang-explain-manifest-v3",
+ expected_identities["optimized_trace_manifest"],
+ ),
+ "wang_z3": ("z3-encoding-summary-v1", expected_identities["wang_z3_summary"]),
+ "verification": (
+ "wang-run-dossier-v2#verification",
+ verification_source_sha256(run_document),
+ ),
+ "optimized_mechanisms": (
+ "wang-optimized-mechanisms-v1",
+ OPTIMIZED_MECHANISMS_SHA256,
+ ),
+ }
+ if run_document["case"]["expected_status"] == "sat":
+ expected_sources["witness_presentation"] = (
+ "wang-solution-v1+wang-generalized-tiles-v1+checked-square-to-hex",
+ witness_presentation_source_sha256(
+ expected_identities["reference_solution"]
+ ),
+ )
+ for name, (contract, digest) in expected_sources.items():
+ record = animations[name]
+ if record["source_contract"] != contract or record["source_sha256"] != digest:
+ raise PipelineSnapshotError(f"narrative source {name} disagrees with run")
+
+ solution_digest = expected_identities["reference_solution"]
+ expected_static_sources = {
+ "formula": (
+ "cm13-formula-snapshot-v1",
+ expected_identities["formula_snapshot"],
+ ),
+ "generalized_sheet": (
+ "wang-generalized-tiles-v1+wang-tileset-snapshot-v1",
+ generalized_digest,
+ ),
+ "atomic_legend": (
+ "wang-generalized-tiles-v1+wang-tileset-snapshot-v1",
+ generalized_digest,
+ ),
+ }
+ if run_document["case"]["expected_status"] == "sat":
+ assert solution_digest is not None
+ expected_static_sources.update(
+ {
+ "home_preview": ("wang-solution-v1", solution_digest),
+ "worked_example": (
+ "wang-run-dossier-v2#named-components",
+ pipeline_digest,
+ ),
+ "square_presentation": ("wang-solution-v1", solution_digest),
+ "generalized_presentation": (
+ "wang-solution-v1+wang-generalized-tiles-v1",
+ generalized_presentation_source_sha256(solution_digest),
+ ),
+ "hex_presentation": (
+ "wang-solution-v1+checked-square-to-hex",
+ hex_presentation_source_sha256(solution_digest),
+ ),
+ }
+ )
+ else:
+ expected_static_sources["presentation_status"] = (
+ "wang-run-dossier-v2#agreement",
+ verification_source_sha256(run_document),
+ )
+ for name, (contract, digest) in expected_static_sources.items():
+ record = document["statics"][name]
+ if record["source_contract"] != contract or record["source_sha256"] != digest:
+ raise PipelineSnapshotError(
+ f"narrative static source {name} disagrees with run"
+ )
+ if (
+ document["product"] == "run-specific"
+ and run_document["case"]["expected_status"] == "sat"
+ ):
+ for name in ("square", "generalized", "hex"):
+ narrative_artifact = document["statics"][f"{name}_presentation"][
+ "artifact"
+ ]
+ run_artifact = run_document["artifacts"][f"{name}_presentation"]
+ expected_run_path = (
+ Path("assets/narrative") / narrative_artifact["path"]
+ ).as_posix()
+ if (
+ run_artifact is not None
+ and (
+ run_artifact["path"] != expected_run_path
+ or run_artifact["sha256"] != narrative_artifact["sha256"]
+ )
+ ):
+ raise PipelineSnapshotError(
+ f"narrative {name} presentation disagrees with run artifact"
+ )
+ return document
diff --git a/python/formats/run_dossier_v2_bundle.py b/python/formats/run_dossier_v2_bundle.py
index 40b090e..0639683 100644
--- a/python/formats/run_dossier_v2_bundle.py
+++ b/python/formats/run_dossier_v2_bundle.py
@@ -201,4 +201,60 @@ def load_run_dossier_v2(path: str | Path) -> dict[str, object]:
raise PipelineSnapshotError("Boolean Z3 witness digest mismatch")
if document["wang_z3"]["witness_sha256"] != witness_sha256(wang_cells):
raise PipelineSnapshotError("Wang Z3 witness digest mismatch")
+ narrative_path = run_path.parent / "assets/narrative/manifest.json"
+ narrative_expected = any(
+ document[solver]["trace"]["selection"]["performed"]
+ for solver in ("reference", "optimized")
+ ) or any(
+ document["artifacts"][f"{name}_presentation"] is not None
+ for name in ("square", "generalized", "hex")
+ )
+ if narrative_expected and not narrative_path.is_file():
+ raise PipelineSnapshotError(
+ "selected narrative assets require assets/narrative/manifest.json"
+ )
+ if narrative_path.is_file():
+ cursor = run_path.parent
+ for component in Path("assets/narrative/manifest.json").parts:
+ cursor /= component
+ if cursor.is_symlink():
+ raise PipelineSnapshotError(
+ "assets/narrative and its manifest may not contain symlinks"
+ )
+ try:
+ resolved_narrative = narrative_path.resolve(strict=True)
+ except OSError as error:
+ raise PipelineSnapshotError(
+ f"cannot resolve narrative manifest: {error}"
+ ) from error
+ if not resolved_narrative.is_relative_to(root):
+ raise PipelineSnapshotError("narrative manifest escapes dossier")
+ from formats.narrative_assets import load_narrative_assets
+
+ narrative = load_narrative_assets(resolved_narrative, document)
+ if narrative["product"] != "run-specific":
+ raise PipelineSnapshotError(
+ "a dossier may contain only a run-specific narrative manifest"
+ )
+ for solver, animation_name in (
+ ("reference", "reference_trace"),
+ ("optimized", "optimized_trace"),
+ ):
+ selection = document[solver]["trace"]["selection"]
+ selected = len(narrative["animations"][animation_name]["frames"])
+ if not selection["performed"]:
+ raise PipelineSnapshotError(
+ f"{solver} narrative manifest requires a performed selection"
+ )
+ if selection["selected_event_count"] != selected:
+ raise PipelineSnapshotError(
+ f"{solver} selected event count disagrees with narrative manifest"
+ )
+ if document["case"]["expected_status"] == "sat" and any(
+ document["artifacts"][f"{name}_presentation"] is None
+ for name in ("square", "generalized", "hex")
+ ):
+ raise PipelineSnapshotError(
+ "SAT narrative manifest requires all presentation artifacts"
+ )
return document
diff --git a/renderer/README.md b/renderer/README.md
index 10a237e..20f8aa8 100644
--- a/renderer/README.md
+++ b/renderer/README.md
@@ -220,20 +220,24 @@ dossier generator reuse one trace bundle without synthesizing a second v1/v2
manifest. The renderer still imports neither native code nor Z3, and it does
not own LaTeX or report metadata.
-Z3 uses a separate `encoding-order` summary. The renderer shows the explicit
-project-owned row-major constraint construction and returned model, never an
-internal Z3 search or debug trace:
+Z3 uses separate `encoding-order` summaries. The same offline consumer renders
+the explicit project-owned Boolean source-order construction or Wang row-major
+construction and returned model, never an internal Z3 search or debug trace:
```bash
+uv run --locked python wang_z3_summary.py \
+ ../tests/fixtures/pipeline_sat_z3/boolean-z3.json \
+ output/boolean-z3-encoding
uv run --locked python wang_z3_summary.py \
../tests/fixtures/pipeline_sat_z3/wang-z3.json \
output/z3-encoding
```
-Three additional commands make their source semantics explicit: builder and
-hex are `canonical-example` views over versioned data and pure checked
-transformation respectively; optimized is a `didactic` overview whose dated
-reports, not the animation, establish performance.
+Three additional commands make their source semantics explicit: builder is a
+`canonical-construction`, hex is a `verified-transformation`, and optimized is
+a `didactic` overview whose dated reports, not the animation, establish
+performance. The optimized source is the closed six-entry
+`data/optimized-mechanisms-v1.json`, including the lazy MRV index.
```bash
uv run --locked python wang_algorithm_animation.py builder \
@@ -246,6 +250,20 @@ uv run --locked python wang_algorithm_animation.py hex \
output/square-to-hex
```
+`wang_narrative.py` adds only fixed downstream compositions for verification,
+the square/generalized/hex witness sequence, the generalized sheet and legend,
+and the eight-component overview. The root shared-asset generator invokes
+these commands after validating `run.json`; no renderer imports native code,
+Z3, Pages, or LaTeX. SAT and UNSAT records use the same pipeline order, while
+UNSAT emits an explicit not-applicable presentation instead of a witness.
+
+The trace frame selector is `semantic-milestones-v1`: it retains phase
+transitions, propagation, decisions, conflicts, backtracks, terminal state,
+and decision/backtrack reductions before filling the widest remaining replay
+gaps. It is deterministic and deliberately not uniform time sampling. The
+selected states are still composed from the same single validated replay used
+for PNG frames, the reduced-motion fallback, contact sheet, and GIF.
+
All loaders reject unknown fields and identity drift before rasterization. No
animation module imports native code; trace rendering and algorithm rendering
do not import Z3. PNG sources are the deterministic test oracles. GIFs exist
@@ -406,6 +424,8 @@ Raises `RenderingException` on pipeline errors.
├── wang_generalized_render.py # Sheet, atomic legend, and square overlay
├── wang_animation.py # Deterministic PNG/contact-sheet/GIF encoder
├── wang_algorithm_animation.py # Canonical and didactic algorithm views
+├── wang_narrative.py # Verification, witness, overview, and PDF-milestone compositions
+├── data/optimized-mechanisms-v1.json # Closed six-mechanism didactic source
├── test_wang_square.py # Square loader, raster, isolation, CLI, and failures
├── test_wang_hex.py # Port proof obligations, hex raster, golden, and CLI
├── test_wang_snapshot.py # Snapshot contracts, views, isolation, and goldens
@@ -413,6 +433,7 @@ Raises `RenderingException` on pipeline errors.
├── test_wang_z3_summary.py # Fixed encoding summaries and byte stability
├── test_wang_generalized.py # Exact mapping, rejection, isolation, and goldens
├── test_wang_algorithm_animation.py # Source checks and animation goldens
+├── test_wang_narrative.py # Shared narrative compositions and accessibility fallbacks
├── input/ # Example input files (palette, scene, tiles, sprites)
├── output/ # Rendered PNG output goes here
├── test_data/
@@ -437,10 +458,10 @@ Raises `RenderingException` on pipeline errors.
uv run --locked pytest -q
```
-The complete isolated suite has 283 tests: the 144 preserved legacy tests
+The complete isolated suite has 290 tests: the 144 preserved legacy tests
below, 45 Wang square tests, 24 square-to-hex/hex-raster tests, 29 static
snapshot/explainability tests, 21 generalized-presentation tests, and 20
-trace/Z3/algorithm-animation tests.
+trace/Z3/algorithm-animation tests plus 7 narrative/semantic-selection tests.
To run only the original upstream suite:
```bash
diff --git a/renderer/data/optimized-mechanisms-v1.json b/renderer/data/optimized-mechanisms-v1.json
new file mode 100644
index 0000000..21de611
--- /dev/null
+++ b/renderer/data/optimized-mechanisms-v1.json
@@ -0,0 +1,41 @@
+{
+ "schema": "wang-optimized-mechanisms-v1",
+ "mechanisms": [
+ {
+ "id": "dynamic-dfs-stack",
+ "title": "Dynamic DFS stack",
+ "description": "grow from 16 frames instead of reserving all active cells",
+ "evidence_route": "/solver_dynamic_stack_2026-08-17/"
+ },
+ {
+ "id": "initial-trail-omission",
+ "title": "Initial trail omission",
+ "description": "do not store undo entries that search cannot consume",
+ "evidence_route": "/solver_initial_trail_2026-08-17/"
+ },
+ {
+ "id": "sat-ownership-transfer",
+ "title": "SAT ownership transfer",
+ "description": "publish the verified domain buffer without a result copy",
+ "evidence_route": "/solver_sat_ownership_2026-08-20/"
+ },
+ {
+ "id": "byte-support-table",
+ "title": "Byte support table",
+ "description": "aggregate compatible tiles through three byte lookups",
+ "evidence_route": "/solver_byte_support_2026-08-20/"
+ },
+ {
+ "id": "queue-deduplication",
+ "title": "Queue deduplication",
+ "description": "suppress an enqueue while the cell is already pending",
+ "evidence_route": "/solver_queue_dedup_2026-08-20/"
+ },
+ {
+ "id": "lazy-mrv-index",
+ "title": "Lazy MRV index",
+ "description": "select after the root from private packed domain-size buckets",
+ "evidence_route": "/solver_mrv_index_2026-08-28/"
+ }
+ ]
+}
diff --git a/renderer/test_wang_algorithm_animation.py b/renderer/test_wang_algorithm_animation.py
index ddcea16..3c9331f 100644
--- a/renderer/test_wang_algorithm_animation.py
+++ b/renderer/test_wang_algorithm_animation.py
@@ -63,13 +63,13 @@ def test_optimized_didactic_animation_is_byte_stable(tmp_path):
first = render_optimized_assets(tmp_path / "first")
render_optimized_assets(tmp_path / "second")
- assert first.fallback.name == "frame-05.png"
+ assert first.fallback.name == "frame-06.png"
_assert_stable_assets(
tmp_path / "first",
tmp_path / "second",
GOLDENS / "optimized-mechanisms",
- frame_count=6,
- fallback_name="frame-05.png",
+ frame_count=7,
+ fallback_name="frame-06.png",
)
@@ -91,5 +91,5 @@ def test_cli_reports_animation_and_fallback(tmp_path, capsys):
assert main(["optimized", str(tmp_path)]) == 0
assert capsys.readouterr().out.splitlines() == [
f"animation={tmp_path / 'trace.gif'}",
- f"fallback={tmp_path / 'frame-05.png'}",
+ f"fallback={tmp_path / 'frame-06.png'}",
]
diff --git a/renderer/test_wang_narrative.py b/renderer/test_wang_narrative.py
new file mode 100644
index 0000000..88d60f9
--- /dev/null
+++ b/renderer/test_wang_narrative.py
@@ -0,0 +1,145 @@
+from __future__ import annotations
+
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+from PIL import Image
+import pytest
+
+from wang_hex_port import WangSquareRenderError
+from wang_generalized import generalized_specification_sha256
+from wang_narrative import (
+ render_generalized_assets,
+ render_overview_assets,
+ render_presentation_status,
+ render_verification_assets,
+ render_witness_assets,
+)
+
+
+RENDERER = Path(__file__).resolve().parent
+ROOT = RENDERER.parent
+MANIFEST = ROOT / "tests/fixtures/pipeline_sat_reduction_explain/manifest.json"
+SOLUTION = ROOT / "tests/fixtures/wang_solution_v1_square_sat.json"
+
+
+def _tree_bytes(directory: Path) -> dict[str, bytes]:
+ return {
+ path.relative_to(directory).as_posix(): path.read_bytes()
+ for path in directory.rglob("*")
+ if path.is_file()
+ }
+
+
+def _run_record(status: str) -> dict[str, object]:
+ performed = status == "sat"
+ checks = {}
+ specifications = (
+ ("boolean_z3_assignment", "oracles.witness_check.is_valid_assignment"),
+ ("reference_tiling", "oracles.tiling_check.is_valid_tiling"),
+ ("reference_assignment", "oracles.witness_check.is_valid_assignment"),
+ ("optimized_tiling", "oracles.tiling_check.is_valid_tiling"),
+ ("optimized_assignment", "oracles.witness_check.is_valid_assignment"),
+ ("wang_z3_tiling", "oracles.tiling_check.is_valid_tiling"),
+ )
+ for name, checker in specifications:
+ checks[name] = {
+ "checker": checker,
+ "performed": performed,
+ "passed": True if performed else None,
+ "witness_sha256": "1" * 64 if performed else None,
+ }
+ agreement = {
+ "expected_status": status,
+ "boolean_z3_status": status,
+ "reference_status": status,
+ "optimized_status": status,
+ "wang_z3_status": status,
+ "all_status_equal": True,
+ "sat_witnesses_valid": True if status == "sat" else None,
+ "passed": True,
+ }
+ payload = {"verification": checks, "agreement": agreement}
+ source_sha256 = hashlib.sha256(
+ (json.dumps(payload, ensure_ascii=False, allow_nan=False, indent=2) + "\n").encode(
+ "utf-8"
+ )
+ ).hexdigest()
+ return {
+ "schema": "wang-verification-receipts-v1",
+ "expected_status": status,
+ **payload,
+ "source_sha256": source_sha256,
+ }
+
+
+def test_verification_composition_is_deterministic_for_sat_and_unsat(tmp_path):
+ for status in ("sat", "unsat"):
+ run = tmp_path / f"{status}.json"
+ run.write_text(json.dumps(_run_record(status)) + "\n", encoding="utf-8")
+ first = render_verification_assets(run, tmp_path / f"{status}-first")
+ render_verification_assets(run, tmp_path / f"{status}-second")
+ assert _tree_bytes(tmp_path / f"{status}-first") == _tree_bytes(
+ tmp_path / f"{status}-second"
+ )
+ assert first.fallback.name == "frame-05.png"
+ with Image.open(first.animation) as animation:
+ assert animation.n_frames == 6
+
+
+def test_verification_composition_rejects_partial_or_forged_receipts(tmp_path):
+ source = tmp_path / "forged.json"
+ document = _run_record("sat")
+ del document["agreement"]["reference_status"]
+ source.write_text(json.dumps(document) + "\n", encoding="utf-8")
+ with pytest.raises(WangSquareRenderError, match="agreement must be closed"):
+ render_verification_assets(source, tmp_path / "output")
+
+
+def test_witness_and_generalized_assets_reuse_checked_presentations(tmp_path):
+ first = render_witness_assets(SOLUTION, tmp_path / "witness-first")
+ render_witness_assets(SOLUTION, tmp_path / "witness-second")
+ assert _tree_bytes(tmp_path / "witness-first") == _tree_bytes(
+ tmp_path / "witness-second"
+ )
+ assert first.animation.fallback.name == "frame-03.png"
+ assert first.square.is_file()
+ assert first.generalized.is_file()
+ assert first.hex.is_file()
+
+ generalized = render_generalized_assets(MANIFEST, tmp_path / "generalized")
+ assert generalized.sheet.is_file()
+ assert generalized.legend.is_file()
+ assert generalized_specification_sha256() == (
+ "5e8e6589271f9059b5ed81df00db4e303b338d5243caa475ed09135b129e3cf2"
+ )
+
+
+def test_overview_and_unsat_status_are_static_fallback_safe(tmp_path):
+ status = render_presentation_status("unsat", tmp_path / "status.png")
+ sources = (status,) * 8
+ first = render_overview_assets(
+ sources,
+ status,
+ tmp_path / "overview-first",
+ include_sat_story=False,
+ )
+ render_overview_assets(
+ sources,
+ status,
+ tmp_path / "overview-second",
+ include_sat_story=False,
+ )
+ assert _tree_bytes(tmp_path / "overview-first") == _tree_bytes(
+ tmp_path / "overview-second"
+ )
+ assert first.home_preview is None
+ assert first.worked_example is None
+ assert first.animation.contact_sheet.is_file()
+
+
+def test_narrative_module_imports_no_native_or_z3_producer():
+ assert "z3" not in sys.modules
+ assert not any(name.startswith("native") for name in sys.modules)
diff --git a/renderer/test_wang_trace.py b/renderer/test_wang_trace.py
index 180f5b2..c63c94c 100644
--- a/renderer/test_wang_trace.py
+++ b/renderer/test_wang_trace.py
@@ -13,7 +13,7 @@
from wang_hex_port import WangSquareRenderError
from wang_trace import TraceEvent, TraceSnapshot, load_trace_bundle, replay_trace
-from wang_trace_render import render_trace_assets
+from wang_trace_render import render_trace_assets, select_semantic_milestones
RENDERER = Path(__file__).resolve().parent
@@ -116,6 +116,16 @@ def test_one_composition_chain_is_byte_stable_for_png_sheet_and_gif(tmp_path):
assert animation.n_frames == 8
+def test_semantic_milestones_precede_gap_filling():
+ bundle = load_trace_bundle(MANIFEST)
+ selected = select_semantic_milestones(bundle.trace.events, 8)
+
+ assert selected == (0, 1, 2516, 2517, 2518, 2893, 2894, 2895)
+ assert selected != tuple(
+ slot * (len(bundle.trace.events) - 1) // 7 for slot in range(8)
+ )
+
+
def test_rejects_hash_tampering_before_parsing_trace(tmp_path):
copied = tmp_path / "bundle"
shutil.copytree(FIXTURE_DIRECTORY, copied)
diff --git a/renderer/test_wang_z3_summary.py b/renderer/test_wang_z3_summary.py
index 9319699..1f9b17d 100644
--- a/renderer/test_wang_z3_summary.py
+++ b/renderer/test_wang_z3_summary.py
@@ -8,7 +8,11 @@
import pytest
from wang_hex_port import WangSquareRenderError
-from wang_z3_summary import load_z3_encoding_summary, render_wang_z3_assets
+from wang_z3_summary import (
+ load_z3_encoding_summary,
+ render_boolean_z3_assets,
+ render_wang_z3_assets,
+)
RENDERER = Path(__file__).resolve().parent
@@ -53,6 +57,18 @@ def test_encoding_order_animation_is_byte_stable_and_matches_goldens(tmp_path):
assert animation.n_frames == 5
+def test_boolean_encoding_order_animation_is_byte_stable(tmp_path):
+ source = FIXTURES / "boolean-z3.json"
+ first = render_boolean_z3_assets(source, tmp_path / "first")
+ render_boolean_z3_assets(source, tmp_path / "second")
+
+ assert _tree_bytes(tmp_path / "first") == _tree_bytes(tmp_path / "second")
+ assert first.fallback.name == "frame-02.png"
+ with Image.open(first.animation) as animation:
+ assert animation.format == "GIF"
+ assert animation.n_frames == 4
+
+
def test_rejects_unknown_fields_and_cross_engine_region_identity(tmp_path):
source = json.loads(
(FIXTURES / "boolean-z3.json").read_text(encoding="utf-8")
diff --git a/renderer/wang_algorithm_animation.py b/renderer/wang_algorithm_animation.py
index 53687ec..828ed3a 100644
--- a/renderer/wang_algorithm_animation.py
+++ b/renderer/wang_algorithm_animation.py
@@ -3,6 +3,7 @@
from __future__ import annotations
import argparse
+import json
from pathlib import Path
from PIL import Image, ImageDraw
@@ -28,13 +29,52 @@
"right_forward": (169, 112, 191),
"clause": (214, 91, 91),
}
-_OPTIMIZATIONS = (
- ("Dynamic DFS stack", "grow from 16 frames instead of reserving all active cells"),
- ("Initial trail omission", "do not store undo entries that search cannot consume"),
- ("SAT ownership transfer", "publish the verified domain buffer without a result copy"),
- ("Byte support table", "aggregate compatible tiles through three byte lookups"),
- ("Queue deduplication", "suppress an enqueue while the cell is already pending"),
-)
+_OPTIMIZATION_SOURCE = Path(__file__).resolve().parent / "data/optimized-mechanisms-v1.json"
+
+
+def _load_optimizations() -> tuple[tuple[str, str], ...]:
+ try:
+ document = json.loads(_OPTIMIZATION_SOURCE.read_text(encoding="utf-8"))
+ except (OSError, UnicodeError, json.JSONDecodeError) as error:
+ raise WangSquareRenderError(
+ f"cannot load optimized mechanism source: {error}"
+ ) from error
+ if type(document) is not dict or set(document) != {"schema", "mechanisms"}:
+ raise WangSquareRenderError("optimized mechanism source must be closed")
+ if document["schema"] != "wang-optimized-mechanisms-v1":
+ raise WangSquareRenderError("optimized mechanism source schema is unsupported")
+ mechanisms = document["mechanisms"]
+ if type(mechanisms) is not list or len(mechanisms) != 6:
+ raise WangSquareRenderError("optimized mechanism source must contain six entries")
+ result: list[tuple[str, str]] = []
+ identifiers: list[str] = []
+ for index, item in enumerate(mechanisms):
+ if type(item) is not dict or set(item) != {
+ "id",
+ "title",
+ "description",
+ "evidence_route",
+ }:
+ raise WangSquareRenderError(
+ f"optimized mechanism entry {index} must be closed"
+ )
+ values = tuple(item.values())
+ if any(type(value) is not str or not value for value in values):
+ raise WangSquareRenderError(
+ f"optimized mechanism entry {index} requires nonempty strings"
+ )
+ if not item["evidence_route"].startswith("/"):
+ raise WangSquareRenderError(
+ f"optimized mechanism entry {index} has an invalid evidence route"
+ )
+ identifiers.append(item["id"])
+ result.append((item["title"], item["description"]))
+ if len(set(identifiers)) != len(identifiers) or identifiers[-1] != "lazy-mrv-index":
+ raise WangSquareRenderError("optimized mechanism IDs are invalid or incomplete")
+ return tuple(result)
+
+
+_OPTIMIZATIONS = _load_optimizations()
def _base_frame(title: str, subtitle: str, size: tuple[int, int]) -> tuple[Image.Image, ImageDraw.ImageDraw]:
@@ -49,7 +89,7 @@ def _builder_frame(bundle: object, stage: int) -> Image.Image:
assert reduction is not None
image, draw = _base_frame(
"Yang-Zhang construction provenance",
- f"canonical-example stage {stage + 1}/6 | actual gadget spans, not a timed builder trace",
+ f"canonical-construction stage {stage + 1}/6 | actual gadget spans, not a timed builder trace",
(980, 390),
)
origin_x, origin_y, cell = 18, 92, 15
@@ -130,8 +170,8 @@ def render_builder_assets(
def _optimized_frame(stage: int) -> Image.Image:
image, draw = _base_frame(
"Optimized serial mechanisms",
- f"didactic stage {stage + 1}/6 | storage/work changes only; search semantics stay shared",
- (960, 430),
+ f"didactic stage {stage + 1}/7 | storage/work changes only; search semantics stay shared",
+ (960, 500),
)
draw.text(
(18, 82),
@@ -140,7 +180,7 @@ def _optimized_frame(stage: int) -> Image.Image:
fill=EXPLAIN_TEXT_RGB,
)
draw.rounded_rectangle(
- (18, 106, 245, 392),
+ (18, 106, 245, 462),
radius=7,
fill=(239, 241, 245),
outline=(170, 177, 190),
@@ -151,11 +191,12 @@ def _optimized_frame(stage: int) -> Image.Image:
"initial trail entries",
"full DFS frame reserve",
"verified SAT result copy",
+ "linear MRV scan after the root",
)
y = 130
for line in baseline:
draw.text((34, y), line, font=explain_font(10), fill=EXPLAIN_MUTED_RGB)
- y += 46
+ y += 48
draw.text((276, 82), "Retained optimized path", font=explain_font(14), fill=EXPLAIN_TEXT_RGB)
for index, (name, description) in enumerate(_OPTIMIZATIONS):
@@ -182,7 +223,7 @@ def _optimized_frame(stage: int) -> Image.Image:
fill=EXPLAIN_TEXT_RGB if active else EXPLAIN_MUTED_RGB,
)
draw.text(
- (276, 400),
+ (276, 468),
"Measured reports establish benefit separately; this animation claims no speedup.",
font=explain_font(9),
fill=EXPLAIN_MUTED_RGB,
@@ -195,12 +236,12 @@ def render_optimized_assets(
*,
duration_ms: int = 750,
) -> AnimationOutputs:
- frames = tuple(_optimized_frame(stage) for stage in range(6))
+ frames = tuple(_optimized_frame(stage) for stage in range(7))
return write_animation_assets(
frames,
- tuple(f"frame-{stage:02d}.png" for stage in range(6)),
+ tuple(f"frame-{stage:02d}.png" for stage in range(7)),
output_directory,
- fallback_index=5,
+ fallback_index=6,
duration_ms=duration_ms,
)
@@ -232,7 +273,7 @@ def _draw_hex_tile(draw: ImageDraw.ImageDraw, origin: tuple[int, int], edges: tu
def _hex_frame(square: object, port: object, stage: int) -> Image.Image:
image, draw = _base_frame(
"Square-to-hex presentation port",
- f"canonical-example stage {stage + 1}/4 | pure Basire/Culik witness mapping",
+ f"verified-transformation stage {stage + 1}/4 | pure Basire/Culik witness mapping",
(920, 430),
)
source_edges = square.tile_edges[0]
diff --git a/renderer/wang_generalized.py b/renderer/wang_generalized.py
index 95ecea0..c3b72a2 100644
--- a/renderer/wang_generalized.py
+++ b/renderer/wang_generalized.py
@@ -12,6 +12,8 @@
from collections.abc import Sequence
from dataclasses import dataclass
+import hashlib
+import json
from typing import Final
@@ -175,6 +177,41 @@ def _validate_fixed_specification() -> None:
_validate_fixed_specification()
+def generalized_specification_sha256() -> str:
+ """Hash the fixed semantic mapping independently of its raster layout."""
+ document = {
+ "schema": "wang-generalized-tiles-v1",
+ "color_names": COLOR_NAMES,
+ "atomic_tile_edges": CANONICAL_ATOMIC_TILE_EDGES,
+ "generalized_tiles": [
+ {
+ "name": tile.name,
+ "parts": [
+ {
+ "tile_id": part.tile_id,
+ "dx": part.dx,
+ "dy": part.dy,
+ "label": part.label,
+ }
+ for part in tile.parts
+ ],
+ }
+ for tile in GENERALIZED_TILES
+ ],
+ }
+ encoded = (
+ json.dumps(
+ document,
+ ensure_ascii=False,
+ allow_nan=False,
+ sort_keys=True,
+ separators=(",", ":"),
+ )
+ + "\n"
+ ).encode("utf-8")
+ return hashlib.sha256(encoded).hexdigest()
+
+
def color_label(color_id: int) -> str:
"""Return the symbolic paper/glue name with the numeric ID secondary."""
if type(color_id) is not int or not 0 <= color_id < len(COLOR_NAMES):
diff --git a/renderer/wang_narrative.py b/renderer/wang_narrative.py
new file mode 100644
index 0000000..ae5d3a2
--- /dev/null
+++ b/renderer/wang_narrative.py
@@ -0,0 +1,645 @@
+"""Fixed narrative compositions built from already validated pipeline outputs."""
+
+from __future__ import annotations
+
+import argparse
+from dataclasses import dataclass
+import hashlib
+import json
+from pathlib import Path
+
+import numpy as np
+from PIL import Image, ImageDraw
+
+from wang_animation import AnimationOutputs, write_animation_assets
+from wang_explain import (
+ EXPLAIN_ACTIVE_RGB,
+ EXPLAIN_MUTED_RGB,
+ EXPLAIN_PANEL_RGB,
+ EXPLAIN_TEXT_RGB,
+ draw_explain_heading,
+ explain_font,
+)
+from wang_generalized_render import (
+ compose_atomic_semantic_legend,
+ compose_generalized_overlay,
+ compose_generalized_sheet,
+)
+from wang_generalized import generalized_specification_sha256
+from wang_hex_port import WangSquareRenderError, check_square_to_hex, reduce_square_to_hex
+from wang_snapshot import load_explainability_bundle
+from wang_square import (
+ _compose_wang_hex_explain,
+ _compose_wang_square_explain,
+ _save_png_atomic,
+ load_wang_presentation,
+)
+
+
+_PIPELINE_LABELS = (
+ "CM1-in-3 formula",
+ "Boolean Z3",
+ "Yang-Zhang reduction",
+ "Reference solver",
+ "Optimized solver",
+ "Wang Z3",
+ "Independent verification",
+ "Square / generalized / hex",
+)
+_CHECKS = (
+ (
+ "boolean_z3_assignment",
+ "Boolean assignment",
+ "oracles.witness_check.is_valid_assignment",
+ ),
+ ("reference_tiling", "Reference tiling", "oracles.tiling_check.is_valid_tiling"),
+ (
+ "reference_assignment",
+ "Reference assignment",
+ "oracles.witness_check.is_valid_assignment",
+ ),
+ ("optimized_tiling", "Optimized tiling", "oracles.tiling_check.is_valid_tiling"),
+ (
+ "optimized_assignment",
+ "Optimized assignment",
+ "oracles.witness_check.is_valid_assignment",
+ ),
+ ("wang_z3_tiling", "Wang Z3 tiling", "oracles.tiling_check.is_valid_tiling"),
+)
+
+
+@dataclass(frozen=True, slots=True)
+class WitnessOutputs:
+ square: Path
+ generalized: Path
+ hex: Path
+ animation: AnimationOutputs
+
+
+@dataclass(frozen=True, slots=True)
+class GeneralizedOutputs:
+ sheet: Path
+ legend: Path
+
+
+@dataclass(frozen=True, slots=True)
+class OverviewOutputs:
+ animation: AnimationOutputs
+ home_preview: Path | None
+ worked_example: Path | None
+
+
+def _save_image(image: Image.Image, path: Path) -> None:
+ if image.mode != "RGB":
+ raise WangSquareRenderError("narrative output must be RGB")
+ _save_png_atomic(np.asarray(image, dtype=np.uint8), path)
+
+
+def _load_image(path: Path) -> Image.Image:
+ try:
+ with Image.open(path) as source:
+ source.load()
+ return source.convert("RGB")
+ except (OSError, ValueError) as error:
+ raise WangSquareRenderError(
+ f"cannot load narrative source image {path!s}: {error}"
+ ) from error
+
+
+def _fit(image: Image.Image, size: tuple[int, int]) -> Image.Image:
+ fitted = image.copy()
+ fitted.thumbnail(size, resample=Image.Resampling.NEAREST)
+ return fitted
+
+
+def _load_verification(path: str | Path) -> tuple[str, tuple[dict[str, object], ...]]:
+ source = Path(path)
+ try:
+ document = json.loads(source.read_text(encoding="utf-8"))
+ except (OSError, UnicodeError, json.JSONDecodeError) as error:
+ raise WangSquareRenderError(
+ f"cannot load verification receipt snapshot {source!s}: {error}"
+ ) from error
+ if type(document) is not dict or set(document) != {
+ "schema",
+ "expected_status",
+ "verification",
+ "agreement",
+ "source_sha256",
+ }:
+ raise WangSquareRenderError("verification receipt snapshot must be closed")
+ if document["schema"] != "wang-verification-receipts-v1":
+ raise WangSquareRenderError("verification receipt schema is unsupported")
+ status = document["expected_status"]
+ if type(status) is not str or status not in {"sat", "unsat"}:
+ raise WangSquareRenderError("verification receipt status is unsupported")
+ verification = document["verification"]
+ agreement = document["agreement"]
+ if type(verification) is not dict or set(verification) != {
+ name for name, _, _ in _CHECKS
+ }:
+ raise WangSquareRenderError("verification receipt record must be closed")
+ agreement_fields = {
+ "expected_status",
+ "boolean_z3_status",
+ "reference_status",
+ "optimized_status",
+ "wang_z3_status",
+ "all_status_equal",
+ "sat_witnesses_valid",
+ "passed",
+ }
+ if type(agreement) is not dict or set(agreement) != agreement_fields:
+ raise WangSquareRenderError("verification agreement must be closed")
+ if (
+ agreement["expected_status"] != status
+ or any(
+ agreement[name] != status
+ for name in (
+ "boolean_z3_status",
+ "reference_status",
+ "optimized_status",
+ "wang_z3_status",
+ )
+ )
+ or agreement["all_status_equal"] is not True
+ or agreement["passed"] is not True
+ or agreement["sat_witnesses_valid"] is not (True if status == "sat" else None)
+ ):
+ raise WangSquareRenderError("verification agreement is inconsistent")
+ records: list[dict[str, object]] = []
+ for name, _, checker in _CHECKS:
+ record = verification[name]
+ if type(record) is not dict or set(record) != {
+ "checker",
+ "performed",
+ "passed",
+ "witness_sha256",
+ }:
+ raise WangSquareRenderError(f"verification record {name} must be closed")
+ if record["checker"] != checker:
+ raise WangSquareRenderError(f"verification record {name} checker drifted")
+ if status == "sat":
+ digest = record["witness_sha256"]
+ valid = (
+ record["performed"] is True
+ and record["passed"] is True
+ and type(digest) is str
+ and len(digest) == 64
+ and all(character in "0123456789abcdef" for character in digest)
+ )
+ else:
+ valid = (
+ record["performed"] is False
+ and record["passed"] is None
+ and record["witness_sha256"] is None
+ )
+ if not valid:
+ raise WangSquareRenderError(f"verification record {name} is inconsistent")
+ records.append(record)
+ encoded_source = (
+ json.dumps(
+ {"verification": verification, "agreement": agreement},
+ ensure_ascii=False,
+ allow_nan=False,
+ indent=2,
+ )
+ + "\n"
+ ).encode("utf-8")
+ source_sha256 = document["source_sha256"]
+ if (
+ type(source_sha256) is not str
+ or hashlib.sha256(encoded_source).hexdigest() != source_sha256
+ ):
+ raise WangSquareRenderError("verification receipt source hash drifted")
+ return status, tuple(records)
+
+
+def _verification_frame(
+ status: str,
+ records: tuple[dict[str, object], ...],
+ stage: int,
+) -> Image.Image:
+ image = Image.new("RGB", (960, 500), EXPLAIN_PANEL_RGB)
+ draw = ImageDraw.Draw(image)
+ draw_explain_heading(
+ draw,
+ (18, 16),
+ title="Independent verification sequence",
+ subtitle=(
+ f"observed record {stage + 1}/6 | expected {status.upper()} | "
+ "renders checker receipts; does not rerun a verifier"
+ ),
+ )
+ for index, ((_, label, expected_prefix), record) in enumerate(
+ zip(_CHECKS, records, strict=True)
+ ):
+ y = 92 + index * 60
+ visible = index <= stage
+ performed = record.get("performed") is True
+ passed = record.get("passed") is True
+ checker = str(record.get("checker", ""))
+ if performed and passed and checker.startswith(expected_prefix):
+ state = "performed / passed"
+ fill = (213, 237, 224)
+ elif status == "unsat" and not performed and record.get("passed") is None:
+ state = "not applicable: no SAT witness"
+ fill = (235, 238, 243)
+ else:
+ raise WangSquareRenderError(
+ f"verification record {_CHECKS[index][0]} is inconsistent"
+ )
+ draw.rounded_rectangle(
+ (18, y, 930, y + 46),
+ radius=6,
+ fill=fill if visible else (242, 244, 247),
+ outline=(53, 144, 93) if index == stage else (181, 188, 199),
+ width=2 if index == stage else 1,
+ )
+ draw.text(
+ (32, y + 7),
+ label,
+ font=explain_font(12),
+ fill=EXPLAIN_TEXT_RGB if visible else EXPLAIN_MUTED_RGB,
+ )
+ draw.text(
+ (278, y + 8),
+ state,
+ font=explain_font(11),
+ fill=EXPLAIN_TEXT_RGB if visible else EXPLAIN_MUTED_RGB,
+ )
+ draw.text(
+ (548, y + 9),
+ checker,
+ font=explain_font(9),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ draw.text(
+ (18, 472),
+ "SAT checks validate named witnesses independently; UNSAT has no fabricated certificate.",
+ font=explain_font(9),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ return image
+
+
+def render_verification_assets(
+ run_path: str | Path,
+ output_directory: str | Path,
+ *,
+ duration_ms: int = 750,
+) -> AnimationOutputs:
+ status, records = _load_verification(run_path)
+ frames = tuple(
+ _verification_frame(status, records, stage) for stage in range(len(_CHECKS))
+ )
+ return write_animation_assets(
+ frames,
+ tuple(f"frame-{stage:02d}.png" for stage in range(len(frames))),
+ output_directory,
+ fallback_index=len(frames) - 1,
+ duration_ms=duration_ms,
+ )
+
+
+def _presentation_frame(
+ square: Image.Image,
+ generalized: Image.Image,
+ hex_image: Image.Image,
+ stage: int,
+) -> Image.Image:
+ image = Image.new("RGB", (1080, 620), EXPLAIN_PANEL_RGB)
+ draw = ImageDraw.Draw(image)
+ labels = (
+ "verified square witness",
+ "exact generalized recognition",
+ "pure Basire/Culik port",
+ "checked hex presentation",
+ )
+ draw_explain_heading(
+ draw,
+ (18, 16),
+ title="Verified witness presentation",
+ subtitle=f"verified-transformation stage {stage + 1}/4 | {labels[stage]}",
+ )
+ sources = (square, generalized, generalized, hex_image)
+ fitted = _fit(sources[stage], (1020, 475))
+ image.paste(
+ fitted,
+ ((1080 - fitted.width) // 2, 88 + (475 - fitted.height) // 2),
+ )
+ if stage == 2:
+ draw.rounded_rectangle(
+ (246, 508, 834, 565),
+ radius=7,
+ fill=(239, 242, 246),
+ outline=(55, 126, 168),
+ width=2,
+ )
+ draw.text(
+ (278, 525),
+ "H(N,E,S,W) = (E,S,kappa,W,N,kappa); inverse and matching checked",
+ font=explain_font(11),
+ fill=EXPLAIN_TEXT_RGB,
+ )
+ draw.text(
+ (18, 594),
+ "The independent square witness check precedes presentation; raster output proves nothing by itself.",
+ font=explain_font(9),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ return image
+
+
+def render_witness_assets(
+ solution_path: str | Path,
+ output_directory: str | Path,
+ *,
+ duration_ms: int = 850,
+) -> WitnessOutputs:
+ destination = Path(output_directory)
+ destination.mkdir(parents=True, exist_ok=True)
+ presentation = load_wang_presentation(solution_path)
+ port = reduce_square_to_hex(presentation)
+ check_square_to_hex(presentation, port)
+ square = Image.fromarray(_compose_wang_square_explain(presentation), mode="RGB")
+ generalized = Image.fromarray(compose_generalized_overlay(presentation), mode="RGB")
+ hex_image = Image.fromarray(_compose_wang_hex_explain(presentation), mode="RGB")
+ square_path = destination / "square.png"
+ generalized_path = destination / "generalized.png"
+ hex_path = destination / "hex.png"
+ _save_image(square, square_path)
+ _save_image(generalized, generalized_path)
+ _save_image(hex_image, hex_path)
+ animation = write_animation_assets(
+ tuple(
+ _presentation_frame(square, generalized, hex_image, stage)
+ for stage in range(4)
+ ),
+ tuple(f"frame-{stage:02d}.png" for stage in range(4)),
+ destination,
+ fallback_index=3,
+ duration_ms=duration_ms,
+ )
+ return WitnessOutputs(square_path, generalized_path, hex_path, animation)
+
+
+def render_generalized_assets(
+ manifest_path: str | Path,
+ output_directory: str | Path,
+) -> GeneralizedOutputs:
+ bundle = load_explainability_bundle(manifest_path)
+ destination = Path(output_directory)
+ destination.mkdir(parents=True, exist_ok=True)
+ sheet = destination / "sheet.png"
+ legend = destination / "atomic-legend.png"
+ _save_png_atomic(compose_generalized_sheet(bundle.tileset.tile_edges), sheet)
+ _save_png_atomic(
+ compose_atomic_semantic_legend(bundle.tileset.tile_edges), legend
+ )
+ return GeneralizedOutputs(sheet, legend)
+
+
+def render_presentation_status(status: str, output_path: str | Path) -> Path:
+ if status != "unsat":
+ raise WangSquareRenderError("presentation status is only valid for UNSAT")
+ image = Image.new("RGB", (960, 500), EXPLAIN_PANEL_RGB)
+ draw = ImageDraw.Draw(image)
+ draw_explain_heading(
+ draw,
+ (18, 16),
+ title="Witness presentation",
+ subtitle="observed | UNSAT | square, generalized overlay, and hex are not applicable",
+ )
+ draw.rounded_rectangle(
+ (145, 142, 815, 350),
+ radius=10,
+ fill=(239, 242, 246),
+ outline=(181, 188, 199),
+ )
+ draw.text(
+ (257, 188),
+ "No SAT witness was returned",
+ font=explain_font(20),
+ fill=EXPLAIN_TEXT_RGB,
+ )
+ draw.text(
+ (213, 242),
+ "No square, generalized, or hex witness is fabricated.",
+ font=explain_font(13),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ draw.text(
+ (226, 285),
+ "The trace records search; it is not an UNSAT certificate.",
+ font=explain_font(12),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ destination = Path(output_path)
+ destination.parent.mkdir(parents=True, exist_ok=True)
+ _save_image(image, destination)
+ return destination
+
+
+def _pipeline_frame(sources: tuple[Image.Image, ...], stage: int) -> Image.Image:
+ image = Image.new("RGB", (1080, 620), EXPLAIN_PANEL_RGB)
+ draw = ImageDraw.Draw(image)
+ draw_explain_heading(
+ draw,
+ (18, 16),
+ title="One captured v2 pipeline run",
+ subtitle=(
+ f"observed milestone {stage + 1}/8 | {_PIPELINE_LABELS[stage]} | "
+ "component order, not a timing scale"
+ ),
+ )
+ node_width = 126
+ for index, label in enumerate(_PIPELINE_LABELS):
+ x = 18 + index * 130
+ active = index <= stage
+ draw.rounded_rectangle(
+ (x, 88, x + node_width - 8, 144),
+ radius=6,
+ fill=(213, 237, 224) if active else (240, 242, 246),
+ outline=(52, 145, 94) if index == stage else (181, 188, 199),
+ width=2 if index == stage else 1,
+ )
+ words = label.replace(" / ", "/").split()
+ draw.text(
+ (x + 7, 96),
+ "\n".join(words[:3]),
+ font=explain_font(8),
+ fill=EXPLAIN_TEXT_RGB if active else EXPLAIN_MUTED_RGB,
+ spacing=2,
+ )
+ if index < len(_PIPELINE_LABELS) - 1:
+ draw.line((x + 118, 116, x + 130, 116), fill=(129, 139, 153), width=2)
+ fitted = _fit(sources[stage], (1020, 400))
+ image.paste(
+ fitted,
+ ((1080 - fitted.width) // 2, 166 + (400 - fitted.height) // 2),
+ )
+ draw.text(
+ (18, 594),
+ "All facts come from one validated v2 run; independent checks remain separate from rendering.",
+ font=explain_font(9),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ return image
+
+
+def _home_preview(square: Image.Image) -> Image.Image:
+ image = Image.new("RGB", (760, 430), EXPLAIN_PANEL_RGB)
+ draw = ImageDraw.Draw(image)
+ draw_explain_heading(
+ draw,
+ (18, 16),
+ title="Verified SAT witness",
+ subtitle="observed | captured SAT source | square presentation",
+ )
+ fitted = _fit(square, (720, 320))
+ image.paste(fitted, ((760 - fitted.width) // 2, 82))
+ draw.text(
+ (18, 407),
+ "Preview only; the worked example retains the full source and trust boundary.",
+ font=explain_font(9),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ return image
+
+
+def _worked_example(sources: tuple[Image.Image, ...]) -> Image.Image:
+ image = Image.new("RGB", (1080, 940), EXPLAIN_PANEL_RGB)
+ draw = ImageDraw.Draw(image)
+ draw_explain_heading(
+ draw,
+ (18, 16),
+ title="Captured SAT semantic milestones",
+ subtitle="observed | fixed component order | static reduced-motion sequence",
+ )
+ card_width, card_height = 510, 195
+ for index, (label, source) in enumerate(zip(_PIPELINE_LABELS, sources, strict=True)):
+ column = index % 2
+ row = index // 2
+ x = 18 + column * 528
+ y = 82 + row * 210
+ draw.rounded_rectangle(
+ (x, y, x + card_width, y + card_height),
+ radius=7,
+ fill=EXPLAIN_ACTIVE_RGB,
+ outline=(181, 188, 199),
+ )
+ draw.text((x + 10, y + 8), f"t{index} {label}", font=explain_font(11), fill=EXPLAIN_TEXT_RGB)
+ fitted = _fit(source, (card_width - 20, card_height - 42))
+ image.paste(fitted, (x + (card_width - fitted.width) // 2, y + 35))
+ draw.text(
+ (18, 918),
+ "Milestones are semantic selections, not uniformly sampled time points.",
+ font=explain_font(9),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ return image
+
+
+def render_overview_assets(
+ source_paths: tuple[str | Path, ...],
+ home_source: str | Path,
+ output_directory: str | Path,
+ *,
+ duration_ms: int = 900,
+ include_sat_story: bool = True,
+) -> OverviewOutputs:
+ if len(source_paths) != len(_PIPELINE_LABELS):
+ raise WangSquareRenderError("pipeline overview requires eight named sources")
+ sources = tuple(_load_image(Path(path)) for path in source_paths)
+ home_image = _load_image(Path(home_source)) if include_sat_story else None
+ destination = Path(output_directory)
+ destination.mkdir(parents=True, exist_ok=True)
+ frames = tuple(_pipeline_frame(sources, stage) for stage in range(len(sources)))
+ animation = write_animation_assets(
+ frames,
+ tuple(f"frame-{stage:02d}.png" for stage in range(len(frames))),
+ destination,
+ fallback_index=len(frames) - 1,
+ duration_ms=duration_ms,
+ )
+ home_preview: Path | None = None
+ worked_example: Path | None = None
+ if home_image is not None:
+ home_preview = destination / "home-preview.png"
+ worked_example = destination / "worked-example.png"
+ _save_image(_home_preview(home_image), home_preview)
+ _save_image(_worked_example(sources), worked_example)
+ return OverviewOutputs(animation, home_preview, worked_example)
+
+
+def _parser() -> argparse.ArgumentParser:
+ parser = argparse.ArgumentParser(
+ description="compose fixed narrative assets from validated pipeline outputs"
+ )
+ subparsers = parser.add_subparsers(dest="mode", required=True)
+ verification = subparsers.add_parser("verification")
+ verification.add_argument("run", type=Path)
+ verification.add_argument("output_directory", type=Path)
+ witness = subparsers.add_parser("witness")
+ witness.add_argument("solution", type=Path)
+ witness.add_argument("output_directory", type=Path)
+ generalized = subparsers.add_parser("generalized")
+ generalized.add_argument("manifest", type=Path)
+ generalized.add_argument("output_directory", type=Path)
+ status = subparsers.add_parser("status")
+ status.add_argument("status", choices=("unsat",))
+ status.add_argument("output", type=Path)
+ overview = subparsers.add_parser("overview")
+ overview.add_argument("output_directory", type=Path)
+ overview.add_argument("sources", nargs=8, type=Path)
+ overview.add_argument("--home-source", required=True, type=Path)
+ overview.add_argument("--omit-sat-story", action="store_true")
+ return parser
+
+
+def main(arguments: list[str] | None = None) -> int:
+ parser = _parser()
+ args = parser.parse_args(arguments)
+ try:
+ if args.mode == "verification":
+ outputs = render_verification_assets(args.run, args.output_directory)
+ print(f"animation={outputs.animation}")
+ print(f"contact_sheet={outputs.contact_sheet}")
+ print(f"fallback={outputs.fallback}")
+ elif args.mode == "witness":
+ outputs = render_witness_assets(args.solution, args.output_directory)
+ print(f"square={outputs.square}")
+ print(f"generalized={outputs.generalized}")
+ print(f"hex={outputs.hex}")
+ print(f"animation={outputs.animation.animation}")
+ print(f"contact_sheet={outputs.animation.contact_sheet}")
+ print(f"fallback={outputs.animation.fallback}")
+ elif args.mode == "generalized":
+ outputs = render_generalized_assets(args.manifest, args.output_directory)
+ print(f"sheet={outputs.sheet}")
+ print(f"legend={outputs.legend}")
+ print(f"spec_sha256={generalized_specification_sha256()}")
+ elif args.mode == "status":
+ print(f"status={render_presentation_status(args.status, args.output)}")
+ else:
+ outputs = render_overview_assets(
+ tuple(args.sources),
+ args.home_source,
+ args.output_directory,
+ include_sat_story=not args.omit_sat_story,
+ )
+ print(f"animation={outputs.animation.animation}")
+ print(f"contact_sheet={outputs.animation.contact_sheet}")
+ print(f"fallback={outputs.animation.fallback}")
+ if outputs.home_preview is not None:
+ print(f"home_preview={outputs.home_preview}")
+ if outputs.worked_example is not None:
+ print(f"worked_example={outputs.worked_example}")
+ except (FileNotFoundError, WangSquareRenderError) as error:
+ parser.error(str(error))
+ return 0
+
+
+if __name__ == "__main__":
+ raise SystemExit(main())
diff --git a/renderer/wang_trace_render.py b/renderer/wang_trace_render.py
index 76d455d..b161cd5 100644
--- a/renderer/wang_trace_render.py
+++ b/renderer/wang_trace_render.py
@@ -33,27 +33,57 @@
_CHANGED_RGB: Final = (245, 178, 60)
-def _selected_indices(events: tuple[TraceEvent, ...], maximum: int) -> tuple[int, ...]:
+def select_semantic_milestones(
+ events: tuple[TraceEvent, ...], maximum: int
+) -> tuple[int, ...]:
+ """Select semantic transitions first, then fill the widest replay gaps.
+
+ This is intentionally different from uniform frame sampling. The selected
+ states still come from the single validated replay performed by the caller.
+ """
if type(maximum) is not int or not 2 <= maximum <= 32:
raise WangSquareRenderError("max_frames must be in [2, 32]")
count = len(events)
if count <= maximum:
return tuple(range(count))
+
priority = [0, count - 1]
- for kind in ("propagation", "decision", "conflict", "backtrack"):
- match = next(
- (index for index, event in enumerate(events) if event.kind == kind),
- None,
- )
- if match is not None:
- priority.append(match)
+ for index in range(1, count):
+ if events[index].phase != events[index - 1].phase:
+ priority.extend((index - 1, index))
+ for kind in (
+ "propagation",
+ "decision",
+ "conflict",
+ "backtrack",
+ "domain_reduction",
+ ):
+ matches = [
+ index for index, event in enumerate(events) if event.kind == kind
+ ]
+ if matches:
+ priority.extend((matches[0], matches[-1]))
+ priority.extend(
+ index
+ for index, event in enumerate(events)
+ if event.kind == "domain_reduction"
+ and event.reason in {"decision", "backtrack"}
+ )
+ deepest_decisions = [
+ (event.depth, index)
+ for index, event in enumerate(events)
+ if event.kind == "decision"
+ ]
+ if deepest_decisions:
+ priority.append(max(deepest_decisions)[1])
+
selected = list(dict.fromkeys(priority))[:maximum]
- for slot in range(maximum):
- index = slot * (count - 1) // (maximum - 1)
- if index not in selected:
- selected.append(index)
- if len(selected) == maximum:
- break
+ while len(selected) < maximum:
+ candidate = max(
+ (index for index in range(count) if index not in selected),
+ key=lambda index: (min(abs(index - item) for item in selected), -index),
+ )
+ selected.append(candidate)
return tuple(sorted(selected))
@@ -187,7 +217,7 @@ def render_trace_assets(
"""Replay once, compose each selected frame once, then encode assets."""
bundle = load_trace_bundle(manifest_path)
states = replay_trace(bundle.trace)
- selected = _selected_indices(bundle.trace.events, max_frames)
+ selected = select_semantic_milestones(bundle.trace.events, max_frames)
frames = tuple(
_compose_frame(bundle, bundle.trace.events[index], states[index])
for index in selected
diff --git a/renderer/wang_z3_summary.py b/renderer/wang_z3_summary.py
index 22fcdea..5989546 100644
--- a/renderer/wang_z3_summary.py
+++ b/renderer/wang_z3_summary.py
@@ -384,6 +384,123 @@ def _compose_wang_frame(summary: Z3EncodingSummary, stage: int) -> Image.Image:
return image
+def _compose_boolean_frame(summary: Z3EncodingSummary, stage: int) -> Image.Image:
+ width, height = 940, 430
+ image = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB)
+ draw = ImageDraw.Draw(image)
+ labels = (
+ "configuration",
+ "Boolean variables",
+ "source-order clauses",
+ "result, assignment, and encoding statistics",
+ )
+ draw_explain_heading(
+ draw,
+ (18, 16),
+ title="Boolean Z3 encoding order",
+ subtitle=(
+ f"encoding-order stage {stage + 1}/4 | {labels[stage]} | "
+ "not a Z3 internal execution trace"
+ ),
+ )
+ draw.text(
+ (18, 78),
+ f"Z3 {summary.version} | random_seed={summary.random_seed} | "
+ f"threads={summary.threads}",
+ font=explain_font(12),
+ fill=EXPLAIN_TEXT_RGB,
+ )
+ steps = (
+ "1. create one Boolean term per variable in ascending ID order",
+ "2. visit clauses in source order",
+ "3. visit each clause left-to-right and assert exactly one true",
+ "4. check once; copy assignment and project-owned statistics",
+ )
+ for index, label in enumerate(steps):
+ y = 112 + index * 48
+ active = index <= stage
+ draw.rounded_rectangle(
+ (18, y, 520, y + 34),
+ radius=5,
+ fill=(213, 235, 246) if active else (239, 241, 245),
+ outline=(54, 127, 169) if index == stage else (184, 190, 201),
+ width=2 if index == stage else 1,
+ )
+ draw.text(
+ (29, y + 9),
+ label,
+ font=explain_font(10),
+ fill=EXPLAIN_TEXT_RGB if active else EXPLAIN_MUTED_RGB,
+ )
+
+ draw.rounded_rectangle(
+ (548, 106, 922, 378),
+ radius=6,
+ fill=EXPLAIN_ACTIVE_RGB,
+ outline=(180, 187, 198),
+ )
+ if stage == 0:
+ lines = (
+ f"formula variables: {summary.variable_count}",
+ "fixed seed and one solver thread",
+ "project order is public; Z3 search order is not",
+ )
+ elif stage == 1:
+ lines = (
+ f"Boolean terms: {summary.variable_count}",
+ "term IDs follow the formula variable IDs",
+ "no native-solver state is imported",
+ )
+ elif stage == 2:
+ lines = (
+ f"assertions: {summary.assertion_count}",
+ "clause order follows the parsed source",
+ "literal positions remain left-to-right",
+ )
+ else:
+ assignment = summary.assignment or ()
+ assignment_text = ", ".join(
+ f"x{index + 1}={'1' if value else '0'}"
+ for index, value in enumerate(assignment)
+ )
+ lines = (
+ f"result: {summary.status.upper()}",
+ f"assignment: {assignment_text or 'not applicable'}",
+ f"encoding statistics: {len(summary.statistics)}",
+ "independent assignment checking is downstream",
+ )
+ y = 128
+ for line in lines:
+ draw.text((566, y), line, font=explain_font(11), fill=EXPLAIN_TEXT_RGB)
+ y += 31
+ draw.text(
+ (18, 408),
+ "Rendering explains declared construction order; it does not expose Z3 decisions.",
+ font=explain_font(9),
+ fill=EXPLAIN_MUTED_RGB,
+ )
+ return image
+
+
+def render_boolean_z3_assets(
+ summary_path: str | Path,
+ output_directory: str | Path,
+ *,
+ duration_ms: int = 800,
+) -> AnimationOutputs:
+ summary = load_z3_encoding_summary(summary_path)
+ if summary.engine != BOOLEAN_ENGINE:
+ raise WangSquareRenderError("encoding animation requires a Boolean Z3 summary")
+ frames = tuple(_compose_boolean_frame(summary, stage) for stage in range(4))
+ return write_animation_assets(
+ frames,
+ tuple(f"frame-{stage:02d}.png" for stage in range(4)),
+ output_directory,
+ fallback_index=2,
+ duration_ms=duration_ms,
+ )
+
+
def render_wang_z3_assets(
summary_path: str | Path,
output_directory: str | Path,
@@ -405,7 +522,7 @@ def render_wang_z3_assets(
def _parser() -> argparse.ArgumentParser:
parser = argparse.ArgumentParser(
- description="render the declared Wang Z3 encoding order without Z3"
+ description="render a declared Boolean or Wang Z3 encoding order without Z3"
)
parser.add_argument("summary", type=Path)
parser.add_argument("output_directory", type=Path)
@@ -417,10 +534,14 @@ def main(arguments: list[str] | None = None) -> int:
parser = _parser()
args = parser.parse_args(arguments)
try:
- outputs = render_wang_z3_assets(
- args.summary,
- args.output_directory,
- duration_ms=args.duration_ms,
+ summary = load_z3_encoding_summary(args.summary)
+ renderer = (
+ render_boolean_z3_assets
+ if summary.engine == BOOLEAN_ENGINE
+ else render_wang_z3_assets
+ )
+ outputs = renderer(
+ args.summary, args.output_directory, duration_ms=args.duration_ms
)
except (FileNotFoundError, WangSquareRenderError) as error:
parser.error(str(error))
diff --git a/schemas/wang-narrative-assets-v1.schema.json b/schemas/wang-narrative-assets-v1.schema.json
new file mode 100644
index 0000000..c761047
--- /dev/null
+++ b/schemas/wang-narrative-assets-v1.schema.json
@@ -0,0 +1,303 @@
+{
+ "$schema": "https://json-schema.org/draft/2020-12/schema",
+ "$id": "https://xtraid.github.io/tiling-foundry/schemas/wang-narrative-assets-v1.schema.json",
+ "title": "Tiling Foundry shared narrative assets v1",
+ "type": "object",
+ "additionalProperties": false,
+ "required": [
+ "schema",
+ "product",
+ "case",
+ "identities",
+ "animations",
+ "statics",
+ "pdf_milestones"
+ ],
+ "properties": {
+ "schema": {"const": "wang-narrative-assets-v1"},
+ "product": {"enum": ["run-specific", "canonical-pages"]},
+ "case": {
+ "type": "object",
+ "additionalProperties": false,
+ "required": ["id", "expected_status", "source_sha256"],
+ "properties": {
+ "id": {"type": "string", "minLength": 1},
+ "expected_status": {"enum": ["sat", "unsat"]},
+ "source_sha256": {"$ref": "#/$defs/sha256"}
+ }
+ },
+ "identities": {
+ "type": "object",
+ "additionalProperties": false,
+ "required": [
+ "source_formula",
+ "formula_snapshot",
+ "tileset",
+ "region",
+ "provenance",
+ "boolean_z3_summary",
+ "reference_trace_manifest",
+ "reference_trace",
+ "reference_solution",
+ "optimized_trace_manifest",
+ "optimized_trace",
+ "optimized_solution",
+ "wang_z3_summary"
+ ],
+ "properties": {
+ "source_formula": {"$ref": "#/$defs/sha256"},
+ "formula_snapshot": {"$ref": "#/$defs/sha256"},
+ "tileset": {"$ref": "#/$defs/sha256"},
+ "region": {"$ref": "#/$defs/sha256"},
+ "provenance": {"$ref": "#/$defs/sha256"},
+ "boolean_z3_summary": {"$ref": "#/$defs/sha256"},
+ "reference_trace_manifest": {"$ref": "#/$defs/sha256"},
+ "reference_trace": {"$ref": "#/$defs/sha256"},
+ "reference_solution": {"$ref": "#/$defs/nullable_sha256"},
+ "optimized_trace_manifest": {"$ref": "#/$defs/sha256"},
+ "optimized_trace": {"$ref": "#/$defs/sha256"},
+ "optimized_solution": {"$ref": "#/$defs/nullable_sha256"},
+ "wang_z3_summary": {"$ref": "#/$defs/sha256"}
+ }
+ },
+ "animations": {
+ "type": "object",
+ "additionalProperties": false,
+ "required": [
+ "pipeline_overview",
+ "boolean_z3",
+ "region_construction",
+ "reference_trace",
+ "optimized_trace",
+ "wang_z3",
+ "verification",
+ "witness_presentation",
+ "optimized_mechanisms"
+ ],
+ "properties": {
+ "pipeline_overview": {"$ref": "#/$defs/animation"},
+ "boolean_z3": {"$ref": "#/$defs/animation"},
+ "region_construction": {"$ref": "#/$defs/animation"},
+ "reference_trace": {"$ref": "#/$defs/animation"},
+ "optimized_trace": {"$ref": "#/$defs/animation"},
+ "wang_z3": {"$ref": "#/$defs/animation"},
+ "verification": {"$ref": "#/$defs/animation"},
+ "witness_presentation": {
+ "oneOf": [
+ {"$ref": "#/$defs/animation"},
+ {"type": "null"}
+ ]
+ },
+ "optimized_mechanisms": {"$ref": "#/$defs/animation"}
+ }
+ },
+ "statics": {
+ "type": "object",
+ "additionalProperties": false,
+ "required": [
+ "home_preview",
+ "worked_example",
+ "formula",
+ "generalized_sheet",
+ "atomic_legend",
+ "square_presentation",
+ "generalized_presentation",
+ "hex_presentation",
+ "presentation_status"
+ ],
+ "properties": {
+ "home_preview": {"$ref": "#/$defs/nullable_static"},
+ "worked_example": {"$ref": "#/$defs/nullable_static"},
+ "formula": {"$ref": "#/$defs/static"},
+ "generalized_sheet": {"$ref": "#/$defs/static"},
+ "atomic_legend": {"$ref": "#/$defs/static"},
+ "square_presentation": {"$ref": "#/$defs/nullable_static"},
+ "generalized_presentation": {"$ref": "#/$defs/nullable_static"},
+ "hex_presentation": {"$ref": "#/$defs/nullable_static"},
+ "presentation_status": {"$ref": "#/$defs/nullable_static"}
+ }
+ },
+ "pdf_milestones": {
+ "type": "object",
+ "additionalProperties": false,
+ "required": [
+ "selector",
+ "region_construction",
+ "reference_trace",
+ "optimized_trace",
+ "end_to_end"
+ ],
+ "properties": {
+ "selector": {"const": "semantic-milestones-v1"},
+ "region_construction": {"$ref": "#/$defs/png_paths"},
+ "reference_trace": {"$ref": "#/$defs/png_paths"},
+ "optimized_trace": {"$ref": "#/$defs/png_paths"},
+ "end_to_end": {"$ref": "#/$defs/png_paths"}
+ }
+ }
+ },
+ "$defs": {
+ "sha256": {"type": "string", "pattern": "^[0-9a-f]{64}$"},
+ "nullable_sha256": {
+ "oneOf": [
+ {"$ref": "#/$defs/sha256"},
+ {"type": "null"}
+ ]
+ },
+ "path": {
+ "type": "string",
+ "pattern": "^(?!/)(?!.*(?:^|/)\\.\\.?(?:/|$))[A-Za-z0-9._-]+(?:/[A-Za-z0-9._-]+)*$",
+ "minLength": 1
+ },
+ "artifact": {
+ "type": "object",
+ "additionalProperties": false,
+ "required": ["path", "sha256", "media_type"],
+ "properties": {
+ "path": {"$ref": "#/$defs/path"},
+ "sha256": {"$ref": "#/$defs/sha256"},
+ "media_type": {"enum": ["image/png", "image/gif"]}
+ }
+ },
+ "scope": {
+ "type": "object",
+ "additionalProperties": false,
+ "required": ["complete", "selected", "truncated"],
+ "properties": {
+ "complete": {"type": "boolean"},
+ "selected": {"type": "boolean"},
+ "truncated": {"const": false}
+ }
+ },
+ "metadata": {
+ "type": "object",
+ "required": [
+ "owner",
+ "semantic_label",
+ "caption",
+ "alt_text",
+ "source_contract",
+ "source_sha256",
+ "producer",
+ "validator",
+ "compositor"
+ ],
+ "properties": {
+ "owner": {
+ "type": "string",
+ "pattern": "^/(?:[A-Za-z0-9._-]+/)*$"
+ },
+ "semantic_label": {
+ "enum": [
+ "observed",
+ "canonical-construction",
+ "encoding-order",
+ "verified-transformation",
+ "didactic"
+ ]
+ },
+ "caption": {"type": "string", "minLength": 1},
+ "alt_text": {"type": "string", "minLength": 1},
+ "source_contract": {"type": "string", "minLength": 1},
+ "source_sha256": {"$ref": "#/$defs/sha256"},
+ "producer": {"type": "string", "minLength": 1},
+ "validator": {"type": "string", "minLength": 1},
+ "compositor": {"type": "string", "minLength": 1}
+ }
+ },
+ "animation": {
+ "allOf": [
+ {"$ref": "#/$defs/metadata"},
+ {
+ "type": "object",
+ "additionalProperties": false,
+ "required": [
+ "owner",
+ "semantic_label",
+ "caption",
+ "alt_text",
+ "source_contract",
+ "source_sha256",
+ "producer",
+ "validator",
+ "compositor",
+ "scope",
+ "animation",
+ "fallback",
+ "contact_sheet",
+ "frames"
+ ],
+ "properties": {
+ "owner": true,
+ "semantic_label": true,
+ "caption": true,
+ "alt_text": true,
+ "source_contract": true,
+ "source_sha256": true,
+ "producer": true,
+ "validator": true,
+ "compositor": true,
+ "scope": {"$ref": "#/$defs/scope"},
+ "animation": {"$ref": "#/$defs/artifact"},
+ "fallback": {"$ref": "#/$defs/artifact"},
+ "contact_sheet": {"$ref": "#/$defs/artifact"},
+ "frames": {
+ "type": "array",
+ "minItems": 1,
+ "items": {"$ref": "#/$defs/artifact"}
+ }
+ }
+ }
+ ]
+ },
+ "static": {
+ "allOf": [
+ {"$ref": "#/$defs/metadata"},
+ {
+ "type": "object",
+ "additionalProperties": false,
+ "required": [
+ "owner",
+ "semantic_label",
+ "caption",
+ "alt_text",
+ "source_contract",
+ "source_sha256",
+ "producer",
+ "validator",
+ "compositor",
+ "artifact"
+ ],
+ "properties": {
+ "owner": true,
+ "semantic_label": true,
+ "caption": true,
+ "alt_text": true,
+ "source_contract": true,
+ "source_sha256": true,
+ "producer": true,
+ "validator": true,
+ "compositor": true,
+ "artifact": {"$ref": "#/$defs/artifact"}
+ }
+ }
+ ]
+ },
+ "nullable_static": {
+ "oneOf": [
+ {"$ref": "#/$defs/static"},
+ {"type": "null"}
+ ]
+ },
+ "png_paths": {
+ "type": "array",
+ "minItems": 1,
+ "items": {
+ "allOf": [
+ {"$ref": "#/$defs/path"},
+ {"pattern": "\\.png$"}
+ ]
+ }
+ }
+ }
+}
diff --git a/tests/python/test_multi_engine_dossier.py b/tests/python/test_multi_engine_dossier.py
index 2a2c6b8..ce29f0e 100644
--- a/tests/python/test_multi_engine_dossier.py
+++ b/tests/python/test_multi_engine_dossier.py
@@ -4,6 +4,7 @@
import json
import os
from pathlib import Path
+import re
import shutil
import subprocess
import sys
@@ -12,7 +13,9 @@
from unittest.mock import patch
from dossier import multi_engine
+from dossier import narrative_assets as narrative_generator
from formats.pipeline_snapshot import PipelineSnapshotError
+from formats.narrative_assets import load_narrative_assets
from formats.run_case_v2 import (
CASE_SCHEMA,
load_run_case_v2,
@@ -33,27 +36,7 @@
ROOT = Path(__file__).resolve().parents[2]
SAT_CASE = ROOT / "examples/run-cases-v2/pipeline-sat.json"
-
-
-def _unsat_case() -> dict[str, object]:
- return {
- "schema": CASE_SCHEMA,
- "id": "pipeline-unsat-v2",
- "title": "Full-pipeline UNSAT capture test",
- "purpose": "Exercise the closed v2 UNSAT and not-applicable fields.",
- "source": "tests/instances/pipeline_unsat_search.cm13",
- "expected_status": "unsat",
- "reference_trace": {
- "event_capacity": 8192,
- "checkpoint_interval": 128,
- "checkpoint_capacity": 64,
- },
- "optimized_trace": {
- "event_capacity": 8192,
- "checkpoint_interval": 128,
- "checkpoint_capacity": 64,
- },
- }
+UNSAT_CASE = ROOT / "examples/run-cases-v2/pipeline-unsat-search.json"
class MultiEngineDossierTests(unittest.TestCase):
@@ -65,14 +48,9 @@ def setUpClass(cls) -> None:
multi_engine.generate_multi_engine_dossier(SAT_CASE, cls.sat_directory)
cls.sat_document = load_run_dossier_v2(cls.sat_directory / "run.json")
- cls.unsat_case_path = cls.root / "unsat-case.json"
- cls.unsat_case_path.write_text(
- json.dumps(_unsat_case(), ensure_ascii=False) + "\n",
- encoding="utf-8",
- )
cls.unsat_directory = cls.root / "unsat"
multi_engine.generate_multi_engine_dossier(
- cls.unsat_case_path,
+ UNSAT_CASE,
cls.unsat_directory,
)
cls.unsat_document = load_run_dossier_v2(
@@ -161,7 +139,27 @@ def test_sat_capture_binds_named_engines_and_shared_native_inputs(self) -> None:
document["reduction"]["region_sha256"],
document["artifacts"]["region_snapshot"]["sha256"],
)
- self.assertIsNone(document["presentation"]["square"]["artifact"])
+ self.assertEqual(
+ document["presentation"]["square"]["artifact"],
+ "square_presentation",
+ )
+ self.assertEqual(document["reference"]["trace"]["selection"], {
+ "performed": True,
+ "selected_event_count": 10,
+ })
+ self.assertEqual(document["optimized"]["trace"]["selection"], {
+ "performed": True,
+ "selected_event_count": 10,
+ })
+ narrative = load_narrative_assets(
+ self.sat_directory / "assets/narrative/manifest.json",
+ document,
+ )
+ self.assertEqual(narrative["product"], "run-specific")
+ self.assertEqual(
+ narrative["animations"]["optimized_mechanisms"]["semantic_label"],
+ "didactic",
+ )
self.assertFalse((self.sat_directory / "report.tex").exists())
self.assertFalse((self.sat_directory / "report.pdf").exists())
@@ -188,6 +186,36 @@ def test_unsat_capture_has_no_witness_or_fabricated_verification(self) -> None:
for presentation in document["presentation"].values():
self.assertFalse(presentation["applicable"])
self.assertIsNone(presentation["artifact"])
+ narrative = load_narrative_assets(
+ self.unsat_directory / "assets/narrative/manifest.json",
+ document,
+ )
+ self.assertIsNone(narrative["animations"]["witness_presentation"])
+ self.assertIsNotNone(narrative["statics"]["presentation_status"])
+ self.assertIsNone(narrative["statics"]["home_preview"])
+ for solver, animation_name in (
+ ("reference", "reference_trace"),
+ ("optimized", "optimized_trace"),
+ ):
+ trace_path = self.unsat_directory / document["artifacts"][
+ f"{solver}_trace"
+ ]["path"]
+ trace = json.loads(trace_path.read_text(encoding="utf-8"))
+ all_kinds = {event["kind"] for event in trace["events"]}
+ self.assertTrue({"decision", "conflict", "backtrack"} <= all_kinds)
+ selected_sequences = {
+ int(Path(frame["path"]).stem.removeprefix("frame-"))
+ for frame in narrative["animations"][animation_name]["frames"]
+ }
+ selected_kinds = {
+ event["kind"]
+ for event in trace["events"]
+ if event["sequence"] in selected_sequences
+ }
+ self.assertTrue(
+ {"conflict", "backtrack", "result"} <= selected_kinds,
+ (solver, selected_kinds),
+ )
def test_case_contract_forbids_initial_domain_overrides(self) -> None:
invalid = json.loads(SAT_CASE.read_text(encoding="utf-8"))
@@ -309,6 +337,187 @@ def test_bundle_loader_imports_no_capture_or_native_producer(self) -> None:
)
self.assertEqual(completed.returncode, 0, completed.stderr)
+ def test_same_compositor_bytes_serve_run_and_canonical_pages(self) -> None:
+ destination = self.root / "canonical-pages-assets"
+ manifest_path = narrative_generator.generate_narrative_assets(
+ self.sat_directory / "run.json",
+ destination,
+ product="canonical-pages",
+ )
+ manifest = load_narrative_assets(manifest_path, self.sat_document)
+ self.assertEqual(manifest["product"], "canonical-pages")
+
+ run_root = self.sat_directory / "assets/narrative"
+ run_files = {
+ path.relative_to(run_root): path.read_bytes()
+ for path in run_root.rglob("*")
+ if path.is_file() and path.name != "manifest.json"
+ }
+ pages_files = {
+ path.relative_to(destination): path.read_bytes()
+ for path in destination.rglob("*")
+ if path.is_file() and path.name != "manifest.json"
+ }
+ self.assertEqual(run_files, pages_files)
+
+ def test_narrative_manifest_rejects_metadata_and_asset_tampering(self) -> None:
+ copied = self.root / "narrative-tampered"
+ shutil.copytree(self.sat_directory, copied)
+ run = load_run_dossier_v2(copied / "run.json")
+ manifest_path = copied / "assets/narrative/manifest.json"
+ manifest = json.loads(manifest_path.read_text(encoding="utf-8"))
+ manifest["animations"]["reference_trace"]["semantic_label"] = "didactic"
+ manifest_path.write_text(json.dumps(manifest) + "\n", encoding="utf-8")
+ with self.assertRaisesRegex(PipelineSnapshotError, "semantic_label"):
+ load_narrative_assets(manifest_path, run)
+
+ copied = self.root / "narrative-source-tampered"
+ shutil.copytree(self.sat_directory, copied)
+ run = load_run_dossier_v2(copied / "run.json")
+ manifest_path = copied / "assets/narrative/manifest.json"
+ manifest = json.loads(manifest_path.read_text(encoding="utf-8"))
+ manifest["statics"]["square_presentation"]["source_sha256"] = "0" * 64
+ manifest_path.write_text(json.dumps(manifest) + "\n", encoding="utf-8")
+ with self.assertRaisesRegex(PipelineSnapshotError, "static source"):
+ load_narrative_assets(manifest_path, run)
+
+ copied = self.root / "narrative-scope-tampered"
+ shutil.copytree(self.sat_directory, copied)
+ run = load_run_dossier_v2(copied / "run.json")
+ manifest_path = copied / "assets/narrative/manifest.json"
+ manifest = json.loads(manifest_path.read_text(encoding="utf-8"))
+ manifest["animations"]["reference_trace"]["scope"]["selected"] = False
+ manifest_path.write_text(json.dumps(manifest) + "\n", encoding="utf-8")
+ with self.assertRaisesRegex(PipelineSnapshotError, "selected.*policy"):
+ load_narrative_assets(manifest_path, run)
+
+ copied = self.root / "narrative-bytes-tampered"
+ shutil.copytree(self.sat_directory, copied)
+ manifest_path = copied / "assets/narrative/manifest.json"
+ manifest = json.loads(manifest_path.read_text(encoding="utf-8"))
+ frame = copied / "assets/narrative" / manifest["animations"][
+ "boolean_z3"
+ ]["frames"][0]["path"]
+ frame.write_bytes(frame.read_bytes() + b"tampered")
+ with self.assertRaisesRegex(PipelineSnapshotError, "does not match file"):
+ load_run_dossier_v2(copied / "run.json")
+
+ copied = self.root / "narrative-symlinked"
+ shutil.copytree(self.sat_directory, copied)
+ manifest_path = copied / "assets/narrative/manifest.json"
+ manifest = json.loads(manifest_path.read_text(encoding="utf-8"))
+ frame = copied / "assets/narrative" / manifest["animations"][
+ "boolean_z3"
+ ]["frames"][0]["path"]
+ alias = frame.with_name("internal-alias.png")
+ alias.write_bytes(frame.read_bytes())
+ frame.unlink()
+ frame.symlink_to(alias.name)
+ with self.assertRaisesRegex(PipelineSnapshotError, "symlinks are forbidden"):
+ load_run_dossier_v2(copied / "run.json")
+
+ copied = self.root / "narrative-parent-symlinked"
+ shutil.copytree(self.sat_directory, copied)
+ narrative_directory = copied / "assets/narrative"
+ relocated = copied / "relocated-narrative"
+ narrative_directory.rename(relocated)
+ narrative_directory.symlink_to("../relocated-narrative", target_is_directory=True)
+ with self.assertRaisesRegex(PipelineSnapshotError, "may not contain symlinks"):
+ load_run_dossier_v2(copied / "run.json")
+
+ def test_narrative_manifest_rejects_toolchain_and_milestone_drift(self) -> None:
+ copied = self.root / "narrative-toolchain-tampered"
+ shutil.copytree(self.sat_directory, copied)
+ run = load_run_dossier_v2(copied / "run.json")
+ manifest_path = copied / "assets/narrative/manifest.json"
+ manifest = json.loads(manifest_path.read_text(encoding="utf-8"))
+ manifest["animations"]["witness_presentation"]["validator"] = "fake.validator"
+ manifest_path.write_text(json.dumps(manifest) + "\n", encoding="utf-8")
+ with self.assertRaisesRegex(PipelineSnapshotError, "validator"):
+ load_narrative_assets(manifest_path, run)
+
+ copied = self.root / "narrative-milestones-tampered"
+ shutil.copytree(self.sat_directory, copied)
+ run = load_run_dossier_v2(copied / "run.json")
+ manifest_path = copied / "assets/narrative/manifest.json"
+ manifest = json.loads(manifest_path.read_text(encoding="utf-8"))
+ manifest["pdf_milestones"]["reference_trace"].reverse()
+ manifest_path.write_text(json.dumps(manifest) + "\n", encoding="utf-8")
+ with self.assertRaisesRegex(PipelineSnapshotError, "shared frame order"):
+ load_narrative_assets(manifest_path, run)
+
+ def test_run_loader_rejects_an_unattached_narrative_manifest(self) -> None:
+ copied = self.root / "narrative-unattached"
+ shutil.copytree(self.sat_directory, copied)
+ run_path = copied / "run.json"
+ run = json.loads(run_path.read_text(encoding="utf-8"))
+ for solver in ("reference", "optimized"):
+ run[solver]["trace"]["selection"] = {
+ "performed": False,
+ "selected_event_count": None,
+ }
+ run_path.write_text(json.dumps(run) + "\n", encoding="utf-8")
+ with self.assertRaisesRegex(PipelineSnapshotError, "performed selection"):
+ load_run_dossier_v2(run_path)
+
+ def test_narrative_generation_preserves_existing_destination_and_cleans_failure(self) -> None:
+ destination = self.root / "existing-narrative"
+ destination.mkdir()
+ sentinel = destination / "sentinel"
+ sentinel.write_text("keep\n", encoding="utf-8")
+ with self.assertRaisesRegex(
+ narrative_generator.NarrativeAssetError,
+ "already exists",
+ ):
+ narrative_generator.generate_narrative_assets(
+ self.sat_directory / "run.json", destination
+ )
+ self.assertEqual(sentinel.read_text(encoding="utf-8"), "keep\n")
+
+ failed = self.root / "failed-narrative"
+ before = set(self.root.glob(".failed-narrative.*"))
+ with patch.object(
+ narrative_generator,
+ "_run_renderer",
+ side_effect=narrative_generator.NarrativeAssetError("forced render failure"),
+ ):
+ with self.assertRaisesRegex(
+ narrative_generator.NarrativeAssetError,
+ "forced render failure",
+ ):
+ narrative_generator.generate_narrative_assets(
+ self.sat_directory / "run.json", failed
+ )
+ self.assertFalse(failed.exists())
+ self.assertEqual(set(self.root.glob(".failed-narrative.*")), before)
+
+ with patch.object(
+ narrative_generator.shutil,
+ "which",
+ return_value="/usr/bin/uv",
+ ), patch.object(
+ narrative_generator.subprocess,
+ "run",
+ return_value=subprocess.CompletedProcess([], 0, stdout="", stderr=""),
+ ):
+ with self.assertRaisesRegex(
+ narrative_generator.NarrativeAssetError,
+ "omitted required output keys: fallback",
+ ):
+ narrative_generator._run_renderer(
+ ["renderer.py"], required_outputs=("fallback",)
+ )
+
+ with self.assertRaisesRegex(
+ narrative_generator.NarrativeAssetError,
+ "canonical pipeline SAT",
+ ):
+ narrative_generator.generate_narrative_assets(
+ self.unsat_directory / "run.json",
+ self.root / "invalid-canonical-pages",
+ product="canonical-pages",
+ )
+
def test_failure_cleanup_and_existing_destination_are_safe(self) -> None:
destination = self.root / "existing"
destination.mkdir()
@@ -354,6 +563,27 @@ def disagree(*args: object, **kwargs: object) -> dict[str, object]:
self.assertFalse(mismatch.exists())
self.assertEqual(set(self.root.glob(".mismatch.*")), before)
+ narrative_failure = self.root / "narrative-failure"
+ before = set(self.root.glob(".narrative-failure.*"))
+ with patch.object(
+ narrative_generator,
+ "generate_narrative_assets",
+ side_effect=narrative_generator.NarrativeAssetError(
+ "forced narrative failure"
+ ),
+ ):
+ with self.assertRaisesRegex(
+ multi_engine.MultiEngineDossierError,
+ "shared narrative asset pass failed",
+ ):
+ multi_engine.generate_multi_engine_dossier(
+ SAT_CASE, narrative_failure
+ )
+ self.assertFalse(narrative_failure.exists())
+ self.assertEqual(
+ set(self.root.glob(".narrative-failure.*")), before
+ )
+
def test_final_replace_failure_leaves_no_partial_destination(self) -> None:
destination = self.root / "replace-failed"
before = set(self.root.glob(".replace-failed.*"))
@@ -383,6 +613,7 @@ def test_v2_schemas_are_closed_draft_2020_12_documents(self) -> None:
for name, expected in (
("wang-run-case-v2.schema.json", CASE_SCHEMA),
("wang-run-dossier-v2.schema.json", RUN_SCHEMA),
+ ("wang-narrative-assets-v1.schema.json", "wang-narrative-assets-v1"),
):
with self.subTest(schema=name):
schema = json.loads((ROOT / "schemas" / name).read_text(encoding="utf-8"))
@@ -392,6 +623,29 @@ def test_v2_schemas_are_closed_draft_2020_12_documents(self) -> None:
)
self.assertEqual(schema["properties"]["schema"]["const"], expected)
self.assertFalse(schema["additionalProperties"])
+ if name == "wang-narrative-assets-v1.schema.json":
+ owner = re.compile(
+ schema["$defs"]["metadata"]["properties"]["owner"][
+ "pattern"
+ ]
+ )
+ self.assertIsNotNone(owner.fullmatch("/"))
+ self.assertIsNotNone(owner.fullmatch("/components/verification/"))
+ self.assertIsNone(owner.fullmatch("components/verification/"))
+ relative_path = re.compile(schema["$defs"]["path"]["pattern"])
+ self.assertIsNotNone(relative_path.fullmatch("frames/frame-00.png"))
+ for invalid in (
+ "/etc/passwd",
+ "../frame.png",
+ "frames/../frame.png",
+ "frames//frame.png",
+ ):
+ self.assertIsNone(relative_path.fullmatch(invalid))
+ png_path_rules = schema["$defs"]["png_paths"]["items"]["allOf"]
+ self.assertEqual(png_path_rules[0]["$ref"], "#/$defs/path")
+ png_suffix = re.compile(png_path_rules[1]["pattern"])
+ self.assertIsNotNone(png_suffix.search("frames/frame-00.png"))
+ self.assertIsNone(png_suffix.search("frames/frame-00.gif"))
if __name__ == "__main__":
diff --git a/tools/generate_narrative_assets.py b/tools/generate_narrative_assets.py
new file mode 100644
index 0000000..984871f
--- /dev/null
+++ b/tools/generate_narrative_assets.py
@@ -0,0 +1,17 @@
+#!/usr/bin/env python3
+"""CLI for the fixed shared narrative-asset pass."""
+
+from __future__ import annotations
+
+from pathlib import Path
+import sys
+
+
+ROOT = Path(__file__).resolve().parents[1]
+sys.path.insert(0, str(ROOT / "python"))
+
+from dossier.narrative_assets import main # noqa: E402
+
+
+if __name__ == "__main__":
+ raise SystemExit(main())
diff --git a/tools/generate_run_dossier.py b/tools/generate_run_dossier.py
index 1ea0226..9a9dddf 100644
--- a/tools/generate_run_dossier.py
+++ b/tools/generate_run_dossier.py
@@ -462,7 +462,7 @@ def generate_run_dossier(
if schema == "wang-run-case-v2":
if tex_engine != "pdflatex" or max_frames != 12 or duration_ms != 500:
raise DossierGenerationError(
- "renderer and TeX options are v1-only until the v2 asset/PDF passes"
+ "v2 uses fixed asset parameters; configurable renderer and TeX options remain v1-only"
)
from dossier.multi_engine import (
MultiEngineDossierError,