Add opt-in observed-run dossiers

.github/workflows/ci.yml

@@ -74,6 +74,14 @@ jobs:
         working-directory: renderer
         run: uv run --locked pytest -q
 
+      - name: Install isolated report compiler
+        run: |
+          sudo apt-get update
+          sudo apt-get install --yes --no-install-recommends texlive-latex-base
+
+      - name: Compile opt-in run dossier without shell escape
+        run: make run-dossier-smoke
+
   strict-compilers:
     runs-on: ubuntu-latest
 

Makefile

@@ -89,7 +89,7 @@ OPENMP_LIBRARY := $(LIB_DIR)/libwang_openmp.a
 	strict-check sanitizer-check analyzer-check valgrind-check \
 	cachegrind-check benchmark benchmark-smoke benchmark-compare \
 	benchmark-compare-smoke coverage coverage-c coverage-python \
-	parser-fuzz parser-fuzz-smoke parser-fuzz-corpus clean
+	parser-fuzz parser-fuzz-smoke parser-fuzz-corpus run-dossier-smoke clean
 
 all: serial shared
 
@@ -167,6 +167,16 @@ pages-check:
 generated-pages-check:
 	$(PYTHON) tools/check_generated_pages.py $(PAGES_BUILD_DIR)
 
+run-dossier-smoke: shared
+	$(RM) -r $(BUILD_DIR)/run-dossier-smoke
+	$(UV) run --frozen python tools/generate_run_dossier.py \
+		examples/run-cases/unsat-root-conflict.json \
+		$(BUILD_DIR)/run-dossier-smoke \
+		--tex-engine pdflatex --max-frames 8
+	test -s $(BUILD_DIR)/run-dossier-smoke/report.tex
+	test -s $(BUILD_DIR)/run-dossier-smoke/report.pdf
+	test -s $(BUILD_DIR)/run-dossier-smoke/run.json
+
 c-check: serial $(C_TEST_BINS)
 	@set -e; \
 	if [ -z "$(strip $(C_TEST_BINS))" ]; then \

README.md

@@ -76,6 +76,7 @@ solving remains future work.
 | Reduction construction provenance | Implemented as a separate opt-in native-owned result with exact signal orders, swap-bound gadget spans, manifest v2, and a square overlay view; the compact standard ABI does not allocate it |
 | Native solver event trace | Implemented as separate opt-in reference/optimized entry points with bounded observed events, full initial state, checkpoints, manifest v3, independent offline replay, and deterministic PNG/GIF views |
 | Reproducible Z3 summaries | Implemented for fixed seed/thread settings and explicit Boolean/Wang encoding order, result/model, and stable project-owned counts; no internal Z3 trace claim |
+| 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 |
 | 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 |
 
@@ -157,10 +158,8 @@ diagram.
 Planned work remains separated into independently reviewed changes. The new
 priority is explainability across the deterministic pipeline:
 
-1. publish a compact formula-to-final-image gallery and optional technical
-   report from versioned examples;
-2. resume serial MRV and hard-UNSAT evidence;
-3. define `TaskPlan` only after the serial evidence, then implement and measure
+1. resume serial MRV and hard-UNSAT evidence;
+2. define `TaskPlan` only after the serial evidence, then implement and measure
    real OpenMP execution.
 
 The implementation follows a deliberately small design rule: each datum has one
@@ -184,7 +183,7 @@ make check
 
 The imported renderer remains a separate locked Python project. Its Pillow and
 NumPy dependencies are not installed by the root project or exercised by
-`make check`. Run its 253-test combined suite independently:
+`make check`. Run its 262-test combined suite independently:
 
 ```sh
 cd renderer
@@ -227,6 +226,9 @@ invariants, and the square-only construction overlay.
 The [solver event trace contract](docs/wang_solver_trace.md) defines bounded
 native capture, manifest v3, semantic replay, checkpoints, truncation, and the
 presentation-only animation boundary.
+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.
 
 To export one observed reference run and render selected replay states:
 
@@ -247,6 +249,22 @@ uv run python tools/export_z3_encoding_summaries.py \
   tests/instances/pipeline_sat.cm13 build/z3-summaries
 ```
 
