From 62edc0e5c217daa0dcbd3a4a01011c3ab6ecd105 Mon Sep 17 00:00:00 2001 From: Manuel Magnabosco Date: Mon, 31 Aug 2026 22:22:43 +0200 Subject: [PATCH] Freeze narrative architecture contract --- ...6-08-31-narrative-architecture-contract.md | 348 ++++++++++++++++++ ...026-08-31-narrative-migration-checklist.md | 253 +++++++++++++ 2 files changed, 601 insertions(+) create mode 100644 docs/plans/2026-08-31-narrative-architecture-contract.md create mode 100644 docs/plans/2026-08-31-narrative-migration-checklist.md diff --git a/docs/plans/2026-08-31-narrative-architecture-contract.md b/docs/plans/2026-08-31-narrative-architecture-contract.md new file mode 100644 index 0000000..c783002 --- /dev/null +++ b/docs/plans/2026-08-31-narrative-architecture-contract.md @@ -0,0 +1,348 @@ +# Narrative architecture contract + +**Status:** frozen for the narrative and multi-model dossier phase + +**Audited baseline:** `17edabc5c956cb6f00cbb19266b7701a04e30ee2` +(`Add lazy optimized MRV indexing (#20)`) on 31 August 2026 + +**Scope:** editorial architecture, content ownership, asset semantics, and the +shared vocabulary between GitHub Pages and the future full-pipeline dossier. +This document does not change public pages, schemas, generators, algorithms, +or generated assets. + +This is the normative input to the remaining narrative work. The companion +[migration checklist](2026-08-31-narrative-migration-checklist.md) records the +disposition of every current public page and asset. + +## 1. Product boundary + +GitHub Pages and the PDF dossier have different jobs: + +- **Pages** explains the project, its stable components, their relationships, + and their trust boundaries. Its prose is authored and reviewed Markdown. +- **A v2 dossier** records one named formula moving through the implemented + components in one captured run. Its prose scaffolding is fixed, and its + facts and static figures come from that run's validated manifest. +- **The v1 dossier** remains a diagnostic report for one configured native + solve. It is not reinterpreted as a multi-model report. + +Both downstream products may consume the same validated contracts and raster +outputs. They must not share generated prose, navigation, a database, or a +generic stage engine. The dependency direction remains: + +```text +native core and independent oracles + -> immutable Python models and existing closed JSON contracts + -> one validator / replay / compositor chain + -> authored Pages or an opt-in static PDF +``` + +Deleting Pages, LaTeX, dossier formatters, and renderer presentation modules +must leave parsing, reduction, native solving, both Z3 oracles, independent +verification, and ordinary square-solution export functional. + +## 2. Content taxonomy + +Every public Markdown document has exactly one editorial class: + +| Class | Meaning | May make current general claims? | Typical destination | +| --- | --- | --- | --- | +| `story` | Human-first explanation of the pipeline or one clearly named example | Yes, when backed by current references and artifacts | Home, pipeline, worked example, and component pages | +| `reference` | Maintained contract, methodology, implementation reference, or bibliography | Yes, within its explicit scope | `/reference/` index and unchanged canonical route | +| `evidence` | Dated, source-bound, corpus-bound, or environment-bound observation | No universal claim; limitations stay adjacent to results | `/evidence/` index and unchanged canonical route | +| `history` | Superseded or context-only design retained for provenance | No current implementation claim | History group in `/reference/` and unchanged route | + +The taxonomy is editorial metadata, not a new semantic schema for solver data. +Plans, authoring templates, and empty post placeholders remain excluded from +the public catalog and do not receive one of these public classes. + +## 3. Canonical examples + +### 3.1 SAT end-to-end example + +`tests/instances/pipeline_sat.cm13` is the sole canonical SAT example for the +homepage, pipeline page, worked example, component examples, full-pipeline v2 +capture, and v2 PDF. Its frozen source SHA-256 is +`3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542`. + +The full-pipeline capture must not apply initial-domain overrides. Boolean Z3, +the native Yang–Zhang reduction, native reference, native optimized, Wang Z3, +the independent verifier, square export, generalized presentation, and the +checked square-to-hex port all refer to this one formula and its hash-bound +derived artifacts. An engine disagreement is an error, not an alternate story. + +### 3.2 UNSAT search example + +`tests/instances/pipeline_unsat_search.cm13`, configured by +`examples/run-cases/unsat-search.json`, is the separate example for conflict +and backtracking. The formula SHA-256 is +`ea2b8feb6eb8f4e722f1ec9021445c84858120c8567d42528631bdfb77400a94`; +the case-file SHA-256 is +`e81fe884ebbcdb8b25bbd32c0ca92577fd7a1fc9400a0b6296410ac7683bbcbb`. +It is an unconstrained optimized run with no initial-domain overrides and an +observed complete depth-two search. + +It must always be named as a different formula and run. Its trace, frames, +timings, status, and artifact hashes must never be presented as later stages of +the SAT example. Root-conflict and propagation-contradiction v1 cases remain +diagnostic examples in the v1 dossier index; they are not part of the canonical +full-pipeline story. + +## 4. Frozen sitemap + +The following routes are additive. Existing routes listed in the migration +checklist remain valid. + +| Route | Class | Canonical responsibility | +| --- | --- | --- | +| `/` | `story` | Project promise, clickable complete pipeline, selected verified result, and routes into story/reference/evidence | +| `/pipeline/` | `story` | Component order, data flow, independence, and trust boundaries | +| `/worked-example/` | `story` | `pipeline_sat.cm13` from source bytes to verified square and checked hex presentation | +| `/components/tileset/` | `story` | Fixed 23 atomic tiles, 14 generalized tiles, colors, matching, and identifiers | +| `/components/boolean-z3/` | `story` | Boolean CM1-in-3 oracle and project-owned encoding order | +| `/components/yang-zhang/` | `story` | Formula-to-region reduction, generalized decomposition, routing, and native provenance | +| `/components/reference-solver/` | `story` | Explanatory native baseline, observed trace, and result ownership | +| `/components/optimized-solver/` | `story` | Six measured serial mechanisms and an observed optimized trace | +| `/components/wang-z3/` | `story` | Independent finite-region oracle and project-owned encoding order | +| `/components/verification/` | `story` | Independent witness checks and the exact claims they do and do not establish | +| `/components/visualization/` | `story` | Square presentation, generalized overlay, and verified square-to-hex transformation | +| `/reference/` | `story` index | Maintained references plus a visibly separate history group | +| `/evidence/` | `story` index | Dated benchmark, profile, coverage, and fuzz evidence | +| `/run-dossiers/` | `reference` index | Links to v1 diagnostic reports and v2 full-pipeline reports without reproducing either report in Markdown | + +`/reference/`, `/evidence/`, and `/run-dossiers/` are authored index pages. +They may derive lists from front matter but may not derive narrative prose from +`run.json`. + +## 5. Permalink compatibility + +All 27 current technical-document permalinks are frozen. The narrative phase +will not rename, remove, or repurpose any of them. In particular: + +- `/run-dossiers/` keeps the v1 contract and gains clearly separated links to + v2 outputs; it does not silently change the meaning of a v1 report; +- dated evidence routes remain dated evidence routes even when a component + page summarizes the accepted mechanism; +- `/historical_architecture/` remains the only public context page that links + the original architecture PDF; +- new component pages become canonical owners of narrative animations, while + old technical pages retain their contract or evidence role and link to the + new owner instead of embedding another copy. + +Because no current route moves, the planned migration requires no redirects. +If a later phase proposes a move, it must add and test an explicit redirect or +compatibility page before removing the old content; a canonical-link change +alone is not a redirect. + +## 6. Component-page template + +Every `/components/.../` page uses this H2 sequence. A section may state that +an item is not applicable, but it may not be omitted. + +1. **What it is** — one-paragraph role and stable project name. +2. **Why it exists** — the problem solved and why another component does not + own that responsibility. +3. **Inputs and outputs** — named models/contracts, identities, and status + behavior, including SAT/UNSAT/UNKNOWN where applicable. +4. **Mechanism** — the algorithm or transformation at the level needed to + interpret output without duplicating the technical reference. +5. **Primary animation** — one owned asset, its semantic label, source, + fallback, caption, and limits. +6. **Position in the pipeline** — predecessor, successor, and whether the + edge is semantic input, independent cross-check, or presentation-only. +7. **Observed example** — the named `pipeline_sat.cm13` run. Solver pages may + additionally link the separately named `unsat-search` example. +8. **Trust boundary** — what this component establishes, what independently + checks it, and what it is forbidden to infer. +9. **Artifacts and references** — schemas, fixtures, source modules, current + technical references, and relevant dated evidence. + +Required front matter will identify `page_class: story`, +`component_id`, `pipeline_order`, and the owned primary asset. Exact checker +syntax is deferred to the Pages implementation, but those concepts and the +section sequence are frozen here. + +## 7. Asset semantics and records + +Every narrative raster or animation declares exactly one of these labels: + +| Label | Permitted claim | +| --- | --- | +| `observed` | Data emitted by a named component execution. The record states whether the trace is complete and whether displayed frames are selected. | +| `canonical-construction` | Deterministic construction from versioned canonical inputs or provenance; it is not a clocked execution trace. | +| `encoding-order` | Project-owned order of constraint construction and returned summary/model; never Z3's internal search order. | +| `verified-transformation` | Deterministic transformation whose input/output relationship is checked by the existing transformation checker; the raster is not the checker. | +| `didactic` | Authored or synthetic explanation that makes no claim to record an execution. | + +`canonical-example` is retired as an asset label. Existing builder material +maps to `canonical-construction`; the checked square-to-hex material maps to +`verified-transformation`. + +Each asset record, whether represented in page front matter or a future closed +manifest, must name: + +- one canonical owner route; +- semantic label and plain-language caption; +- source instance or canonical input; +- source contract and its SHA-256 identity when applicable; +- producer, validator/replay, and compositor; +- complete/selected/truncated scope when events are involved; +- GIF, static reduced-motion fallback, contact sheet, and alt text when + animation is involved; +- whether the artifact is canonical Pages output or run-specific dossier + output. + +Two products may produce byte-identical files from the same input and +parameters, but they must not share ownership of one public file. A technical +page may link to an owned animation; only its owner embeds and explains it. + +## 8. Page-to-asset-to-source ownership + +This matrix fixes responsibilities, not final filenames. Assets marked `new` +are produced in the later shared-asset phase from the existing validator, +replay, and compositor chain. + +| Canonical owner | Primary asset | Label | Authoritative source | Consumer rule | +| --- | --- | --- | --- | --- | +| `/` | selected verified SAT square output (`new`) | `observed` | v2 `pipeline_sat.cm13` run, `wang-solution-v1` artifact | Small result preview; links to worked example and visualization owner | +| `/pipeline/` | complete component-flow composition (`new`) | `observed` | one validated v2 SAT dossier manifest and its named stage artifacts | Owns pipeline-wide composition; component pages own component detail | +| `/worked-example/` | static end-to-end milestone sequence (`new`) | `observed` | same v2 SAT manifest; one semantic milestone selector | Static sequence only; links to owned component animations | +| `/components/tileset/` | 14 generalized / 23 atomic decomposition sequence, sheet, and legend (`new`) | `canonical-construction` | fixed canonical tile table and exact generalized mapping | Owns tile vocabulary; no solver claim | +| `/components/boolean-z3/` | Boolean constraint construction (`new`) | `encoding-order` | `tests/fixtures/pipeline_sat_z3/boolean-z3.json` or its v2 hash-equivalent capture | Project encoding and model only; no internal Z3 search claim | +| `/components/yang-zhang/` | builder routing plus generalized overlay (replacement) | `canonical-construction` | `pipeline_sat_reduction_explain/manifest.json`, native provenance, generalized mapping | Replaces ownership currently held by the builder reference | +| `/components/reference-solver/` | observed reference trace (current bundle may seed replacement) | `observed` | `pipeline_sat_solver_trace/manifest.json` or v2 reference capture | Complete trace, selected frames; reference page owns explanation | +| `/components/optimized-solver/` | observed optimized trace (`new`) | `observed` | v2 optimized capture for `pipeline_sat.cm13` | Primary asset; complete trace, selected frames | +| `/components/optimized-solver/` | six-mechanism overview (replacement) | `didactic` | measured mechanism list including the MRV index | Secondary asset; dated reports establish performance | +| `/components/wang-z3/` | Wang constraint construction (current bundle may seed replacement) | `encoding-order` | `tests/fixtures/pipeline_sat_z3/wang-z3.json` or v2 capture | Project encoding and returned model only | +| `/components/verification/` | named checker sequence (`new`) | `observed` | v2 verification records over the shared solution/region/tileset identities | Shows checks performed; does not invent an UNSAT certificate | +| `/components/visualization/` | square to generalized to checked hex sequence (`new`) | `verified-transformation` | verified v2 square witness, generalized mapping, and pure square-to-hex checker | Presentation follows verification and never establishes SAT | +| `/run-dossiers/` | none | n/a | v1 and v2 report indexes | Links only; no copied report narrative or animation | +| `/historical_architecture/` | original architecture PDF | n/a | `docs/Wang23_C_OpenMP_Architecture_Spec_Merged.pdf` | Sole public context and download owner | + +The unsat-search observed trace is run-specific evidence linked from the two +solver pages and dossier index. It is not a second canonical pipeline asset and +must retain its separate source identity. + +## 9. Existing bundle disposition + +| Existing Pages bundle | Current source | Frozen target owner | Target label | Required migration | +| --- | --- | --- | --- | --- | +| `assets/images/builder-routing/` | reduction-explanation v2 manifest for `pipeline_sat.cm13` | `/components/yang-zhang/` | `canonical-construction` | Keep one physical bundle or replace it once; old builder reference links to owner | +| `assets/images/optimized-mechanisms/` | hard-coded didactic list of five retained mechanisms | `/components/optimized-solver/` | `didactic` | Replace with six-mechanism version including MRV; all dated reports link to owner | +| `assets/images/solver-trace/` | reference solver-trace v3 manifest for `pipeline_sat.cm13` | `/components/reference-solver/` | `observed` | Keep or replace once from shared pipeline; serial guide and trace contract link to owner | +| `assets/images/square-to-hex/` | checked `wang_solution_v1_square_sat.json` fixture | `/components/visualization/` | `verified-transformation` | Replace with canonical pipeline SAT witness when shared assets are ready | +| `assets/images/z3-encoding/` | Wang `z3-encoding-summary-v1` fixture for `pipeline_sat.cm13` | `/components/wang-z3/` | `encoding-order` | Keep or replace once; old oracle report links to owner | + +No bundle is moved, regenerated, or deleted by this contract. + +## 10. V2 PDF outline + +The v2 PDF follows the pipeline exactly: + +1. title, executive summary, instance identity, terminal status, and agreement; +2. readable CM13 input; +3. Boolean Z3 result, assignment when SAT, project encoding summary, and raw + run timing; +4. Yang–Zhang region, generalized vocabulary, native provenance, and static + semantic milestones `t0...tn`; +5. reference solver summary, selected observed frames, and raw metrics; +6. optimized solver summary, selected observed frames, six mechanisms, and raw + metrics; +7. Wang Z3 encoding summary, result, raw timing, and agreement; +8. independent verification and, for SAT only, atomic square, generalized, and + checked hex witness views; +9. reproducibility appendix containing commit, environment, parameters, + identities, hashes, manifests, raw timings, and the reproduction boundary. + +UNSAT reports retain the same order and explicitly mark assignment, witness, +and witness-only transformations not applicable. They do not fabricate a +solution, verification success, generalized witness, hex witness, or UNSAT +certificate. + +The PDF embeds only static PNG milestones already produced by the shared asset +pass. It embeds no GIF/video and invokes no second compositor. + +## 11. Fields shared by Pages and PDF + +"Shared" means identical validated facts, names, and artifacts. It does not +mean shared prose or a global project-state object. + +The future v2 closed contracts must provide named fields for: + +- case ID, title, purpose, source path, source SHA-256, and SAT/UNSAT intent; +- repository commit and capture environment; +- formula, region, tileset, provenance, reference trace, optimized trace, + solution, and Z3-summary schema names and SHA-256 identities; +- Boolean Z3, reference, optimized, and Wang Z3 configurations and terminal + results; +- agreement among named engines, with mismatch represented as failure; +- independent verification performed/result fields and the verified solution + identity when SAT; +- named raw timing fields whose identity is explicitly run-specific; +- named artifacts with relative path, SHA-256, media type, role, semantic + label, source identity, and static/animated form; +- trace completeness, selection, capacity, and truncation facts; +- square, generalized, and hex presentation relationships. + +The components are fixed and named. They are not encoded as a generic list of +stages, plugins, nodes, or callbacks. Pages may quote stable identities or +values and embed canonical assets, but all explanatory prose and navigation +remain Markdown. The PDF formatter may consume the fields directly, but it +must not recompute a solve, verification, replay, event count, or timing. + +## 12. V1 dossier compatibility + +The following are frozen throughout the narrative phase: + +- `wang-run-case-v1` and `wang-run-dossier-v1` schema names, closed fields, + classifications, and validation meaning; +- the four existing v1 case files and their distinction between unconstrained + and initial-domain-override runs; +- `run.json` as the authoritative v1 report input; +- the v1 generator's single-native-engine scope, output directory shape, + atomic installation, static/GIF asset behavior, and isolated pdfLaTeX rules; +- the rule that v1 UNSAT traces are diagnostic and not standalone proofs. + +V2 uses separate case and dossier schema names, validators, formatter, and +template. It may share focused helpers through a thin CLI dispatch, but it may +not add optional v2 fields to v1 or scatter v2 conditions through the v1 +formatter. Full-pipeline v2 cases forbid initial-domain overrides. + +## 13. Decision log and non-goals + +1. The site gains an authored narrative layer; it is not generated from a run. +2. The PDF records one run; it is not a general documentation mirror. +3. Existing permalinks and the v1 dossier meaning are preserved. +4. Every public animation has one owner; other pages link to it. +5. `pipeline_sat.cm13` is the sole SAT story instance; `unsat-search` is + explicitly separate. +6. The five asset semantic labels in section 7 are exhaustive. +7. Component pages use the section order in section 6. +8. Existing validators, replay, compositor, exporter, and independent checker + remain the only semantic implementations. +9. Generalized tiles are a presentation of the exact fixed 23-tile table, not + a new tileset, solution schema, color model, or solver domain. +10. Raw run timings remain evidence for one environment and never become a + benchmark claim in Pages or PDF. + +Explicit non-goals are: an event bus, workflow/DAG engine, plugin or stage +registry, generated prose, client-side documentation application, a second +verifier, a second replay, a second compositor, a renderer dependency in the +core, new solver events for presentation, a Z3 internal-search trace claim, +GIFs in PDF, changing the standard square/hex CLI behavior, or implementing +any final narrative asset in this contract freeze. + +## 14. Exit conditions for the contract freeze + +This contract is complete only when: + +- every current public page has one classification and an unchanged permalink; +- every current public asset has a current source and one frozen destination; +- every future component and primary asset has one owner; +- Pages, v2 PDF, and v1 dossier responsibilities cannot be confused; +- SAT and UNSAT examples cannot be mistaken for one run; +- downstream work can test semantic labels, component sections, ownership, + fallbacks, links, and dossier identity without inventing editorial policy. + +The companion checklist supplies those inventories and is part of this frozen +contract. diff --git a/docs/plans/2026-08-31-narrative-migration-checklist.md b/docs/plans/2026-08-31-narrative-migration-checklist.md new file mode 100644 index 0000000..f007949 --- /dev/null +++ b/docs/plans/2026-08-31-narrative-migration-checklist.md @@ -0,0 +1,253 @@ +# Narrative migration checklist + +**Status:** frozen inventory and migration map + +**Baseline:** `17edabc5c956cb6f00cbb19266b7701a04e30ee2` on 31 August +2026 + +This checklist applies the +[narrative architecture contract](2026-08-31-narrative-architecture-contract.md) +to every current public page, public Pages asset, dossier/schema contract, and +known excluded documentation source. Unchecked implementation actions belong +to later work; this inventory itself makes no public-site or asset change. + +## 1. Baseline audit + +- [x] Confirm `origin/main` points to the merged MRV-index squash commit + `17edabc` and descends directly from `ca8690c`. +- [x] Confirm the merged tree is byte-identical to reviewed feature commit + `cb33f37`. +- [x] Confirm all ten pull-request checks completed successfully. +- [x] Confirm 27 public technical documents plus `docs/index.md`. +- [x] Confirm all 27 current technical permalinks are unique and retained. +- [x] Confirm five public animation bundles, two public SVG files, one public + historical PDF, site CSS, and site JavaScript. +- [x] Confirm 12 closed JSON schemas, four v1 run cases, and one v1 dossier + generator family. +- [x] Confirm canonical SAT source `tests/instances/pipeline_sat.cm13` and + separate search-UNSAT source `tests/instances/pipeline_unsat_search.cm13`. +- [x] Record their SHA-256 identities in the architecture contract, together + with the separate `unsat-search` case-file identity. + +## 2. Public page inventory + +The `Destination` column names the future index or story owner. `Keep route` +is mandatory for every existing permalink. + +| Source and current route | Class | Destination / relationship | Frozen migration action | +| --- | --- | --- | --- | +| `docs/index.md` `/` | `story` | Homepage story owner | Rewrite only after shared assets exist; preserve technical catalog access | +| `docs/development_principles.md` `/development_principles/` | `reference` | `/reference/`; linked from `/pipeline/` | Keep route and current architecture authority | +| `docs/reduction_notes.md` `/reduction_notes/` | `reference` | `/reference/`; linked from Yang–Zhang component | Keep route and mathematical/project convention boundary | +| `docs/references.md` `/references/` | `reference` | `/reference/`; linked from relevant components | Keep route and external-source policy | +| `docs/run_dossiers.md` `/run-dossiers/` | `reference` | Dossier index owner | Keep v1 meaning; add visibly separate v2 links only after v2 exists | +| `docs/serial_solver_implementation_guide.md` `/serial_solver_implementation_guide/` | `reference` | `/reference/`; linked from both native solver components | Keep route; replace embedded trace animation with link to its component owner | +| `docs/solver_comparison_benchmark.md` `/solver_comparison_benchmark/` | `reference` | `/reference/`; linked from pipeline/evidence | Keep route as protocol, not an observed result | +| `docs/solver_performance_scope.md` `/solver_performance_scope/` | `reference` | `/reference/`; linked from optimized component | Keep route as optimization methodology | +| `docs/wang_explainability_snapshots.md` `/wang-explainability-snapshots/` | `reference` | `/reference/`; linked from pipeline and visualization | Keep route and snapshot contract responsibility | +| `docs/wang_reduction_explanation.md` `/wang-reduction-explanation/` | `reference` | `/reference/`; linked from Yang–Zhang component | Keep route and native-provenance contract responsibility | +| `docs/wang_solution_v1.md` `/wang-solution-v1/` | `reference` | `/reference/`; linked from verification/visualization | Keep route and square-solution contract responsibility | +| `docs/wang_solver_trace.md` `/wang-solver-trace/` | `reference` | `/reference/`; linked from native solver components | Keep route; replace embedded reference animation with link to owner | +| `docs/wang_square_to_hex.md` `/wang-square-to-hex/` | `reference` | `/reference/`; linked from visualization | Keep route and proof/checker responsibility; link to owned transformation animation | +| `docs/wang_z3_edge_table_2026-08-24.md` `/wang_z3_edge_table_2026-08-24/` | `reference` | `/reference/`; linked from Wang Z3 component | Keep route as oracle-model reference; move animation ownership to component | +| `docs/yang_zhang_builder_design.md` `/yang_zhang_builder_design/` | `reference` | `/reference/`; linked from Yang–Zhang component | Keep route and builder contract; move animation ownership to component | +| `docs/designs/2026-08-21-witness-extension-design.md` `/witness_correspondence/` | `reference` | `/reference/`; linked from verification | Keep route and witness-correspondence design | +| `docs/coverage_baseline_2026-08-22.md` `/coverage_baseline_2026-08-22/` | `evidence` | `/evidence/` | Keep route, source identity, and no-threshold limitation | +| `docs/parser_fuzz_smoke_2026-08-22.md` `/parser_fuzz_smoke_2026-08-22/` | `evidence` | `/evidence/` | Keep route, corpus, budget, and platform limits | +| `docs/solver_byte_support_2026-08-20.md` `/solver_byte_support_2026-08-20/` | `evidence` | `/evidence/`; linked from optimized component | Keep route; remove duplicate animation embed and link to component owner | +| `docs/solver_comparison_smoke_2026-08-21.md` `/solver_comparison_smoke_2026-08-21/` | `evidence` | `/evidence/` | Keep route and single-environment interpretation limits | +| `docs/solver_dynamic_stack_2026-08-17.md` `/solver_dynamic_stack_2026-08-17/` | `evidence` | `/evidence/`; linked from optimized component | Keep route; remove duplicate animation embed and link to component owner | +| `docs/solver_initial_trail_2026-08-17.md` `/solver_initial_trail_2026-08-17/` | `evidence` | `/evidence/`; linked from optimized component | Keep route; remove duplicate animation embed and link to component owner | +| `docs/solver_mrv_index_2026-08-28.md` `/solver_mrv_index_2026-08-28/` | `evidence` | `/evidence/`; linked from optimized component | Keep route and accepted sixth-mechanism evidence | +| `docs/solver_queue_dedup_2026-08-20.md` `/solver_queue_dedup_2026-08-20/` | `evidence` | `/evidence/`; linked from optimized component | Keep route; remove duplicate animation embed and link to component owner | +| `docs/solver_queue_trail_profile_2026-08-20.md` `/solver_queue_trail_profile_2026-08-20/` | `evidence` | `/evidence/` | Keep route and profiling limits | +| `docs/solver_reference_profile_2026-08-17.md` `/solver_reference_profile_2026-08-17/` | `evidence` | `/evidence/`; linked from reference component | Keep route and baseline limits | +| `docs/solver_sat_ownership_2026-08-20.md` `/solver_sat_ownership_2026-08-20/` | `evidence` | `/evidence/`; linked from optimized component | Keep route; remove duplicate animation embed and link to component owner | +| `docs/historical_architecture.md` `/historical_architecture/` | `history` | History group under `/reference/` | Keep route as sole context/download page for original PDF | + +Classification totals are one `story`, 15 `reference`, 11 `evidence`, and one +`history` across the 28 current public page sources. + +## 3. New story-page checklist + +- [ ] Add `/pipeline/` only after its shared composition and source manifest + are validated. +- [ ] Add `/worked-example/` using only `pipeline_sat.cm13`; do not splice in + `unsat-search` frames or timings. +- [ ] Add all eight component routes with the exact frozen section order. +- [ ] Add `/reference/` and `/evidence/` as authored indexes, not generated + prose. +- [ ] Keep history visually distinct inside `/reference/`. +- [ ] Keep `/run-dossiers/` an index; do not render `run.json` as Markdown. +- [ ] Add taxonomy, component-section, primary-owner, semantic-label, + fallback, caption, alt-text, permalink, and generated-output checks. +- [ ] Build Pages without generating any dossier or invoking LaTeX. + +## 4. Public asset inventory + +Each directory row covers every file currently present in that directory. +"Later action" does not authorize changes in this contract-freeze work. + +| Current asset(s) | Current producer/source | Frozen owner | Later action | +| --- | --- | --- | --- | +| `docs/assets/images/builder-routing/{trace.gif,contact-sheet.png,frame-00.png...frame-05.png}` | `render_builder_assets`; reduction v2 manifest and native gadget spans for `pipeline_sat.cm13` | `/components/yang-zhang/` | Relabel `canonical-construction`; retain or replace once; old reference links to owner | +| `docs/assets/images/optimized-mechanisms/{trace.gif,contact-sheet.png,frame-00.png...frame-05.png}` | `render_optimized_assets`; synthetic five-mechanism list | `/components/optimized-solver/` | Replace with six mechanisms including MRV; label `didactic`; all evidence pages link | +| `docs/assets/images/solver-trace/{trace.gif,contact-sheet.png,frame-000000.png,frame-000413.png,frame-000827.png,frame-001240.png,frame-001654.png,frame-002516.png,frame-002517.png,frame-002895.png}` | `render_trace_assets`; complete 2,896-event reference v3 bundle for `pipeline_sat.cm13` | `/components/reference-solver/` | Label `observed`; retain or replace once; contract and serial guide link | +| `docs/assets/images/square-to-hex/{trace.gif,contact-sheet.png,frame-00.png...frame-03.png}` | `render_hex_assets`; checked `tests/fixtures/wang_solution_v1_square_sat.json` | `/components/visualization/` | Replace with canonical SAT witness; label `verified-transformation`; old proof page links | +| `docs/assets/images/z3-encoding/{trace.gif,contact-sheet.png,frame-00.png...frame-04.png}` | Wang `z3-encoding-summary-v1` fixture for `pipeline_sat.cm13` | `/components/wang-z3/` | Label `encoding-order`; retain or replace once; oracle reference links | +| `docs/assets/images/wang-edge-convention.svg` | hand-authored square edge convention, currently referenced only by excluded post template | `/components/tileset/` | Treat as `didactic`; either adopt there or remove only after no source references remain | +| `docs/assets/images/tile-mark.svg` and `docs/_includes/tile-mark.html` | hand-authored site identity | site shell (`docs/_layouts/default.html`) | Retain as chrome; narrative semantic labels do not apply | +| `docs/Wang23_C_OpenMP_Architecture_Spec_Merged.pdf` | original Italian architecture document | `/historical_architecture/` | Retain bytes and sole contextual owner | +| `docs/assets/css/site.css` | site presentation | site shell | Reuse; add only narrative styles justified by final pages | +| `docs/assets/js/document-toc.js` | technical-page TOC enhancement | `docs/_layouts/page.html` | Retain; no dossier dependency | +| all ten modules under `docs/assets/js/wang/` | decorative background field | `docs/_layouts/default.html` | Retain; no semantic or pipeline claim | + +No public bundle may be copied under a second route. If a replacement changes +filenames, update all source links in the same migration and let generated-site +checks prove the old files are unreferenced before deletion. + +## 5. Non-public raster and fixture sources + +- [x] Record `renderer/test_data/pipeline_sat_formula.png`, + `pipeline_sat_reduction.png`, `pipeline_sat_region_square.png`, + `pipeline_sat_region_hex.png`, `pipeline_sat_tileset_square.png`, and + `pipeline_sat_tileset_hex.png` as renderer goldens, not public narrative + ownership. +- [x] Record `renderer/test_data/wang_solution_v1_*` images as renderer + goldens, not proof or public story assets. +- [x] Record legacy renderer input/output PNGs and `renderer/project_python.pdf` + as imported renderer-project material, outside the narrative migration. +- [x] Record `tests/fixtures/pipeline_sat_explain/`, + `pipeline_sat_reduction_explain/`, `pipeline_sat_solver_trace/`, and + `pipeline_sat_z3/` as versioned semantic sources for later shared assets. +- [ ] Do not promote a renderer golden to Pages merely because it is + deterministic; it must have the canonical instance, semantic label, owner, + validator chain, caption, alt text, and fallback required by the contract. + +## 6. Closed-contract inventory + +| Contract | Current canonical documentation | Narrative disposition | +| --- | --- | --- | +| `cm13-formula-snapshot-v1` | `/wang-explainability-snapshots/` | Retain unchanged; bind formula identity into v2 by hash | +| `wang-tileset-snapshot-v1` | `/wang-explainability-snapshots/` | Retain unchanged; source for atomic/generalized presentation | +| `wang-region-snapshot-v1` | `/wang-explainability-snapshots/` | Retain unchanged; source for reduction and region views | +| `wang-reduction-explanation-v1` | `/wang-reduction-explanation/` | Retain unchanged; source for native construction provenance | +| `wang-solution-v1` | `/wang-solution-v1/` | Retain unchanged; sole square witness transport | +| `wang-solver-trace-v1` | `/wang-solver-trace/` | Retain unchanged; sole native event/replay source | +| `z3-encoding-summary-v1` | `/wang_z3_edge_table_2026-08-24/` and snapshot docs | Retain unchanged; distinguish project encoding order from Z3 internals | +| `wang-explain-manifest-v1` | `/wang-explainability-snapshots/` | Retain static-stage meaning | +| `wang-explain-manifest-v2` | `/wang-reduction-explanation/` | Retain provenance-stage meaning | +| `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 | + +- [ ] 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, + 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 + 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 + validation, rendering, Pages build, or PDF formatting. + +## 7. Dossier v1 preservation checklist + +- [x] Four current v1 cases remain: + `sat-end-to-end`, `unsat-root-conflict`, `unsat-propagation`, and + `unsat-search`. +- [x] `sat-end-to-end` and `unsat-search` have no initial-domain overrides; + the two constrained diagnostic cases remain explicitly configured Wang + solves rather than claims about the unconstrained formula. +- [ ] Keep v1 schema bytes/meaning and current cases compatible through every + v2 change. +- [ ] Keep v1 formatter/template isolated from v2; share only focused helpers + behind thin dispatch. +- [ ] Keep v1 atomic destination install, isolated pdfLaTeX, no-shell-escape, + run-specific timing identity, and diagnostic-UNSAT boundary. +- [ ] Run the existing SAT and all three UNSAT v1 dossier tests after each v2 + contract, asset, and PDF change. + +## 8. Shared-asset migration order + +1. [ ] 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 + component identities by SHA-256. +3. [ ] 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, + keeping it secondary to observed trace output. +5. [ ] 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. +7. [ ] Prove every remaining public asset has exactly one embedding owner and + every internal link resolves in generated HTML. + +## 9. Pages implementation gates + +- [ ] Add exactly one public class to every cataloged document and reject + unknown or missing classes. +- [ ] Enforce the nine component sections in order. +- [ ] Enforce one primary asset owner per component and uniqueness across + Pages. +- [ ] Enforce the five allowed semantic labels and reject + `canonical-example`. +- [ ] Enforce GIF owner, nonempty alt text, reduced-motion PNG, caption, + contact sheet, source, and scope. +- [ ] Preserve all current permalinks and validate all literal and generated + links/anchors. +- [ ] Distinguish the general pipeline from the named SAT worked example in + visible copy. +- [ ] Keep technical references and dated evidence available without + duplicating their prose in story pages. +- [ ] Build and check the site with no native build, renderer environment, + dossier generation, or LaTeX installation. + +## 10. V2 PDF implementation gates + +- [ ] Follow the nine-section order frozen in the architecture contract. +- [ ] Consume the same validated facts and static assets as the captured v2 + run; do not consume Pages HTML or Markdown. +- [ ] Embed no GIF/video and perform no second render or replay. +- [ ] Mark assignment, witness, verification, generalized witness, and hex + witness not applicable for UNSAT without fabricating a certificate. +- [ ] Keep raw timings in their named component sections and full detail in the + appendix; make no general performance comparison. +- [ ] Compile with isolated, reproducible, no-shell-escape pdfLaTeX rules. +- [ ] Validate self-containment, hashes, source identity, component agreement, + static-template inputs, and partial-failure cleanup. +- [ ] Prove v1 cases and output contracts remain compatible. + +## 11. Excluded documentation sources + +| Source | Status | Migration rule | +| --- | --- | --- | +| `docs/plans/2026-08-21-witness-extension.md` | completed internal plan | Keep excluded as implementation history | +| `docs/plans/2026-08-25-pages-overview-audit.md` | completed internal audit/plan | Keep excluded; this contract supersedes its deferred sitemap choices where they differ | +| `docs/plans/2026-08-31-narrative-architecture-contract.md` | current internal contract | Keep excluded; downstream implementation references it | +| `docs/plans/2026-08-31-narrative-migration-checklist.md` | current internal checklist | Keep excluded; update checkmarks only with evidence | +| `docs/post-template.md` | excluded authoring scaffold | Keep excluded; do not treat its sample SVG as public ownership | +| `docs/_posts/.gitkeep` | empty placeholder | Keep outside taxonomy until an authored post exists | + +## 12. Final migration audit + +- [ ] The public catalog reports the expected counts for story, reference, + evidence, and history. +- [ ] All 27 legacy technical routes and `/` resolve after the migration. +- [ ] Every new sitemap route resolves with one H1, description, canonical URL, + and expected page class. +- [ ] Every narrative asset has one owner, one source chain, and one allowed + semantic label. +- [ ] No GIF is duplicated, embedded by two owners, missing a static fallback, + or included in a PDF. +- [ ] `pipeline_sat.cm13` identities agree across the worked example, all + engines, verification, presentation, Pages assets, and v2 dossier. +- [ ] `unsat-search` remains visibly and cryptographically separate. +- [ ] Removing documentation and explainability leaves core build, solve, + oracles, verifier, and standard export functional. +- [ ] Full suites, strict compilers, sanitizer, analyzer, dynamic analysis, + applicable profiling, renderer tests, Pages/Jekyll, TeX smoke, diff, secret, + file-mode, and artifact checks are green before publication.