Add multi-engine run dossier capture

README.md

@@ -78,6 +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 |
 | 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 |
 

docs/plans/2026-08-31-narrative-migration-checklist.md

@@ -141,15 +141,15 @@ checks prove the old files are unreferenced before deletion.
 | `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 |
 
-- [ ] Add separate closed v2 case and dossier contracts; do not extend or
+- [x] Add separate closed v2 case and dossier contracts; do not extend or
   loosen either v1 schema.
-- [ ] Name Boolean Z3, reduction, reference, optimized, Wang Z3, verification,
+- [x] Name Boolean Z3, reduction, reference, optimized, Wang Z3, verification,
   presentation, timings, and artifacts explicitly; do not use a generic stage
   array or plugin registry.
-- [ ] Require one formula/region/tileset/provenance identity across all named
+- [x] Require one formula/region/tileset/provenance identity across all named
   native and Z3 components.
-- [ ] Forbid initial-domain overrides in full-pipeline v2 cases.
-- [ ] Capture each engine once and reuse its result; do not solve during
+- [x] Forbid initial-domain overrides in full-pipeline v2 cases.
+- [x] Capture each engine once and reuse its result; do not solve during
   validation, rendering, Pages build, or PDF formatting.
 
 ## 7. Dossier v1 preservation checklist
@@ -173,7 +173,7 @@ checks prove the old files are unreferenced before deletion.
 
 1. [x] Freeze and test the exact generalized 14-to-23 mapping without changing
    the atomic tileset or standard square/hex output.
-2. [ ] Capture the explicit v2 multi-engine fields once per engine and bind all
+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
    compositor, including static semantic milestones.

docs/run_dossiers.md

@@ -2,20 +2,25 @@
 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.
+description: Opt-in v1 diagnostic reports and v2 multi-engine captures built from hash-bound traces, summaries, witnesses, and raw run metadata.
 section: Architecture and correctness
 document_kind: Reproduction and report contract
 status: Current implementation
-updated: 2026-08-28
+updated: 2026-09-01
 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.
+The sole public generator dispatches closed v1 and v2 case documents to
+separate implementations. Both are explicitly opt-in and leave parsing,
+reduction, ordinary solving, snapshot export, and the default Wang renderer
+unchanged.
+
+The v1 path turns one configured native run into a self-contained directory
+with `run.json`, `report.tex`, `report.pdf`, and `assets/`. Its four diagnostic
+cases, schemas, formatter, template, initial-domain behavior, and output shape
+remain unchanged.
 
 `run.json` is the authoritative report input. It records the source and Git
 identity, environment, solver options and result, complete trace counters,
@@ -94,3 +99,42 @@ 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.
+
+## Full-pipeline v2 capture
+
+`wang-run-case-v2` deliberately has no initial-domain override field. Its
+canonical case follows `tests/instances/pipeline_sat.cm13` through the four
+named engines and one shared native reduction:
+
+```sh
+make shared
+uv run --frozen python tools/generate_run_dossier.py \
+  examples/run-cases-v2/pipeline-sat.json \
+  build/run-dossiers/pipeline-sat-v2
+```
+
+The v2 implementation parses and reduces once, then runs the traced reference
+and optimized solvers exactly once while the same native formula and reduction
+are alive. It invokes the existing Boolean Z3 and Wang Z3 summary producers
+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
+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
+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.
+
+All v2 durations use one monotonic nanosecond clock and are labelled
+`run-specific-observation-not-a-benchmark`. They are raw facts about that
+capture, never a performance comparison. SAT-only checker timings are null for
+UNSAT rather than fabricated as zero.

examples/run-cases-v2/pipeline-sat.json

@@ -0,0 +1,18 @@
+{
+  "schema": "wang-run-case-v2",
+  "id": "pipeline-sat-v2",
+  "title": "Canonical SAT full-pipeline multi-engine capture",
+  "purpose": "Capture the named Boolean Z3, native reduction, reference, optimized, Wang Z3, and independent verification results for the canonical pipeline_sat.cm13 instance without domain overrides.",
+  "source": "tests/instances/pipeline_sat.cm13",
+  "expected_status": "sat",
+  "reference_trace": {
+    "event_capacity": 8192,
+    "checkpoint_interval": 128,
+    "checkpoint_capacity": 64
+  },
+  "optimized_trace": {
+    "event_capacity": 8192,
+    "checkpoint_interval": 128,
+    "checkpoint_capacity": 64
+  }
+}

python/dossier/__init__.py

@@ -0,0 +1 @@
+"""Opt-in dossier capture leaves; core and oracle modules never import this package."""