+To generate one self-contained report outside the ordinary run path, provide
+pdfLaTeX and select a versioned case explicitly:
+
+```sh
+make shared
+uv run --frozen python tools/generate_run_dossier.py \
+  examples/run-cases/sat-end-to-end.json \
+  build/run-dossiers/sat-end-to-end \
+  --tex-engine pdflatex
+```
+
+The compiler is invoked without shell escape. `run.json` preserves raw stage
+durations and hashes; the PDF reuses the validated trace frames and existing
+square/hex renderers. TeX remains an opt-in CI/tooling dependency, not a root
+Python dependency.
+
 Useful individual targets:
 
 ```sh

docs/run_dossiers.md

@@ -0,0 +1,96 @@
+---
+layout: page
+title: Observed-run dossiers and example index
+permalink: /run-dossiers/
+description: Opt-in LaTeX/PDF reports built from hash-bound solver traces, raw run metadata, and the existing square and hex render chain.
+section: Architecture and correctness
+document_kind: Reproduction and report contract
+status: Current implementation
+updated: 2026-08-28
+nav_order: 35
+---
+
+# Observed-run dossiers and example index
+
+The report generator turns one configured native run into a self-contained
+directory with `run.json`, `report.tex`, `report.pdf`, and `assets/`. It is
+explicitly opt-in and does not change parsing, reduction, ordinary solving,
+snapshot export, or the default Wang renderer.
+
+`run.json` is the authoritative report input. It records the source and Git
+identity, environment, solver options and result, complete trace counters,
+initial-domain overrides, raw stage durations, replay scope, and SHA-256 for
+every referenced JSON or raster asset. The LaTeX document and PDF are derived
+from that one document. They do not recalculate events, witness state, timing,
+or provenance.
+
+## Example index
+
+Four strict case documents are versioned. Their classification is checked
+against the observed trace rather than trusted as prose.
+
+| Case | Configured result | Required observed shape | Case source |
+| --- | --- | --- | --- |
+| SAT end to end | SAT | complete trace, independently checked witness, square and checked hex views | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/sat-end-to-end.json) |
+| Immediate root conflict | UNSAT | three events: root, initial conflict, result; no propagation or search | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-root-conflict.json) |
+| Initial propagation contradiction | UNSAT | domain reductions and propagation reach an initial conflict before any decision | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-propagation.json) |
+| Non-superficial search | UNSAT | complete depth-two run with four decisions, three conflicts, and four backtracks | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-search.json) |
+
+The first three cases use the same small formula so the observed boundary is
+easy to compare. The two constrained UNSAT cases deliberately exercise the
+public initial-domain option: their UNSAT status describes that configured
+Wang solve, not the unconstrained source formula. The search case uses a
+separate cubic monotone input whose unconstrained optimized run reaches depth
+two before exhausting all branches.
+
+This page is only an index. The [solver trace contract]({{ '/wang-solver-trace/' | relative_url }})
+remains the canonical explanation of event semantics, truncation, replay, and
+the existing animation assets. The [static snapshot contract]({{ '/wang-explainability-snapshots/' | relative_url }})
+defines formula and region views, while the [square-to-hex reference]({{ '/wang-square-to-hex/' | relative_url }})
+defines the presentation-only port. No animation, explanation, or generated
+run narrative is copied here.
+
+## Reproduce one dossier
+
+Build the shared native library, provide pdfLaTeX, and run the sole generator:
+
+```sh
+make shared
+uv run --frozen python tools/generate_run_dossier.py \
+  examples/run-cases/sat-end-to-end.json \
+  build/run-dossiers/sat-end-to-end \
+  --tex-engine pdflatex
+```
+
+The destination must not exist. Every intermediate is written below a sibling
+staging directory, the trace bundle is validated before rendering, and the
+completed directory is installed with one rename. A failed render or TeX
+compile leaves no partial destination.
+
+The generator calls the isolated renderer through its locked environment. A
+single replay composes the selected frames used for individual PNGs, the
+contact sheet, and the optional GIF. The PDF embeds the already-produced
+contact sheet and static square/hex PNGs; it never embeds viewer-dependent GIF
+or video content. UNSAT reports contain region views rather than inventing a
+solution.
+
+pdfLaTeX is invoked directly, never through a shell, with
+`-no-shell-escape`, restricted input/output policy, a private TeX home, UTC,
+and `SOURCE_DATE_EPOCH` derived from the recorded run time. The CI smoke
+installs TeX only inside its disposable runner. TeX is not a runtime or root
+Python dependency.
+
+## Timing and evidence boundary
+
+The monotonic durations for parse, region build, solve, export, render, and SAT
+witness verification are raw evidence from one environment. They are excluded
+from snapshot identity and are not performance gates. The native solver has no
+Z3-style encoding stage, so `encoding` is explicitly recorded as not applicable
+rather than reported as a fabricated zero-duration operation. Verification is
+also explicitly not applicable to UNSAT runs because the trace is diagnostic,
+not an independently checked certificate.
+
+Every example requires a complete trace. Selected frames remain a presentation
+subset of that trace. For UNSAT, `unsat_certificate` is always false: conflicts
+and trail history diagnose what the run observed but do not constitute a
+standalone mathematical proof of unsatisfiability.

docs/wang_solver_trace.md

@@ -161,3 +161,8 @@ Z3 uses a different boundary. Its versioned summaries are explicitly labeled
 `encoding-order`, fix version, seed and thread count, and record the
 project-defined constraint order, returned result/model, and stable
 project-owned counts. They do not expose or infer Z3's internal search order.
+
+The [observed-run dossier index]({{ '/run-dossiers/' | relative_url }}) lists
+the versioned SAT and UNSAT cases that reuse this trace and rendering chain in
+an opt-in LaTeX/PDF report. It adds no second replay path and does not turn
+UNSAT diagnostics into a proof certificate.

examples/run-cases/sat-end-to-end.json

@@ -0,0 +1,16 @@
+{
+  "schema": "wang-run-case-v1",
+  "id": "sat-end-to-end",
+  "title": "SAT formula-to-witness observed run",
+  "classification": "sat-end-to-end",
+  "description": "A complete optimized native run from a parsed CM13 formula through reduction, verified square witness, checked hex presentation, and selected replay frames.",
+  "source": "tests/instances/pipeline_sat.cm13",
+  "solver": "optimized",
+  "expected_status": "sat",
+  "trace": {
+    "event_capacity": 8192,
+    "checkpoint_interval": 128,
+    "checkpoint_capacity": 64
+  },
+  "initial_domain_overrides": []
+}

examples/run-cases/unsat-propagation.json

@@ -0,0 +1,21 @@
+{
+  "schema": "wang-run-case-v1",
+  "id": "unsat-propagation",
+  "title": "UNSAT contradiction during initial propagation",
+  "classification": "unsat-propagation-contradiction",
+  "description": "An observed constrained solve whose locally valid singleton on active cell zero propagates to an empty domain before search begins.",
+  "source": "tests/instances/pipeline_sat.cm13",
+  "solver": "optimized",
+  "expected_status": "unsat",
+  "trace": {
+    "event_capacity": 8192,
+    "checkpoint_interval": 128,
+    "checkpoint_capacity": 64
+  },
+  "initial_domain_overrides": [
+    {
+      "cell": 0,
+      "domain": 8
+    }
+  ]
+}

examples/run-cases/unsat-root-conflict.json

@@ -0,0 +1,21 @@
+{
+  "schema": "wang-run-case-v1",
+  "id": "unsat-root-conflict",
+  "title": "UNSAT immediate root conflict",
+  "classification": "unsat-root-conflict",
+  "description": "An observed constrained solve whose caller-supplied empty domain on active cell zero is rejected immediately in the initial phase.",
+  "source": "tests/instances/pipeline_sat.cm13",
+  "solver": "optimized",
+  "expected_status": "unsat",
+  "trace": {
+    "event_capacity": 8192,
+    "checkpoint_interval": 128,
+    "checkpoint_capacity": 64
+  },
+  "initial_domain_overrides": [
+    {
+      "cell": 0,
+      "domain": 0
+    }
+  ]
+}

examples/run-cases/unsat-search.json

@@ -0,0 +1,16 @@
+{
+  "schema": "wang-run-case-v1",
+  "id": "unsat-search",
+  "title": "UNSAT depth-two search with backtracking",
+  "classification": "unsat-non-superficial-search",
+  "description": "A complete optimized native run that survives initial propagation, reaches search depth two, and exhausts alternatives through multiple conflicts and backtracks.",
+  "source": "tests/instances/pipeline_unsat_search.cm13",
+  "solver": "optimized",
+  "expected_status": "unsat",
+  "trace": {
+    "event_capacity": 8192,
+    "checkpoint_interval": 128,
+    "checkpoint_capacity": 64
+  },
+  "initial_domain_overrides": []
+}