diff --git a/docs/_includes/header.html b/docs/_includes/header.html index 6996e57..a8cb3e2 100644 --- a/docs/_includes/header.html +++ b/docs/_includes/header.html @@ -6,8 +6,10 @@ diff --git a/docs/_includes/narrative-animation.html b/docs/_includes/narrative-animation.html new file mode 100644 index 0000000..ea27580 --- /dev/null +++ b/docs/_includes/narrative-animation.html @@ -0,0 +1,22 @@ +
+ + + {{ include.alt | escape }} + +
+ {{ include.label | escape }}. + {{ include.caption | escape }} + Open the static contact sheet. + Source contract: {{ include.source | escape }}. +
+
diff --git a/docs/_includes/narrative-static.html b/docs/_includes/narrative-static.html new file mode 100644 index 0000000..a7c0355 --- /dev/null +++ b/docs/_includes/narrative-static.html @@ -0,0 +1,15 @@ +
+ {{ include.alt | escape }} +
+ {{ include.label | escape }}. + {{ include.caption | escape }} + Source contract: {{ include.source | escape }}. +
+
diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html index 8634d6d..252de12 100644 --- a/docs/_layouts/default.html +++ b/docs/_layouts/default.html @@ -15,6 +15,8 @@ diff --git a/docs/_layouts/page.html b/docs/_layouts/page.html index 717ce68..7008868 100644 --- a/docs/_layouts/page.html +++ b/docs/_layouts/page.html @@ -3,8 +3,14 @@ ---
+ {% assign catalog_route = '/reference/' %} + {% assign catalog_label = 'Reference' %} + {% if page.page_class == 'evidence' %} + {% assign catalog_route = '/evidence/' %} + {% assign catalog_label = 'Evidence' %} + {% endif %} @@ -37,7 +43,7 @@
diff --git a/docs/_layouts/story.html b/docs/_layouts/story.html new file mode 100644 index 0000000..b396478 --- /dev/null +++ b/docs/_layouts/story.html @@ -0,0 +1,33 @@ +--- +layout: default +--- +
+
+ +

{{ page.description | escape }}

+
+ +
+ {{ content }} +
+ + +
+ diff --git a/docs/assets/css/site.css b/docs/assets/css/site.css index fc281c4..990c9f2 100644 --- a/docs/assets/css/site.css +++ b/docs/assets/css/site.css @@ -329,6 +329,62 @@ figure { color: var(--ink-strong); } +.story-context { + max-width: var(--reading-width); + margin: 0 auto 2rem; + padding-bottom: 1.15rem; + border-bottom: 1px solid var(--rule); + color: var(--muted); + font: 0.68rem/1.5 var(--mono); + letter-spacing: 0.08em; + text-transform: uppercase; +} + +.story-context a { + color: var(--ink); + text-decoration: none; +} + +.story-actions, +.pipeline-links { + display: flex; + flex-wrap: wrap; + gap: 0.7rem 1.4rem; + padding-left: 0; + list-style: none; + font: 0.76rem/1.5 var(--mono); +} + +.narrative-asset { + width: min(100%, 70rem); + margin: 2rem auto; + overflow: hidden; + border: 1px solid var(--rule-strong); + background: var(--black-raised); +} + +.narrative-asset picture, +.narrative-asset img { + display: block; + width: 100%; + height: auto; +} + +.narrative-asset figcaption { + margin: 0; + padding: 1rem 1.15rem; + border-top: 1px solid var(--rule); + color: var(--muted); + font: 0.74rem/1.55 var(--mono); +} + +.narrative-asset .asset-source { + display: block; + margin-top: 0.55rem; + color: var(--faint); + font-size: 0.68rem; +} + .article-abstract { max-width: 40rem; margin: 0; @@ -389,6 +445,7 @@ samp { } :not(pre) > code { + overflow-wrap: anywhere; padding: 0.13em 0.35em; border: 1px solid #292e30; background: #101314; diff --git a/docs/assets/images/solver-trace/contact-sheet.png b/docs/assets/images/solver-trace/contact-sheet.png deleted file mode 100644 index 425e409..0000000 Binary files a/docs/assets/images/solver-trace/contact-sheet.png and /dev/null differ diff --git a/docs/assets/images/wang-edge-convention.svg b/docs/assets/images/wang-edge-convention.svg deleted file mode 100644 index 0742a9d..0000000 --- a/docs/assets/images/wang-edge-convention.svg +++ /dev/null @@ -1,17 +0,0 @@ - - Wang tile edge convention - A square split into north, east, south, and west triangles meeting at the center. - - - - - - - - - NORTH - EAST - SOUTH - WEST - - diff --git a/docs/assets/narrative/boolean-z3/contact-sheet.png b/docs/assets/narrative/boolean-z3/contact-sheet.png new file mode 100644 index 0000000..98c96c9 Binary files /dev/null and b/docs/assets/narrative/boolean-z3/contact-sheet.png differ diff --git a/docs/assets/narrative/boolean-z3/frame-00.png b/docs/assets/narrative/boolean-z3/frame-00.png new file mode 100644 index 0000000..4afc116 Binary files /dev/null and b/docs/assets/narrative/boolean-z3/frame-00.png differ diff --git a/docs/assets/narrative/boolean-z3/frame-01.png b/docs/assets/narrative/boolean-z3/frame-01.png new file mode 100644 index 0000000..93e751f Binary files /dev/null and b/docs/assets/narrative/boolean-z3/frame-01.png differ diff --git a/docs/assets/narrative/boolean-z3/frame-02.png b/docs/assets/narrative/boolean-z3/frame-02.png new file mode 100644 index 0000000..7a8c0b4 Binary files /dev/null and b/docs/assets/narrative/boolean-z3/frame-02.png differ diff --git a/docs/assets/narrative/boolean-z3/frame-03.png b/docs/assets/narrative/boolean-z3/frame-03.png new file mode 100644 index 0000000..b8ea254 Binary files /dev/null and b/docs/assets/narrative/boolean-z3/frame-03.png differ diff --git a/docs/assets/narrative/boolean-z3/trace.gif b/docs/assets/narrative/boolean-z3/trace.gif new file mode 100644 index 0000000..66e4ba3 Binary files /dev/null and b/docs/assets/narrative/boolean-z3/trace.gif differ diff --git a/docs/assets/narrative/formula.png b/docs/assets/narrative/formula.png new file mode 100644 index 0000000..b7592ad Binary files /dev/null and b/docs/assets/narrative/formula.png differ diff --git a/docs/assets/narrative/generalized-tiles/atomic-legend.png b/docs/assets/narrative/generalized-tiles/atomic-legend.png new file mode 100644 index 0000000..c23650c Binary files /dev/null and b/docs/assets/narrative/generalized-tiles/atomic-legend.png differ diff --git a/docs/assets/narrative/generalized-tiles/sheet.png b/docs/assets/narrative/generalized-tiles/sheet.png new file mode 100644 index 0000000..11eb7a7 Binary files /dev/null and b/docs/assets/narrative/generalized-tiles/sheet.png differ diff --git a/docs/assets/narrative/manifest.json b/docs/assets/narrative/manifest.json new file mode 100644 index 0000000..917a285 --- /dev/null +++ b/docs/assets/narrative/manifest.json @@ -0,0 +1,799 @@ +{ + "schema": "wang-narrative-assets-v1", + "product": "canonical-pages", + "case": { + "id": "pipeline-sat-v2", + "expected_status": "sat", + "source_sha256": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542" + }, + "identities": { + "source_formula": "3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542", + "formula_snapshot": "5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815", + "tileset": "462a102690c420bfe52a634e7b365a6be3bfcf59169f0acd96264831196723fa", + "region": "aad4dc7dcb46ed070995bf975248a7f2f0bf27d69db3eb653208d08c5826199a", + "provenance": "6abbea9333509f852d59ed9be943d76380a49bfbdcf0f1c13e923e9ec4c4f3e2", + "boolean_z3_summary": "c0213b57faade9f61c7b0f31813f0b91322a7484d383d7971e3f554dbc4ae214", + "reference_trace_manifest": "2134fe7587b71ca245b7e2820c5cbcc1c9d469ac537f246a6021108b776e2f57", + "reference_trace": "4a3ad4cbb476949a61db74dbc22696bc8ef69cb9e6226b816495a0b10322628c", + "reference_solution": "2273f58cda026dca73c0dfa25c960e01296ac1e34ae6accbddf5be29034d156a", + "optimized_trace_manifest": "9646e24077890a86e32b4d974d18c6a60b2de7dc2612beac39ab455dc9493699", + "optimized_trace": "92e4389e7eba41fa9c075b21f1dc19700c2a039add2d7449b01c83d163525bc0", + "optimized_solution": "9c02aea7867d26514d013dc44ea1d7e105ae86ddeef1ff247e0311e3c030377d", + "wang_z3_summary": "a150dc76e2193d9ae65e165b8555df4b269afcbe572c6d55026a97d0765fb62b" + }, + "animations": { + "pipeline_overview": { + "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": "197f9a2d1b55722b1680c3b04443c1ea183ad37340cfeacce4aadb5d867d8b18", + "producer": "dossier.narrative_assets", + "validator": "formats.run_dossier_v2_bundle.load_run_dossier_v2", + "compositor": "renderer.wang_narrative.render_overview_assets", + "scope": { + "complete": true, + "selected": true, + "truncated": false + }, + "animation": { + "path": "pipeline-overview/trace.gif", + "sha256": "a6bfed665e4f2861b4755ddbd86d6a388c33c83355cfe54e92c1ad6df71e6b08", + "media_type": "image/gif" + }, + "fallback": { + "path": "pipeline-overview/frame-07.png", + "sha256": "a7199a7372405572d5b1aca0c36ca8a4258bdd610d9fb3ecf88ba7acd07c05d9", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "pipeline-overview/contact-sheet.png", + "sha256": "f57d90bb9f66511d4217a5ac9599e0f2d8b414f69ae4b9dbbf2c680b30083031", + "media_type": "image/png" + }, + "frames": [ + { + "path": "pipeline-overview/frame-00.png", + "sha256": "035a5fe720745671248735debc42c740184db64be179980b4fcd114ccfc7d6f3", + "media_type": "image/png" + }, + { + "path": "pipeline-overview/frame-01.png", + "sha256": "5ce0045655044abffdc093f43fc0bcefc25245baa74a36d6a845d5bf18e78151", + "media_type": "image/png" + }, + { + "path": "pipeline-overview/frame-02.png", + "sha256": "9ba1499f598142daf6e102c8d98a59b106116fbd9418e8252aeb67d8a2e52592", + "media_type": "image/png" + }, + { + "path": "pipeline-overview/frame-03.png", + "sha256": "290d4663c000298f68583ccf7952109fd9784d8ea91771cd41edb1090eb58885", + "media_type": "image/png" + }, + { + "path": "pipeline-overview/frame-04.png", + "sha256": "5981d818629ea64b4742c76da2caf20bff4c59b03ea91986c49058f42cdd0a5e", + "media_type": "image/png" + }, + { + "path": "pipeline-overview/frame-05.png", + "sha256": "a20b6e761b9e8dc09db2a50cf37ce3579717f90c61151cf378ee2ab4fc5ae857", + "media_type": "image/png" + }, + { + "path": "pipeline-overview/frame-06.png", + "sha256": "9f5e7f2b1beb929ce0a0451e015018a5aaf54456378d752553f7ff78eb3c1cfe", + "media_type": "image/png" + }, + { + "path": "pipeline-overview/frame-07.png", + "sha256": "a7199a7372405572d5b1aca0c36ca8a4258bdd610d9fb3ecf88ba7acd07c05d9", + "media_type": "image/png" + } + ] + }, + "boolean_z3": { + "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": "c0213b57faade9f61c7b0f31813f0b91322a7484d383d7971e3f554dbc4ae214", + "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", + "scope": { + "complete": true, + "selected": false, + "truncated": false + }, + "animation": { + "path": "boolean-z3/trace.gif", + "sha256": "724aeb4c06babd8fd14e5b541198e0d6a7edbbb27f2376f6b5cd4db9c279ac71", + "media_type": "image/gif" + }, + "fallback": { + "path": "boolean-z3/frame-02.png", + "sha256": "a2991b1e2781d51192347e3fd76f3264527ae7ceafb644ed81805e2ea08f2a44", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "boolean-z3/contact-sheet.png", + "sha256": "acd7b8cf0fb8769adcc2c743edc41bfa2eb87f2f38f1327b10691cb7ddfc9800", + "media_type": "image/png" + }, + "frames": [ + { + "path": "boolean-z3/frame-00.png", + "sha256": "ff9f45064c479dbd4e77482af090201af9786a5d4202738077201db733f47de0", + "media_type": "image/png" + }, + { + "path": "boolean-z3/frame-01.png", + "sha256": "c1ffee1bc549c7d9a739ad3a894f5cec5c3af77baa57f81d2a56dfc210a78125", + "media_type": "image/png" + }, + { + "path": "boolean-z3/frame-02.png", + "sha256": "a2991b1e2781d51192347e3fd76f3264527ae7ceafb644ed81805e2ea08f2a44", + "media_type": "image/png" + }, + { + "path": "boolean-z3/frame-03.png", + "sha256": "8f742d1e90d4eb554d9cd485860fb107afabda9282845a71c1f8505fa4e069af", + "media_type": "image/png" + } + ] + }, + "region_construction": { + "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": "6abbea9333509f852d59ed9be943d76380a49bfbdcf0f1c13e923e9ec4c4f3e2", + "producer": "formats.solver_trace_snapshot.dump_solver_trace_bundle", + "validator": "renderer.wang_snapshot.load_explainability_bundle", + "compositor": "renderer.wang_algorithm_animation.render_builder_assets", + "scope": { + "complete": true, + "selected": true, + "truncated": false + }, + "animation": { + "path": "region-construction/trace.gif", + "sha256": "7a5e3938527a3d2ed4a1e90d0ae01cd694d5e632f0f637ca5c76b2693d7edf64", + "media_type": "image/gif" + }, + "fallback": { + "path": "region-construction/frame-04.png", + "sha256": "ba4c03ddb50f4cf2a3bfe492b23f1c95a4ceed62cf40764bbb55a82272a9f5ab", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "region-construction/contact-sheet.png", + "sha256": "b00710859c6f96efc972d1a999c867465b91a5e6903d120cc776e0a0048c1a96", + "media_type": "image/png" + }, + "frames": [ + { + "path": "region-construction/frame-00.png", + "sha256": "8dfb4ca866b5503375fe9dad3611522d8ff8b5e5b997033f8116d8439b383a71", + "media_type": "image/png" + }, + { + "path": "region-construction/frame-01.png", + "sha256": "9181341338b5bc21798d1715ecce20c799def0a62f9c7115e6edc1d0cfe89cb1", + "media_type": "image/png" + }, + { + "path": "region-construction/frame-02.png", + "sha256": "d95745a1d26f63679f3ae5b416ed3371bc9ee96c7571ce2909cea57739903d96", + "media_type": "image/png" + }, + { + "path": "region-construction/frame-03.png", + "sha256": "b355cf3531374a02ea0812aa80847d339090b6a88da1657789e17143fe250d3b", + "media_type": "image/png" + }, + { + "path": "region-construction/frame-04.png", + "sha256": "ba4c03ddb50f4cf2a3bfe492b23f1c95a4ceed62cf40764bbb55a82272a9f5ab", + "media_type": "image/png" + }, + { + "path": "region-construction/frame-05.png", + "sha256": "4e700c2bdefa0315b177e225b4d069058b38815c0cf57980f45303323a662829", + "media_type": "image/png" + } + ] + }, + "reference_trace": { + "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": "2134fe7587b71ca245b7e2820c5cbcc1c9d469ac537f246a6021108b776e2f57", + "producer": "formats.solver_trace_snapshot.dump_solver_trace_bundle", + "validator": "renderer.wang_trace.load_trace_bundle", + "compositor": "renderer.wang_trace_render.render_trace_assets", + "scope": { + "complete": true, + "selected": true, + "truncated": false + }, + "animation": { + "path": "reference-trace/trace.gif", + "sha256": "bd9b88a90a41f079987ba3de6d3982f7eef2fb3823e0f5e30f69979d079b7ce3", + "media_type": "image/gif" + }, + "fallback": { + "path": "reference-trace/frame-002517.png", + "sha256": "a0e5619938a6ce5a370935420b66bb2dda997e898a4c0b9d8edcc648f0f40e62", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "reference-trace/contact-sheet.png", + "sha256": "6e54fc956d2f750e49ef31e6b01312d377c1de2a845cf0fcd29907b52b02b236", + "media_type": "image/png" + }, + "frames": [ + { + "path": "reference-trace/frame-000000.png", + "sha256": "38cc17f0f06068f2c19aafc43b53bb877e03140c7dc362ed2e9149e62405c8cc", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-000001.png", + "sha256": "6c1dcde135d552722b1a5983502b739c192227b601b4592869d36733347cd4fd", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-001258.png", + "sha256": "fb8ae6449ddcf336d4116c13e01734d2426f661210a854014a8c7847391cbddd", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-001887.png", + "sha256": "863753a075613f19948d2195f67a4c45c327e665fea23b611848f1d10d5bf3f3", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-002516.png", + "sha256": "5587f030f1655a84bf7a0170ed6e2843cd019989742630d4f7ce086f29e17cb2", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-002517.png", + "sha256": "a0e5619938a6ce5a370935420b66bb2dda997e898a4c0b9d8edcc648f0f40e62", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-002518.png", + "sha256": "63ef43ee6d99ea6250196a52d657c71dc1421fef278f275a92d6b4f0d2370e75", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-002893.png", + "sha256": "25337a3aa0bd9bc9a054e176e526c621587356588395960da03c69d98777fcd1", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-002894.png", + "sha256": "d83f134bae8c463108457486886979c749e231ff0624bf807eeed5126beb2414", + "media_type": "image/png" + }, + { + "path": "reference-trace/frame-002895.png", + "sha256": "abcdb03dd746ee8e7588a4d9c0341a2958e5a81e0ee35cde005e9add2f3ec0ea", + "media_type": "image/png" + } + ] + }, + "optimized_trace": { + "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": "9646e24077890a86e32b4d974d18c6a60b2de7dc2612beac39ab455dc9493699", + "producer": "formats.solver_trace_snapshot.dump_solver_trace_bundle", + "validator": "renderer.wang_trace.load_trace_bundle", + "compositor": "renderer.wang_trace_render.render_trace_assets", + "scope": { + "complete": true, + "selected": true, + "truncated": false + }, + "animation": { + "path": "optimized-trace/trace.gif", + "sha256": "e65aabffac9f8e72458bdd1bbebf57cf3a6c96763f1229997ef72ded5d456620", + "media_type": "image/gif" + }, + "fallback": { + "path": "optimized-trace/frame-002562.png", + "sha256": "ad118624dc3350d399c8ff84924dd49754e03c1a554dc1c862057c05c98ab79f", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "optimized-trace/contact-sheet.png", + "sha256": "4fbf79fad2e8226ae14b7bb6c6c2b7b8e66890420b3aad5a712ba70e8ee78922", + "media_type": "image/png" + }, + "frames": [ + { + "path": "optimized-trace/frame-000000.png", + "sha256": "bd190ac15f769b666215f6c88071ebea8be864bf53ee794a31caa086f26e3eb6", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-000001.png", + "sha256": "d8a852c029d862b7f9e50a02a137033d07fc94f67e39519007c6fd7b3ae79505", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-000641.png", + "sha256": "4573fb517160ac2d415eddd1d332880b984be7f699696870de1081ca6c38c887", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-001281.png", + "sha256": "49d370ff9376595252f1aae7b936c57dbeb407a4cba26de49403972181a5cb5d", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-002561.png", + "sha256": "832884d407c0463e32365d8741b2c834a7525d6b8d5c65a3a74f0a43d5083ca8", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-002562.png", + "sha256": "ad118624dc3350d399c8ff84924dd49754e03c1a554dc1c862057c05c98ab79f", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-002563.png", + "sha256": "44298474500d368c92d9286c55f409ec82885f8c466b50641800a9b95bce9483", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-002938.png", + "sha256": "d28144f3f7f1949584b8c62ab7602bdf9ebbe419e338be4996a0a2c1548b51b6", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-002939.png", + "sha256": "843345eb090bf4b2530a765e9fbbcd01d38acb880c28d7f10a05e0e910fafff0", + "media_type": "image/png" + }, + { + "path": "optimized-trace/frame-002940.png", + "sha256": "ce8fa205d52a9185a54f8e978e1da989774448e09ea8d28a72b775be3c8cf2ee", + "media_type": "image/png" + } + ] + }, + "wang_z3": { + "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": "a150dc76e2193d9ae65e165b8555df4b269afcbe572c6d55026a97d0765fb62b", + "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", + "scope": { + "complete": true, + "selected": false, + "truncated": false + }, + "animation": { + "path": "wang-z3/trace.gif", + "sha256": "f6c93f5ee0914113b188d659012b92c4bb3f094c3a1f7f93c6b16c7e09e2d06c", + "media_type": "image/gif" + }, + "fallback": { + "path": "wang-z3/frame-03.png", + "sha256": "48a850e4f5d335bc6562e37563d345de83ec838941aa9990ca61da5d08d672b4", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "wang-z3/contact-sheet.png", + "sha256": "a8a93a04a0df6558874086a7766d79422799d5782395843f61758b5889815606", + "media_type": "image/png" + }, + "frames": [ + { + "path": "wang-z3/frame-00.png", + "sha256": "74e6ffcf5e70386304af308cf6587491ff128d93d96f1caeba810f30e7dd3868", + "media_type": "image/png" + }, + { + "path": "wang-z3/frame-01.png", + "sha256": "dc6d7e04cd37bf313a5be866e62b653cc45cb07ad65567294db28a8ad7f946db", + "media_type": "image/png" + }, + { + "path": "wang-z3/frame-02.png", + "sha256": "5ea43effac89a4b4b7d235c841abc8301562a9b29bd720951394f812a2abb970", + "media_type": "image/png" + }, + { + "path": "wang-z3/frame-03.png", + "sha256": "48a850e4f5d335bc6562e37563d345de83ec838941aa9990ca61da5d08d672b4", + "media_type": "image/png" + }, + { + "path": "wang-z3/frame-04.png", + "sha256": "1414ec4028027935cb36c2db02afd97d2b87b61196d9c4d7dff236710adb3509", + "media_type": "image/png" + } + ] + }, + "verification": { + "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": "a47f7172f07dd65be697be97dab5ab608b07f4d0fb139e10ebc3a1a621da17e3", + "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", + "scope": { + "complete": true, + "selected": false, + "truncated": false + }, + "animation": { + "path": "verification/trace.gif", + "sha256": "04f4ed56ed1da0ca40b60b964732647a81c42746841965f422ba4438e241e76f", + "media_type": "image/gif" + }, + "fallback": { + "path": "verification/frame-05.png", + "sha256": "98edd0a7e37c2ac38e4b9ee853607a3ed003d5be3df50beb3dea1ab7101d246d", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "verification/contact-sheet.png", + "sha256": "de396acac387952b1591329d040d31150375bbcb043810f1fa9aa8b8b938335f", + "media_type": "image/png" + }, + "frames": [ + { + "path": "verification/frame-00.png", + "sha256": "13fa18831f69137ee961a8f1d2b5f88a9429fa4057747dae51ed28001500cd6f", + "media_type": "image/png" + }, + { + "path": "verification/frame-01.png", + "sha256": "8ca06c4f98766b88a47a7eb39c385ad2e746d146179bf280e89cb3d559f532a0", + "media_type": "image/png" + }, + { + "path": "verification/frame-02.png", + "sha256": "5b6f321887b36fab1989bf6b9b42373c56d6f6c24c0f59e42037d02e9dd749b2", + "media_type": "image/png" + }, + { + "path": "verification/frame-03.png", + "sha256": "48dd44e40082bcd220b22ab255fb228b6398fbe58a338499d5595676027889f8", + "media_type": "image/png" + }, + { + "path": "verification/frame-04.png", + "sha256": "2b29f63fcac42416a2fcf02f2ee098ee1c54d99f260a684f97607d68488dacb3", + "media_type": "image/png" + }, + { + "path": "verification/frame-05.png", + "sha256": "98edd0a7e37c2ac38e4b9ee853607a3ed003d5be3df50beb3dea1ab7101d246d", + "media_type": "image/png" + } + ] + }, + "witness_presentation": { + "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": "30e43f79c5967c481c781ae975327c1af9cf8a941677d65841fe20f06aa34af0", + "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", + "scope": { + "complete": true, + "selected": false, + "truncated": false + }, + "animation": { + "path": "presentation/trace.gif", + "sha256": "fd23bfddb27ca4e74de58e9ae5adbffbcc66d01b0fd086cb1564dc99c3ccf42f", + "media_type": "image/gif" + }, + "fallback": { + "path": "presentation/frame-03.png", + "sha256": "52d75fecd13738c85d10a8179a77ba976ea2a2a26cc0e691e2388c26c57e16bd", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "presentation/contact-sheet.png", + "sha256": "1b5b6d177f8ad99765bc2aa86cf36a028bd6fc0785b61ed9014ffd439ce4fd11", + "media_type": "image/png" + }, + "frames": [ + { + "path": "presentation/frame-00.png", + "sha256": "c7fb208c02038fc6a8f9c6b7b75447c1abab14de90a27288b6eff09c3a349719", + "media_type": "image/png" + }, + { + "path": "presentation/frame-01.png", + "sha256": "13845f481415f3b0a8b8920578d6068f7a4b3ab1822ae09e346bb8556b48c3e2", + "media_type": "image/png" + }, + { + "path": "presentation/frame-02.png", + "sha256": "5b37808d37f863385be683950a6262cf9cab4974fbd107f40036f810b37d9507", + "media_type": "image/png" + }, + { + "path": "presentation/frame-03.png", + "sha256": "52d75fecd13738c85d10a8179a77ba976ea2a2a26cc0e691e2388c26c57e16bd", + "media_type": "image/png" + } + ] + }, + "optimized_mechanisms": { + "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": "5f0c6e1f80601f6112ae8e358fe8029fa3d94fd260693edf0b37ea474419f212", + "producer": "renderer/data/optimized-mechanisms-v1.json", + "validator": "renderer.wang_algorithm_animation._load_optimizations", + "compositor": "renderer.wang_algorithm_animation.render_optimized_assets", + "scope": { + "complete": true, + "selected": false, + "truncated": false + }, + "animation": { + "path": "optimized-mechanisms/trace.gif", + "sha256": "148f55b4796e04dc4fb3fb020608879422d8448095115f93154449351ebe9fd3", + "media_type": "image/gif" + }, + "fallback": { + "path": "optimized-mechanisms/frame-06.png", + "sha256": "1335f54b894100393d7bcbaf68558a879c60169dbb590c87014db496fbc33e83", + "media_type": "image/png" + }, + "contact_sheet": { + "path": "optimized-mechanisms/contact-sheet.png", + "sha256": "789efc596c7e0b853ee3d057f39b48595d9a8230ef9635fedaafc7ff75e30664", + "media_type": "image/png" + }, + "frames": [ + { + "path": "optimized-mechanisms/frame-00.png", + "sha256": "3c25541c2b85ea2785f2d58e02cf1afb9f2d301e3ea35e3ea51b721afeeba906", + "media_type": "image/png" + }, + { + "path": "optimized-mechanisms/frame-01.png", + "sha256": "49cf477983620cc0f0c1faf5efb67ba7098ff07b0664cb39efa21cb5be3d5ceb", + "media_type": "image/png" + }, + { + "path": "optimized-mechanisms/frame-02.png", + "sha256": "80fdfa6e029b2f5165d1ea499ba27e33b3d18d315fc97dc19c1b8f6be46ac3b5", + "media_type": "image/png" + }, + { + "path": "optimized-mechanisms/frame-03.png", + "sha256": "6fabbde7c8ca8543bfc6ce41ae2724ad59037d85516f2b12f4d2ae6f7d5eeb49", + "media_type": "image/png" + }, + { + "path": "optimized-mechanisms/frame-04.png", + "sha256": "b3deccba1235538143021207c332c19377142d47326215cdd2f6a68a1483225d", + "media_type": "image/png" + }, + { + "path": "optimized-mechanisms/frame-05.png", + "sha256": "ee34b6de2c6d72a3c465423a18302295c1921d300fe0c2501522756e69a2f9ab", + "media_type": "image/png" + }, + { + "path": "optimized-mechanisms/frame-06.png", + "sha256": "1335f54b894100393d7bcbaf68558a879c60169dbb590c87014db496fbc33e83", + "media_type": "image/png" + } + ] + } + }, + "statics": { + "home_preview": { + "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": "2273f58cda026dca73c0dfa25c960e01296ac1e34ae6accbddf5be29034d156a", + "producer": "dossier.narrative_assets", + "validator": "formats.run_dossier_v2_bundle.load_run_dossier_v2", + "compositor": "renderer.wang_narrative.render_overview_assets", + "artifact": { + "path": "pipeline-overview/home-preview.png", + "sha256": "84d555657f7d8977a4ba6ccbeab99eb769c0404698e4aec7eaea1a2ce90ae05f", + "media_type": "image/png" + } + }, + "worked_example": { + "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": "197f9a2d1b55722b1680c3b04443c1ea183ad37340cfeacce4aadb5d867d8b18", + "producer": "dossier.narrative_assets", + "validator": "formats.run_dossier_v2_bundle.load_run_dossier_v2", + "compositor": "renderer.wang_narrative.render_overview_assets", + "artifact": { + "path": "pipeline-overview/worked-example.png", + "sha256": "8f56f45967a9c68aa0f42e6478a9953b8c1ae6b418d09080c9fd52ebe2b8c1af", + "media_type": "image/png" + } + }, + "formula": { + "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": "5098eb9a85adebf28757b1368e9307fdb5fea0617de3256b717ead1af1d67815", + "producer": "dossier.narrative_assets", + "validator": "renderer.wang_snapshot.load_explainability_bundle", + "compositor": "renderer.wang_snapshot.render_pipeline_snapshot", + "artifact": { + "path": "formula.png", + "sha256": "381879859d1987cb8b2b6e7b65ed9e51d9580972e8d87ea118c1b21c5e2b6c11", + "media_type": "image/png" + } + }, + "generalized_sheet": { + "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": "ce7331049b9bbec8e481bef7e332eaa6e10b6232351282c120dc5d460b218c0d", + "producer": "dossier.narrative_assets", + "validator": "renderer.wang_snapshot.load_explainability_bundle+renderer.wang_generalized.check_canonical_atomic_tileset", + "compositor": "renderer.wang_narrative.render_generalized_assets", + "artifact": { + "path": "generalized-tiles/sheet.png", + "sha256": "753b1042553aa8dfe347fada252bd7cbed1b8cb2f41b4b40d08864da282d7830", + "media_type": "image/png" + } + }, + "atomic_legend": { + "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": "ce7331049b9bbec8e481bef7e332eaa6e10b6232351282c120dc5d460b218c0d", + "producer": "dossier.narrative_assets", + "validator": "renderer.wang_snapshot.load_explainability_bundle+renderer.wang_generalized.check_canonical_atomic_tileset", + "compositor": "renderer.wang_narrative.render_generalized_assets", + "artifact": { + "path": "generalized-tiles/atomic-legend.png", + "sha256": "e93c587b15ba9810b610688e614ecf4b51cc46be25ab677dc44a6e71b3e2b315", + "media_type": "image/png" + } + }, + "square_presentation": { + "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": "2273f58cda026dca73c0dfa25c960e01296ac1e34ae6accbddf5be29034d156a", + "producer": "dossier.narrative_assets", + "validator": "renderer.wang_square.load_wang_presentation", + "compositor": "renderer.wang_narrative.render_witness_assets", + "artifact": { + "path": "presentation/square.png", + "sha256": "6bfdf8b9545e35a54d1f64b2477235488b270027f3c10775cf3fa41dd0530707", + "media_type": "image/png" + } + }, + "generalized_presentation": { + "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": "5df89e1b413106a7d61478194eb0f37d3a68a3add1da16b2158e391ad943c10e", + "producer": "dossier.narrative_assets", + "validator": "renderer.wang_square.load_wang_presentation+renderer.wang_generalized.recognize_generalized_tiles", + "compositor": "renderer.wang_narrative.render_witness_assets", + "artifact": { + "path": "presentation/generalized.png", + "sha256": "86fe403887af74ac642afcf834e2a8fd79643c68297aa6b5371752fd45ebd2a1", + "media_type": "image/png" + } + }, + "hex_presentation": { + "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": "308c9bfa297bde34b6c85711f3c21e5d42604b5356863700dff65305b8a16c4e", + "producer": "dossier.narrative_assets", + "validator": "renderer.wang_square.load_wang_presentation+renderer.wang_hex_port.check_square_to_hex", + "compositor": "renderer.wang_narrative.render_witness_assets", + "artifact": { + "path": "presentation/hex.png", + "sha256": "0f5a968eaa8175b699739823318f6f12fed8ec28be148f3338ec7e8120bbc554", + "media_type": "image/png" + } + }, + "presentation_status": null + }, + "pdf_milestones": { + "selector": "semantic-milestones-v1", + "region_construction": [ + "region-construction/frame-00.png", + "region-construction/frame-01.png", + "region-construction/frame-02.png", + "region-construction/frame-03.png", + "region-construction/frame-04.png", + "region-construction/frame-05.png" + ], + "reference_trace": [ + "reference-trace/frame-000000.png", + "reference-trace/frame-000001.png", + "reference-trace/frame-001258.png", + "reference-trace/frame-001887.png", + "reference-trace/frame-002516.png", + "reference-trace/frame-002517.png", + "reference-trace/frame-002518.png", + "reference-trace/frame-002893.png", + "reference-trace/frame-002894.png", + "reference-trace/frame-002895.png" + ], + "optimized_trace": [ + "optimized-trace/frame-000000.png", + "optimized-trace/frame-000001.png", + "optimized-trace/frame-000641.png", + "optimized-trace/frame-001281.png", + "optimized-trace/frame-002561.png", + "optimized-trace/frame-002562.png", + "optimized-trace/frame-002563.png", + "optimized-trace/frame-002938.png", + "optimized-trace/frame-002939.png", + "optimized-trace/frame-002940.png" + ], + "end_to_end": [ + "pipeline-overview/frame-00.png", + "pipeline-overview/frame-01.png", + "pipeline-overview/frame-02.png", + "pipeline-overview/frame-03.png", + "pipeline-overview/frame-04.png", + "pipeline-overview/frame-05.png", + "pipeline-overview/frame-06.png", + "pipeline-overview/frame-07.png" + ] + } +} diff --git a/docs/assets/images/optimized-mechanisms/contact-sheet.png b/docs/assets/narrative/optimized-mechanisms/contact-sheet.png similarity index 100% rename from docs/assets/images/optimized-mechanisms/contact-sheet.png rename to docs/assets/narrative/optimized-mechanisms/contact-sheet.png diff --git a/docs/assets/images/optimized-mechanisms/frame-00.png b/docs/assets/narrative/optimized-mechanisms/frame-00.png similarity index 100% rename from docs/assets/images/optimized-mechanisms/frame-00.png rename to docs/assets/narrative/optimized-mechanisms/frame-00.png diff --git a/docs/assets/images/optimized-mechanisms/frame-01.png b/docs/assets/narrative/optimized-mechanisms/frame-01.png similarity index 100% rename from docs/assets/images/optimized-mechanisms/frame-01.png rename to docs/assets/narrative/optimized-mechanisms/frame-01.png diff --git a/docs/assets/images/optimized-mechanisms/frame-02.png b/docs/assets/narrative/optimized-mechanisms/frame-02.png similarity index 100% rename from docs/assets/images/optimized-mechanisms/frame-02.png rename to docs/assets/narrative/optimized-mechanisms/frame-02.png diff --git a/docs/assets/images/optimized-mechanisms/frame-03.png b/docs/assets/narrative/optimized-mechanisms/frame-03.png similarity index 100% rename from docs/assets/images/optimized-mechanisms/frame-03.png rename to docs/assets/narrative/optimized-mechanisms/frame-03.png diff --git a/docs/assets/images/optimized-mechanisms/frame-04.png b/docs/assets/narrative/optimized-mechanisms/frame-04.png similarity index 100% rename from docs/assets/images/optimized-mechanisms/frame-04.png rename to docs/assets/narrative/optimized-mechanisms/frame-04.png diff --git a/docs/assets/images/optimized-mechanisms/frame-05.png b/docs/assets/narrative/optimized-mechanisms/frame-05.png similarity index 100% rename from docs/assets/images/optimized-mechanisms/frame-05.png rename to docs/assets/narrative/optimized-mechanisms/frame-05.png diff --git a/docs/assets/images/optimized-mechanisms/frame-06.png b/docs/assets/narrative/optimized-mechanisms/frame-06.png similarity index 100% rename from docs/assets/images/optimized-mechanisms/frame-06.png rename to docs/assets/narrative/optimized-mechanisms/frame-06.png diff --git a/docs/assets/images/optimized-mechanisms/trace.gif b/docs/assets/narrative/optimized-mechanisms/trace.gif similarity index 100% rename from docs/assets/images/optimized-mechanisms/trace.gif rename to docs/assets/narrative/optimized-mechanisms/trace.gif diff --git a/docs/assets/narrative/optimized-trace/contact-sheet.png b/docs/assets/narrative/optimized-trace/contact-sheet.png new file mode 100644 index 0000000..97c983f Binary files /dev/null and b/docs/assets/narrative/optimized-trace/contact-sheet.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-000000.png b/docs/assets/narrative/optimized-trace/frame-000000.png new file mode 100644 index 0000000..e75bf67 Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-000000.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-000001.png b/docs/assets/narrative/optimized-trace/frame-000001.png new file mode 100644 index 0000000..04a6a6c Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-000001.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-000641.png b/docs/assets/narrative/optimized-trace/frame-000641.png new file mode 100644 index 0000000..ef40d75 Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-000641.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-001281.png b/docs/assets/narrative/optimized-trace/frame-001281.png new file mode 100644 index 0000000..55ec437 Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-001281.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-002561.png b/docs/assets/narrative/optimized-trace/frame-002561.png new file mode 100644 index 0000000..2474cbe Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-002561.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-002562.png b/docs/assets/narrative/optimized-trace/frame-002562.png new file mode 100644 index 0000000..3b9f7c7 Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-002562.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-002563.png b/docs/assets/narrative/optimized-trace/frame-002563.png new file mode 100644 index 0000000..b1b6404 Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-002563.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-002938.png b/docs/assets/narrative/optimized-trace/frame-002938.png new file mode 100644 index 0000000..855c8a3 Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-002938.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-002939.png b/docs/assets/narrative/optimized-trace/frame-002939.png new file mode 100644 index 0000000..3ba5f3c Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-002939.png differ diff --git a/docs/assets/narrative/optimized-trace/frame-002940.png b/docs/assets/narrative/optimized-trace/frame-002940.png new file mode 100644 index 0000000..2aa04f1 Binary files /dev/null and b/docs/assets/narrative/optimized-trace/frame-002940.png differ diff --git a/docs/assets/narrative/optimized-trace/trace.gif b/docs/assets/narrative/optimized-trace/trace.gif new file mode 100644 index 0000000..92a4eba Binary files /dev/null and b/docs/assets/narrative/optimized-trace/trace.gif differ diff --git a/docs/assets/narrative/pipeline-overview/contact-sheet.png b/docs/assets/narrative/pipeline-overview/contact-sheet.png new file mode 100644 index 0000000..ddddd8a Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/contact-sheet.png differ diff --git a/docs/assets/narrative/pipeline-overview/frame-00.png b/docs/assets/narrative/pipeline-overview/frame-00.png new file mode 100644 index 0000000..9e5b608 Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/frame-00.png differ diff --git a/docs/assets/narrative/pipeline-overview/frame-01.png b/docs/assets/narrative/pipeline-overview/frame-01.png new file mode 100644 index 0000000..400f498 Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/frame-01.png differ diff --git a/docs/assets/narrative/pipeline-overview/frame-02.png b/docs/assets/narrative/pipeline-overview/frame-02.png new file mode 100644 index 0000000..1394e0d Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/frame-02.png differ diff --git a/docs/assets/narrative/pipeline-overview/frame-03.png b/docs/assets/narrative/pipeline-overview/frame-03.png new file mode 100644 index 0000000..49a1687 Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/frame-03.png differ diff --git a/docs/assets/narrative/pipeline-overview/frame-04.png b/docs/assets/narrative/pipeline-overview/frame-04.png new file mode 100644 index 0000000..ea47e22 Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/frame-04.png differ diff --git a/docs/assets/narrative/pipeline-overview/frame-05.png b/docs/assets/narrative/pipeline-overview/frame-05.png new file mode 100644 index 0000000..d2ccdb4 Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/frame-05.png differ diff --git a/docs/assets/narrative/pipeline-overview/frame-06.png b/docs/assets/narrative/pipeline-overview/frame-06.png new file mode 100644 index 0000000..1e5d01e Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/frame-06.png differ diff --git a/docs/assets/narrative/pipeline-overview/frame-07.png b/docs/assets/narrative/pipeline-overview/frame-07.png new file mode 100644 index 0000000..7074146 Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/frame-07.png differ diff --git a/docs/assets/narrative/pipeline-overview/home-preview.png b/docs/assets/narrative/pipeline-overview/home-preview.png new file mode 100644 index 0000000..37aa14d Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/home-preview.png differ diff --git a/docs/assets/narrative/pipeline-overview/trace.gif b/docs/assets/narrative/pipeline-overview/trace.gif new file mode 100644 index 0000000..8b1cf38 Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/trace.gif differ diff --git a/docs/assets/narrative/pipeline-overview/worked-example.png b/docs/assets/narrative/pipeline-overview/worked-example.png new file mode 100644 index 0000000..b72b33d Binary files /dev/null and b/docs/assets/narrative/pipeline-overview/worked-example.png differ diff --git a/docs/assets/narrative/presentation/contact-sheet.png b/docs/assets/narrative/presentation/contact-sheet.png new file mode 100644 index 0000000..1171ffd Binary files /dev/null and b/docs/assets/narrative/presentation/contact-sheet.png differ diff --git a/docs/assets/narrative/presentation/frame-00.png b/docs/assets/narrative/presentation/frame-00.png new file mode 100644 index 0000000..41b0ff8 Binary files /dev/null and b/docs/assets/narrative/presentation/frame-00.png differ diff --git a/docs/assets/narrative/presentation/frame-01.png b/docs/assets/narrative/presentation/frame-01.png new file mode 100644 index 0000000..60ec482 Binary files /dev/null and b/docs/assets/narrative/presentation/frame-01.png differ diff --git a/docs/assets/narrative/presentation/frame-02.png b/docs/assets/narrative/presentation/frame-02.png new file mode 100644 index 0000000..018acfb Binary files /dev/null and b/docs/assets/narrative/presentation/frame-02.png differ diff --git a/docs/assets/narrative/presentation/frame-03.png b/docs/assets/narrative/presentation/frame-03.png new file mode 100644 index 0000000..0c4bce9 Binary files /dev/null and b/docs/assets/narrative/presentation/frame-03.png differ diff --git a/docs/assets/narrative/presentation/generalized.png b/docs/assets/narrative/presentation/generalized.png new file mode 100644 index 0000000..a4ba596 Binary files /dev/null and b/docs/assets/narrative/presentation/generalized.png differ diff --git a/docs/assets/narrative/presentation/hex.png b/docs/assets/narrative/presentation/hex.png new file mode 100644 index 0000000..6a633d0 Binary files /dev/null and b/docs/assets/narrative/presentation/hex.png differ diff --git a/docs/assets/narrative/presentation/square.png b/docs/assets/narrative/presentation/square.png new file mode 100644 index 0000000..68fbe11 Binary files /dev/null and b/docs/assets/narrative/presentation/square.png differ diff --git a/docs/assets/narrative/presentation/trace.gif b/docs/assets/narrative/presentation/trace.gif new file mode 100644 index 0000000..81fc799 Binary files /dev/null and b/docs/assets/narrative/presentation/trace.gif differ diff --git a/docs/assets/narrative/reference-trace/contact-sheet.png b/docs/assets/narrative/reference-trace/contact-sheet.png new file mode 100644 index 0000000..a3251f5 Binary files /dev/null and b/docs/assets/narrative/reference-trace/contact-sheet.png differ diff --git a/docs/assets/images/solver-trace/frame-000000.png b/docs/assets/narrative/reference-trace/frame-000000.png similarity index 100% rename from docs/assets/images/solver-trace/frame-000000.png rename to docs/assets/narrative/reference-trace/frame-000000.png diff --git a/docs/assets/images/solver-trace/frame-000001.png b/docs/assets/narrative/reference-trace/frame-000001.png similarity index 100% rename from docs/assets/images/solver-trace/frame-000001.png rename to docs/assets/narrative/reference-trace/frame-000001.png diff --git a/docs/assets/narrative/reference-trace/frame-001258.png b/docs/assets/narrative/reference-trace/frame-001258.png new file mode 100644 index 0000000..01ad876 Binary files /dev/null and b/docs/assets/narrative/reference-trace/frame-001258.png differ diff --git a/docs/assets/narrative/reference-trace/frame-001887.png b/docs/assets/narrative/reference-trace/frame-001887.png new file mode 100644 index 0000000..9554447 Binary files /dev/null and b/docs/assets/narrative/reference-trace/frame-001887.png differ diff --git a/docs/assets/images/solver-trace/frame-002516.png b/docs/assets/narrative/reference-trace/frame-002516.png similarity index 100% rename from docs/assets/images/solver-trace/frame-002516.png rename to docs/assets/narrative/reference-trace/frame-002516.png diff --git a/docs/assets/images/solver-trace/frame-002517.png b/docs/assets/narrative/reference-trace/frame-002517.png similarity index 100% rename from docs/assets/images/solver-trace/frame-002517.png rename to docs/assets/narrative/reference-trace/frame-002517.png diff --git a/docs/assets/images/solver-trace/frame-002518.png b/docs/assets/narrative/reference-trace/frame-002518.png similarity index 100% rename from docs/assets/images/solver-trace/frame-002518.png rename to docs/assets/narrative/reference-trace/frame-002518.png diff --git a/docs/assets/images/solver-trace/frame-002893.png b/docs/assets/narrative/reference-trace/frame-002893.png similarity index 100% rename from docs/assets/images/solver-trace/frame-002893.png rename to docs/assets/narrative/reference-trace/frame-002893.png diff --git a/docs/assets/images/solver-trace/frame-002894.png b/docs/assets/narrative/reference-trace/frame-002894.png similarity index 100% rename from docs/assets/images/solver-trace/frame-002894.png rename to docs/assets/narrative/reference-trace/frame-002894.png diff --git a/docs/assets/images/solver-trace/frame-002895.png b/docs/assets/narrative/reference-trace/frame-002895.png similarity index 100% rename from docs/assets/images/solver-trace/frame-002895.png rename to docs/assets/narrative/reference-trace/frame-002895.png diff --git a/docs/assets/images/solver-trace/trace.gif b/docs/assets/narrative/reference-trace/trace.gif similarity index 78% rename from docs/assets/images/solver-trace/trace.gif rename to docs/assets/narrative/reference-trace/trace.gif index 16ec2f6..7a8b37b 100644 Binary files a/docs/assets/images/solver-trace/trace.gif and b/docs/assets/narrative/reference-trace/trace.gif differ diff --git a/docs/assets/images/builder-routing/contact-sheet.png b/docs/assets/narrative/region-construction/contact-sheet.png similarity index 100% rename from docs/assets/images/builder-routing/contact-sheet.png rename to docs/assets/narrative/region-construction/contact-sheet.png diff --git a/docs/assets/images/builder-routing/frame-00.png b/docs/assets/narrative/region-construction/frame-00.png similarity index 100% rename from docs/assets/images/builder-routing/frame-00.png rename to docs/assets/narrative/region-construction/frame-00.png diff --git a/docs/assets/images/builder-routing/frame-01.png b/docs/assets/narrative/region-construction/frame-01.png similarity index 100% rename from docs/assets/images/builder-routing/frame-01.png rename to docs/assets/narrative/region-construction/frame-01.png diff --git a/docs/assets/images/builder-routing/frame-02.png b/docs/assets/narrative/region-construction/frame-02.png similarity index 100% rename from docs/assets/images/builder-routing/frame-02.png rename to docs/assets/narrative/region-construction/frame-02.png diff --git a/docs/assets/images/builder-routing/frame-03.png b/docs/assets/narrative/region-construction/frame-03.png similarity index 100% rename from docs/assets/images/builder-routing/frame-03.png rename to docs/assets/narrative/region-construction/frame-03.png diff --git a/docs/assets/images/builder-routing/frame-04.png b/docs/assets/narrative/region-construction/frame-04.png similarity index 100% rename from docs/assets/images/builder-routing/frame-04.png rename to docs/assets/narrative/region-construction/frame-04.png diff --git a/docs/assets/images/builder-routing/frame-05.png b/docs/assets/narrative/region-construction/frame-05.png similarity index 100% rename from docs/assets/images/builder-routing/frame-05.png rename to docs/assets/narrative/region-construction/frame-05.png diff --git a/docs/assets/images/builder-routing/trace.gif b/docs/assets/narrative/region-construction/trace.gif similarity index 100% rename from docs/assets/images/builder-routing/trace.gif rename to docs/assets/narrative/region-construction/trace.gif diff --git a/docs/assets/narrative/verification/contact-sheet.png b/docs/assets/narrative/verification/contact-sheet.png new file mode 100644 index 0000000..e9329a6 Binary files /dev/null and b/docs/assets/narrative/verification/contact-sheet.png differ diff --git a/docs/assets/narrative/verification/frame-00.png b/docs/assets/narrative/verification/frame-00.png new file mode 100644 index 0000000..bda43b7 Binary files /dev/null and b/docs/assets/narrative/verification/frame-00.png differ diff --git a/docs/assets/narrative/verification/frame-01.png b/docs/assets/narrative/verification/frame-01.png new file mode 100644 index 0000000..2e314a0 Binary files /dev/null and b/docs/assets/narrative/verification/frame-01.png differ diff --git a/docs/assets/narrative/verification/frame-02.png b/docs/assets/narrative/verification/frame-02.png new file mode 100644 index 0000000..7e6a490 Binary files /dev/null and b/docs/assets/narrative/verification/frame-02.png differ diff --git a/docs/assets/narrative/verification/frame-03.png b/docs/assets/narrative/verification/frame-03.png new file mode 100644 index 0000000..3cb533c Binary files /dev/null and b/docs/assets/narrative/verification/frame-03.png differ diff --git a/docs/assets/narrative/verification/frame-04.png b/docs/assets/narrative/verification/frame-04.png new file mode 100644 index 0000000..18e51f8 Binary files /dev/null and b/docs/assets/narrative/verification/frame-04.png differ diff --git a/docs/assets/narrative/verification/frame-05.png b/docs/assets/narrative/verification/frame-05.png new file mode 100644 index 0000000..051b3d7 Binary files /dev/null and b/docs/assets/narrative/verification/frame-05.png differ diff --git a/docs/assets/narrative/verification/trace.gif b/docs/assets/narrative/verification/trace.gif new file mode 100644 index 0000000..89bc4ac Binary files /dev/null and b/docs/assets/narrative/verification/trace.gif differ diff --git a/docs/assets/images/z3-encoding/contact-sheet.png b/docs/assets/narrative/wang-z3/contact-sheet.png similarity index 100% rename from docs/assets/images/z3-encoding/contact-sheet.png rename to docs/assets/narrative/wang-z3/contact-sheet.png diff --git a/docs/assets/images/z3-encoding/frame-00.png b/docs/assets/narrative/wang-z3/frame-00.png similarity index 100% rename from docs/assets/images/z3-encoding/frame-00.png rename to docs/assets/narrative/wang-z3/frame-00.png diff --git a/docs/assets/images/z3-encoding/frame-01.png b/docs/assets/narrative/wang-z3/frame-01.png similarity index 100% rename from docs/assets/images/z3-encoding/frame-01.png rename to docs/assets/narrative/wang-z3/frame-01.png diff --git a/docs/assets/images/z3-encoding/frame-02.png b/docs/assets/narrative/wang-z3/frame-02.png similarity index 100% rename from docs/assets/images/z3-encoding/frame-02.png rename to docs/assets/narrative/wang-z3/frame-02.png diff --git a/docs/assets/images/z3-encoding/frame-03.png b/docs/assets/narrative/wang-z3/frame-03.png similarity index 100% rename from docs/assets/images/z3-encoding/frame-03.png rename to docs/assets/narrative/wang-z3/frame-03.png diff --git a/docs/assets/images/z3-encoding/frame-04.png b/docs/assets/narrative/wang-z3/frame-04.png similarity index 100% rename from docs/assets/images/z3-encoding/frame-04.png rename to docs/assets/narrative/wang-z3/frame-04.png diff --git a/docs/assets/images/z3-encoding/trace.gif b/docs/assets/narrative/wang-z3/trace.gif similarity index 100% rename from docs/assets/images/z3-encoding/trace.gif rename to docs/assets/narrative/wang-z3/trace.gif diff --git a/docs/components/boolean-z3.md b/docs/components/boolean-z3.md new file mode 100644 index 0000000..2940ca1 --- /dev/null +++ b/docs/components/boolean-z3.md @@ -0,0 +1,69 @@ +--- +layout: story +title: Boolean Z3 oracle +permalink: /components/boolean-z3/ +page_class: story +component_id: boolean-z3 +pipeline_order: 2 +primary_asset: boolean_z3 +owned_assets: boolean_z3 +description: The independent source-formula oracle and its project-owned constraint construction order. +--- + +# Boolean Z3 oracle + +## What it is + +Boolean Z3 is an independent oracle for the canonical Cubic Monotone 1-in-3 +SAT formula. It decides the source model directly and returns an assignment +when the result is SAT. + +## Why it exists + +The oracle supplies a decision path that does not depend on the Yang–Zhang +builder, Wang region, native solver, or renderer. Agreement across that boundary +is stronger evidence than asking one implementation to check itself. + +## Inputs and outputs + +Input is the immutable canonical formula. Output preserves SAT, UNSAT, or +UNKNOWN and, for SAT, a Boolean assignment copied from the model. A closed +`z3-encoding-summary-v1` document records source identity, project-owned +assertion order, counters, status, and optional assignment. + +## Mechanism + +The adapter creates one Boolean variable per source variable and adds exactly +one constraint for each three-variable clause in source order. Its fixed Z3 +configuration uses one thread and a fixed random seed. + +## Primary animation + +`boolean_z3` shows only project-owned encoding order and the returned result. + +{% include narrative-animation.html asset_id="boolean_z3" animation="/assets/narrative/boolean-z3/trace.gif" fallback="/assets/narrative/boolean-z3/frame-02.png" contact_sheet="/assets/narrative/boolean-z3/contact-sheet.png" alt="Four frames add Boolean variables and source-order exactly-one clauses before showing the copied result." width="940" height="430" label="encoding-order" caption="Project-owned Boolean constraint construction and returned assignment." source="z3-encoding-summary-v1" %} + +## Position in the pipeline + +This branch starts at the source formula and meets the Wang decision paths only +at the agreement boundary. It is an independent cross-check, not a predecessor +that supplies domains or hints to the native solvers. + +## Observed example + +For `pipeline_sat.cm13`, Boolean Z3 returns SAT and the independent assignment +checker accepts the copied assignment. The asset is bound to the same formula +hash shown on the [worked example]({{ '/worked-example/' | relative_url }}). + +## Trust boundary + +The summary establishes which constraints the project asked Z3 to construct +and what result was copied back. It does not expose or stabilize Z3's internal +branching, propagation, proof, or debug trace. + +## Artifacts and references + +The implementation is in `python/oracles/boolean_solver.py`; encoding summaries +are defined by `schemas/z3-encoding-summary-v1.schema.json`. See the +[comparison protocol]({{ '/solver_comparison_benchmark/' | relative_url }}) and +[verification component]({{ '/components/verification/' | relative_url }}). diff --git a/docs/components/optimized-solver.md b/docs/components/optimized-solver.md new file mode 100644 index 0000000..0e0c2e8 --- /dev/null +++ b/docs/components/optimized-solver.md @@ -0,0 +1,75 @@ +--- +layout: story +title: Optimized native solver +permalink: /components/optimized-solver/ +page_class: story +component_id: optimized-solver +pipeline_order: 5 +primary_asset: optimized_trace +owned_assets: optimized_trace, optimized_mechanisms +description: The semantically equivalent serial path, its observed trace, and six separately measured private mechanisms. +--- + +# Optimized native solver + +## What it is + +The optimized solver is a second public native entry point over the same Wang +search core. It selects six private serial mechanisms while retaining the +reference path's inputs, outputs, search meaning, and mandatory verification. + +## Why it exists + +Performance work needs isolated mechanisms, direct counters, and a stable +baseline. Keeping this path beside the reference solver makes equivalence and +regressions testable without turning measured choices into universal claims. + +## Inputs and outputs + +The input and public result contracts match the reference path: immutable +region and tileset, optional initial domains, SAT with caller-owned witness, +UNSAT, or ERROR. Optional metrics count direct work and storage; optional trace +records the actual optimized invocation. + +## Mechanism + +The retained mechanisms are a geometrically growing DFS stack, omission of +non-consumable initial trail entries, transfer of verified SAT domains, +byte-wise support tables, queue deduplication, and a private lazy MRV index. +Each has separate evidence and preserves row-major tie breaking. + +## Primary animation + +`optimized_trace` is the primary observed asset. `optimized_mechanisms` is a +secondary didactic overview; it makes no timing or speedup claim. + +{% include narrative-animation.html asset_id="optimized_trace" animation="/assets/narrative/optimized-trace/trace.gif" fallback="/assets/narrative/optimized-trace/frame-002562.png" contact_sheet="/assets/narrative/optimized-trace/contact-sheet.png" alt="Observed optimized domain states at root, propagation, decision, search, and result milestones." width="988" height="414" label="observed" caption="Selected semantic milestones from the complete optimized trace." source="wang-explain-manifest-v3" %} + +{% include narrative-animation.html asset_id="optimized_mechanisms" animation="/assets/narrative/optimized-mechanisms/trace.gif" fallback="/assets/narrative/optimized-mechanisms/frame-06.png" contact_sheet="/assets/narrative/optimized-mechanisms/contact-sheet.png" alt="Seven didactic frames contrast the reference baseline with six measured optimized mechanisms." width="960" height="500" label="didactic" caption="The six retained serial mechanisms, including the lazy MRV index." source="wang-optimized-mechanisms-v1" %} + +## Position in the pipeline + +This is an independent invocation on the same reduction consumed by the +reference solver and Wang Z3. Its result joins them at agreement and +verification; neither trace nor metrics are used as solver input. + +## Observed example + +The `pipeline_sat.cm13` optimized run returns a checked SAT witness with a +complete trace. The separately named search-UNSAT capture in the +[dossier index]({{ '/run-dossiers/' | relative_url }}) exercises conflict, +backtrack, and exhaustion without becoming a second canonical story. + +## Trust boundary + +Correctness comes from status equivalence, checked witnesses, differential +tests, and the independent verifier. The observed trace describes one run; +the didactic mechanism asset does not establish performance. Dated reports +remain scoped to their corpus and environment. + +## Artifacts and references + +Start with the [optimization methodology]({{ '/solver_performance_scope/' | relative_url }}) +and [serial solver reference]({{ '/serial_solver_implementation_guide/' | relative_url }}). +The six accepted reports are collected in the +[evidence index]({{ '/evidence/' | relative_url }}). diff --git a/docs/components/reference-solver.md b/docs/components/reference-solver.md new file mode 100644 index 0000000..3be6d99 --- /dev/null +++ b/docs/components/reference-solver.md @@ -0,0 +1,71 @@ +--- +layout: story +title: Reference native solver +permalink: /components/reference-solver/ +page_class: story +component_id: reference-solver +pipeline_order: 4 +primary_asset: reference_trace +owned_assets: reference_trace +description: The executable native baseline, its observed semantic trace, result ownership, and verification boundary. +--- + +# Reference native solver + +## What it is + +The reference solver is the deliberately direct native baseline for finite +Wang regions. It remains executable beside the optimized entry point and uses +the same public status and ownership contracts. + +## Why it exists + +A readable baseline keeps correctness and performance changes comparable. +Optimizations must match this path on the full corpus rather than replace the +only executable statement of the search semantics. + +## Inputs and outputs + +Input is an immutable `Region`, a tileset, and optional initial domains. Output +is SAT with a caller-owned dense witness, UNSAT, or ERROR. Optional metrics and +bounded traces are separate caller-owned results; ordinary calls allocate no +trace state. + +## Mechanism + +The solver applies boundary restrictions and local arc propagation, chooses the +next non-singleton cell by row-major minimum remaining values, and explores +choices with iterative depth-first search and an undo trail. Every SAT result +is checked before publication. + +## Primary animation + +`reference_trace` selects semantic milestones from one complete observed trace. +Unshown visual frames do not mean skipped solver events. + +{% include narrative-animation.html asset_id="reference_trace" animation="/assets/narrative/reference-trace/trace.gif" fallback="/assets/narrative/reference-trace/frame-002517.png" contact_sheet="/assets/narrative/reference-trace/contact-sheet.png" alt="Observed reference domain states at root, propagation, decision, search, and result milestones." width="988" height="414" label="observed" caption="Selected semantic milestones from the complete reference trace." source="wang-explain-manifest-v3" %} + +## Position in the pipeline + +This solver consumes the native reduction. Its result is compared with the +optimized invocation and Wang Z3, then passed to independent witness checks. +The trace is downstream evidence and never feeds search. + +## Observed example + +The `pipeline_sat.cm13` reference run reaches SAT with a complete trace and a +checked tiling. A separately identified search-UNSAT run is available through +the [dossier index]({{ '/run-dossiers/' | relative_url }}); it is not part of +the SAT story. + +## Trust boundary + +The solver establishes only its returned decision under its inputs. A trace is +diagnostic, not an UNSAT certificate. The independent verifier, not the trace +renderer, accepts a SAT tiling. + +## Artifacts and references + +See the [serial solver reference]({{ '/serial_solver_implementation_guide/' | relative_url }}), +[trace contract]({{ '/wang-solver-trace/' | relative_url }}), and +[reference profile]({{ '/solver_reference_profile_2026-08-17/' | relative_url }}). diff --git a/docs/components/tileset.md b/docs/components/tileset.md new file mode 100644 index 0000000..00959b2 --- /dev/null +++ b/docs/components/tileset.md @@ -0,0 +1,76 @@ +--- +layout: story +title: Tile vocabulary +permalink: /components/tileset/ +page_class: story +component_id: tileset +pipeline_order: 1 +primary_asset: generalized_sheet +owned_assets: generalized_sheet, atomic_legend +description: The fixed 23 atomic Wang tiles, exact 14 generalized tiles, edge colors, matching rule, and stable identifiers. +--- + +# Tile vocabulary + +## What it is + +The project uses one fixed table of 23 positional Wang tiles. Fourteen named +generalized tiles describe exact rectangular groupings of those atomic IDs for +explaining the Yang–Zhang construction. + +## Why it exists + +Solvers need a small, immutable vocabulary with unambiguous edge colors and +identifiers. The generalized view helps people recognize gadgets, but it does +not create a second tileset or change the atomic domain seen by a solver. + +## Inputs and outputs + +The atomic input is the compiled `TILESET`; its snapshot contract records IDs +and `(N,E,S,W)` colors. The generalized specification maps each of 14 shapes to +an exact arrangement of those 23 IDs. It outputs presentation metadata only, +with no SAT, UNSAT, or UNKNOWN status. + +## Mechanism + +Two neighboring square tiles match when their touching edge colors are equal. +Rotation and reflection are not allowed. The generalized recognizer checks the +entire atomic pattern before drawing a contour, so a partial resemblance is +never promoted to a generalized occurrence. + +## Primary animation + +`generalized_sheet` is deliberately static: a tile vocabulary has no execution +timeline to animate. The canonical sheet is the primary reduced-motion-safe +asset, followed by its atomic legend. + +{% include narrative-static.html asset_id="generalized_sheet" image="/assets/narrative/generalized-tiles/sheet.png" alt="A sheet of fourteen Yang-Zhang generalized tiles with internal seams and atomic identifiers." width="908" height="1146" label="canonical-construction" caption="The exact 14 generalized tiles decomposed into 23 positional atomic IDs." source="wang-generalized-tiles-v1+wang-tileset-snapshot-v1" %} + +{% include narrative-static.html asset_id="atomic_legend" image="/assets/narrative/generalized-tiles/atomic-legend.png" alt="A semantic legend for twenty-three positional Wang tiles and their edge colors." width="1296" height="782" label="canonical-construction" caption="All 23 atomic IDs with symbolic paper colors and generalized roles." source="wang-generalized-tiles-v1+wang-tileset-snapshot-v1" %} + +## Position in the pipeline + +The vocabulary is an immutable input to region construction and all three Wang +decision paths. Generalized labels flow only to explanation and visualization; +they are not semantic solver input. + +## Observed example + +The named `pipeline_sat.cm13` capture binds the same tileset identity into the +region, both native trace manifests, Wang Z3 summary, solution, and rendered +views. The displayed sheet is canonical construction data, not an observed +solver trace. + +## Trust boundary + +The tile table and matching rule define local compatibility. They do not prove +that a region is tileable, that a reduction is correct, or that a rendered +witness is valid. Those claims belong to construction tests, solvers, and the +independent verifier. + +## Artifacts and references + +See the [static snapshot contract]({{ '/wang-explainability-snapshots/' | relative_url }}), +the [reduction note]({{ '/reduction_notes/' | relative_url }}), and the +[Yang–Zhang builder contract]({{ '/yang_zhang_builder_design/' | relative_url }}). +The public C table is defined in `include/wang/tile.h` and `src/core/tile.c`. diff --git a/docs/components/verification.md b/docs/components/verification.md new file mode 100644 index 0000000..47fad6d --- /dev/null +++ b/docs/components/verification.md @@ -0,0 +1,71 @@ +--- +layout: story +title: Independent verification +permalink: /components/verification/ +page_class: story +component_id: verification +pipeline_order: 7 +primary_asset: verification +owned_assets: verification +description: Named assignment and tiling checks, witness correspondence, and the exact claims those checks establish. +--- + +# Independent verification + +## What it is + +Verification is a set of pure, named checks over returned assignments and +tilings. It is separate from solver success paths and from every renderer. + +## Why it exists + +A solver's SAT status is not enough to publish a witness. Independent checks +re-evaluate the source clauses, tile compatibility, exposed boundary colors, +and Boolean–Wang correspondence without trusting internal solver state. + +## Inputs and outputs + +Inputs are the canonical formula, shared region and tileset, returned Boolean +assignment or Wang tiling, and the reduction provenance needed by the witness +bridge. Each receipt records checker name, whether it ran, pass/fail, and the +witness identity. Witness-only checks are not applicable for UNSAT. + +## Mechanism + +The Boolean checker requires exactly one true variable in every source clause. +The tiling checker validates every active cell, internal edge, inactive cell, +and exposed boundary. Native witnesses also pass through the independent +assignment extraction bridge before their assignments are checked. + +## Primary animation + +`verification` presents the six receipts already captured from the named +checkers. It does not rerun or replace them. + +{% include narrative-animation.html asset_id="verification" animation="/assets/narrative/verification/trace.gif" fallback="/assets/narrative/verification/frame-05.png" contact_sheet="/assets/narrative/verification/contact-sheet.png" alt="Six frames report Boolean, native, and Wang Z3 witness checks without rerunning a verifier." width="960" height="500" label="observed" caption="The six named independent checker records from the captured run." source="wang-run-dossier-v2#verification" %} + +## Position in the pipeline + +Verification follows all four decision results and precedes witness +presentation. It receives semantic artifacts, not PNGs. A failed check aborts +the captured pipeline instead of being presented as an alternate outcome. + +## Observed example + +The `pipeline_sat.cm13` capture records passing checks for the Boolean Z3 +assignment, reference tiling and extracted assignment, optimized tiling and +extracted assignment, and Wang Z3 tiling. + +## Trust boundary + +Passing receipts establish validity of the named SAT witnesses under their +inputs. They do not prove that every implementation is bug-free, turn an UNSAT +trace into a certificate, or make a raster authoritative. + +## Artifacts and references + +Read the [witness correspondence]({{ '/witness_correspondence/' | relative_url }}), +[solution contract]({{ '/wang-solution-v1/' | relative_url }}), and +[serial solver reference]({{ '/serial_solver_implementation_guide/' | relative_url }}). +The pure Python checkers live in `python/oracles/witness_check.py` and +`python/oracles/tiling_check.py`. diff --git a/docs/components/visualization.md b/docs/components/visualization.md new file mode 100644 index 0000000..e2dd34b --- /dev/null +++ b/docs/components/visualization.md @@ -0,0 +1,76 @@ +--- +layout: story +title: Verified visualization +permalink: /components/visualization/ +page_class: story +component_id: visualization +pipeline_order: 8 +primary_asset: witness_presentation +owned_assets: witness_presentation, square_presentation, generalized_presentation, hex_presentation +description: Square witness rendering, exact generalized overlays, and the checked presentation-only square-to-hex transformation. +--- + +# Verified visualization + +## What it is + +Visualization is the removable downstream layer that renders a verified square +Wang witness, recognizes exact generalized shapes, and produces a checked +pointy-top hex presentation. + +## Why it exists + +Dense solution arrays are precise but difficult to inspect. These views expose +tile IDs, boundaries, generalized gadget structure, and the square-to-hex +correspondence without moving correctness into pixels. + +## Inputs and outputs + +Input is a validated `wang-solution-v1` square witness and the canonical +generalized specification. Outputs are raster presentations only. The hex view +has a raster-independent inverse check and remains a one-to-one transformation +of the square witness, never a separate solution schema. + +## Mechanism + +The square renderer draws the stored active cells and edges. Generalized +recognition accepts only exact atomic patterns. The hex port maps `(x,y)` to +pointy-top axial `(q,r)`, preserves the four source edges, and assigns one fresh +color to the two additional axes. + +## Primary animation + +`witness_presentation` moves from the verified square witness through exact +generalized recognition to the checked hex port. + +{% include narrative-animation.html asset_id="witness_presentation" animation="/assets/narrative/presentation/trace.gif" fallback="/assets/narrative/presentation/frame-03.png" contact_sheet="/assets/narrative/presentation/contact-sheet.png" alt="Four frames move from the verified square witness through generalized recognition to the checked hex presentation." width="1080" height="620" label="verified-transformation" caption="Verified square witness, exact generalized overlay, and checked hex port." source="wang-solution-v1+wang-generalized-tiles-v1+checked-square-to-hex" %} + +## Position in the pipeline + +Presentation follows independent SAT verification. No rendered output is fed +back to a solver, oracle, reduction, or checker. Removing this layer leaves +all semantic decisions and witness validation intact. + +## Observed example + +All three views below derive from the same checked `pipeline_sat.cm13` square +witness. + +{% include narrative-static.html asset_id="square_presentation" image="/assets/narrative/presentation/square.png" alt="The complete square Wang witness for the captured SAT source." width="1538" height="422" label="observed" caption="The independently verified square witness with atomic IDs and boundaries." source="wang-solution-v1" %} + +{% include narrative-static.html asset_id="generalized_presentation" image="/assets/narrative/presentation/generalized.png" alt="The square witness grouped into exact Yang-Zhang generalized tile occurrences." width="1616" height="430" label="canonical-construction" caption="Exact generalized contours over the same verified square witness." source="wang-solution-v1+wang-generalized-tiles-v1" %} + +{% include narrative-static.html asset_id="hex_presentation" image="/assets/narrative/presentation/hex.png" alt="A pointy-top hex presentation preserving the square witness cells, edges, and boundary." width="3171" height="615" label="verified-transformation" caption="The checked Basire/Culik square-to-hex port of the same witness." source="wang-solution-v1+checked-square-to-hex" %} + +## Trust boundary + +The square witness contract and independent tiling verifier establish SAT +witness validity. The generalized recognizer and square-to-hex checker establish +their transformation relationships. None of the PNG or GIF files is itself a +proof or an independent solver result. + +## Artifacts and references + +See the [snapshot views]({{ '/wang-explainability-snapshots/' | relative_url }}), +[square solution contract]({{ '/wang-solution-v1/' | relative_url }}), and +[square-to-hex reference]({{ '/wang-square-to-hex/' | relative_url }}). diff --git a/docs/components/wang-z3.md b/docs/components/wang-z3.md new file mode 100644 index 0000000..13d3d78 --- /dev/null +++ b/docs/components/wang-z3.md @@ -0,0 +1,69 @@ +--- +layout: story +title: Wang Z3 oracle +permalink: /components/wang-z3/ +page_class: story +component_id: wang-z3 +pipeline_order: 6 +primary_asset: wang_z3 +owned_assets: wang_z3 +description: The independent finite-region oracle and its project-owned edge-term construction order. +--- + +# Wang Z3 oracle + +## What it is + +Wang Z3 is an independent Python oracle for a finite `Region` and immutable +tileset. It returns a dense row-major tiling model when the region is SAT. + +## Why it exists + +This oracle checks the native decision paths with a different implementation +and constraint engine. It neither parses the source formula nor rebuilds the +Yang–Zhang reduction, so the shared region identity is an explicit boundary. + +## Inputs and outputs + +Input is the hash-bound region and tileset produced once by the native +construction. Output preserves SAT, UNSAT, or UNKNOWN and an optional dense +model. `z3-encoding-summary-v1` records project-owned term and assertion order, +counts, identity, status, and copied model. + +## Mechanism + +The model creates `(N,E,S,W)` edge-color terms in row-major order, shares terms +across active internal adjacencies, restricts each cell to a canonical tile +tuple, and applies exposed boundary colors. Its fixed configuration uses one +thread and a fixed random seed. + +## Primary animation + +`wang_z3` shows the project's edge-term construction and returned result, not +the solver engine's internal search. + +{% include narrative-animation.html asset_id="wang_z3" animation="/assets/narrative/wang-z3/trace.gif" fallback="/assets/narrative/wang-z3/frame-03.png" contact_sheet="/assets/narrative/wang-z3/contact-sheet.png" alt="Five frames add edge terms, shared internal edges, tile relations, boundaries, and the copied result." width="940" height="430" label="encoding-order" caption="Project-owned Wang edge-term construction and returned model." source="z3-encoding-summary-v1" %} + +## Position in the pipeline + +Wang Z3 consumes the same constructed region as both native solvers and joins +them at agreement. It is an independent cross-check, not a fallback or a +producer of hints for either native path. + +## Observed example + +For `pipeline_sat.cm13`, the oracle returns SAT over the same region and tile +identities as the native runs, and its dense model passes the pure Python +tiling checker. + +## Trust boundary + +The summary stabilizes project construction order and the copied result only. +It does not claim to expose Z3 branching, propagation, proof search, or debug +events. A rendered frame is not the tiling checker. + +## Artifacts and references + +See the [Wang Z3 model reference]({{ '/wang_z3_edge_table_2026-08-24/' | relative_url }}), +[comparison protocol]({{ '/solver_comparison_benchmark/' | relative_url }}), +and `python/oracles/tiling_solver.py`. diff --git a/docs/components/yang-zhang.md b/docs/components/yang-zhang.md new file mode 100644 index 0000000..b4dc89d --- /dev/null +++ b/docs/components/yang-zhang.md @@ -0,0 +1,71 @@ +--- +layout: story +title: Yang–Zhang construction +permalink: /components/yang-zhang/ +page_class: story +component_id: yang-zhang +pipeline_order: 3 +primary_asset: region_construction +owned_assets: region_construction +description: The formula-to-region reduction, generalized routing vocabulary, and native construction provenance. +--- + +# Yang–Zhang construction + +## What it is + +The native Yang–Zhang builder transforms a validated Cubic Monotone 1-in-3 SAT +formula into one finite simply connected region over the fixed 23 Wang tiles. + +## Why it exists + +This component owns the semantic bridge from Boolean clauses to boundary-colored +geometry. Solvers remain generic consumers of a `Region`; they do not know +about variables, clauses, gadgets, or the reduction theorem. + +## Inputs and outputs + +Input is a canonical formula. Output is a caller-owned reduction containing +the region, adjacent-swap trace, and optional immutable provenance. Snapshot +and explanation contracts bind formula, tileset, region, signal, permutation, +and gadget-span identities. + +## Mechanism + +Variable signals are routed in source order through forwarders and adjacent +crossovers into clause gadgets. The implementation decomposes generalized +tiles into the fixed atomic IDs and constructs the complete exposed boundary +transactionally. + +## Primary animation + +`region_construction` is a deterministic construction view, not an instrumented +clock or solver trace. + +{% include narrative-animation.html asset_id="region_construction" animation="/assets/narrative/region-construction/trace.gif" fallback="/assets/narrative/region-construction/frame-04.png" contact_sheet="/assets/narrative/region-construction/contact-sheet.png" alt="Six frames reveal variable, forwarding, crossover, and clause gadget spans on the same region." width="980" height="390" label="canonical-construction" caption="Native Yang-Zhang gadget spans accumulated over the observed region." source="wang-reduction-explanation-v1" %} + +## Position in the pipeline + +The builder follows parsing and supplies the shared region to the reference +solver, optimized solver, and Wang Z3 oracle. Boolean Z3 remains a parallel +source-level cross-check; rendering is a removable downstream consumer. + +## Observed example + +For `pipeline_sat.cm13`, the capture builds the reduction once and shares its +hash-bound formula, tileset, region, and provenance across both native runs and +the Wang oracle. + +## Trust boundary + +Provenance explains what the native builder constructed. It is not a second +reduction and does not by itself prove satisfiability. Black-box reduction +tests, Boolean agreement, witness correspondence, and independent tiling +verification establish separate obligations. + +## Artifacts and references + +Read the [reduction note]({{ '/reduction_notes/' | relative_url }}), +[builder contract]({{ '/yang_zhang_builder_design/' | relative_url }}), and +[provenance contract]({{ '/wang-reduction-explanation/' | relative_url }}). +Public ownership begins in `include/wang/yang_zhang.h`. diff --git a/docs/coverage_baseline_2026-08-22.md b/docs/coverage_baseline_2026-08-22.md index 7faf5d2..d8b2552 100644 --- a/docs/coverage_baseline_2026-08-22.md +++ b/docs/coverage_baseline_2026-08-22.md @@ -2,6 +2,7 @@ layout: page title: C and Python coverage baseline permalink: /coverage_baseline_2026-08-22/ +page_class: evidence description: Informational line, function, and branch coverage from the complete local test suites. section: Architecture and correctness document_kind: Coverage report diff --git a/docs/designs/2026-08-21-witness-extension-design.md b/docs/designs/2026-08-21-witness-extension-design.md index df4fb9f..d37d86b 100644 --- a/docs/designs/2026-08-21-witness-extension-design.md +++ b/docs/designs/2026-08-21-witness-extension-design.md @@ -2,6 +2,7 @@ layout: page title: Boolean–Wang witness correspondence permalink: /witness_correspondence/ +page_class: reference description: How exact Boolean assignments are extended to Wang tilings and extracted again without coupling the generic solver to reduction semantics. section: Architecture and correctness document_kind: Technical design diff --git a/docs/development_principles.md b/docs/development_principles.md index ada185e..43e7a42 100644 --- a/docs/development_principles.md +++ b/docs/development_principles.md @@ -2,6 +2,7 @@ layout: page title: Development principles and architecture boundaries permalink: /development_principles/ +page_class: reference description: How Tiling Foundry separates source data, derived state, native lifetimes, solvers, and independent verification. section: Architecture and correctness document_kind: Architecture reference diff --git a/docs/evidence.md b/docs/evidence.md new file mode 100644 index 0000000..cbe8159 --- /dev/null +++ b/docs/evidence.md @@ -0,0 +1,16 @@ +--- +layout: story +title: Evidence +permalink: /evidence/ +page_class: story +description: Dated, source-bound benchmark, profile, coverage, and fuzz reports with their interpretation limits. +--- + +# Evidence + +Every item below is tied to a named source state, corpus, environment, or test +budget. Read its method and limitations before carrying an observation to a +different machine or workload. + +{% assign evidence = site.pages | where: "page_class", "evidence" | sort: "title" %} +{% include document-list.html documents=evidence %} diff --git a/docs/historical_architecture.md b/docs/historical_architecture.md index 897f42a..75ee7e3 100644 --- a/docs/historical_architecture.md +++ b/docs/historical_architecture.md @@ -2,6 +2,7 @@ layout: page title: Initial C/OpenMP architecture specification permalink: /historical_architecture/ +page_class: history description: Context and limitations for the project's original future-facing architecture PDF. section: Historical material document_kind: Historical specification diff --git a/docs/index.md b/docs/index.md index 5747d20..7a39a02 100644 --- a/docs/index.md +++ b/docs/index.md @@ -1,173 +1,76 @@ --- layout: default title: Tiling Foundry +permalink: / page_kind: home +page_class: story +owned_assets: home_preview description: A research software laboratory for finite Wang tilings and inspectable solver design. ---
-

Finite tilings / algorithm laboratory

+

Finite tilings / inspectable decisions

Tiling Foundry

- Tiling Foundry turns the Yang–Zhang reduction into an inspectable software - pipeline. Construction, solving, verification, witness correspondence, and - measurement remain separate so that each result can be audited rather than - merely observed. + Follow one Cubic Monotone 1-in-3 SAT instance through independent Boolean + and Wang models, the Yang–Zhang construction, two native solver paths, + explicit verification, and presentation-only views.

- Explore the documentation -
- -
-
-

Reading path

-

Understand, inspect, verify

-
- -
-

- Start with the architecture reference and reduction note to understand the - pipeline. Use implementation contracts and the data contract when inspecting - code or integrations. Use methodology pages before interpreting dated - benchmark, profile, coverage, or fuzzing reports. -

- -

- Each catalog entry shows both its document type and status. Current - specifications, contracts, references, notes, and designs describe maintained - behavior within their stated scope. Methodology pages define how evidence is - collected. Dated reports preserve results for a named source state and date. - Historical pages preserve earlier decisions and are not current API - documentation. -

- -

- Completed implementation plans remain versioned under docs/plans/ - for operational history, but are excluded from this public catalog. -

+
+ Explore the pipeline + Inspect the worked example
-{% comment %} -Author-approved narrative can be inserted as layout-reading sections. The wide -components below emit no markup until their complete front-matter data exists. -{% endcomment %} -{% if page.pipeline %} - {% include home-pipeline.html pipeline=page.pipeline %} -{% endif %} -{% if page.featured_output %} - {% include home-output.html output=page.featured_output %} -{% endif %} -{% if page.evidence %} - {% include home-evidence.html evidence=page.evidence %} -{% endif %} -{% if page.implementation_status %} - {% include home-status.html status=page.implementation_status %} -{% endif %} - -{% assign architecture = site.pages - | where: "section", "Architecture and correctness" - | sort: "nav_order" %} -{% assign reduction = site.pages | where: "section", "Yang–Zhang reduction" | sort: "nav_order" %} -{% assign optimization = site.pages | where: "section", "Solver optimization" | sort: "nav_order" %} -{% assign comparisons = site.pages - | where: "section", "Cross-engine benchmarks" - | sort: "nav_order" %} -{% assign historical = site.pages | where: "section", "Historical material" | sort: "nav_order" %} - -
+
-

Start here

-

Architecture and correctness

+

Project map

+

One construction, several independent checks

-

- These current references define the software boundaries that keep the - reduction, solver, independent verification, solution transport, and - Boolean–Wang witness correspondence auditable. -

- - {% include document-list.html documents=architecture %} +
    +
  1. The fixed tile vocabulary supplies one immutable domain.
    2. +
  2. Boolean Z3 checks the source formula.
    3. +
  3. Yang–Zhang constructs one finite Wang region.
    4. +
  4. Reference and optimized native paths solve the same region.
    5. +
  5. Wang Z3 provides a separate finite-region oracle.
    6. +
  6. Independent checkers validate returned witnesses.
    7. +
  7. Visualization follows verification and changes no decision.
    8. +
-
+
-

Construction

-

Yang–Zhang reduction

+

Verified output

+

A selected result, not a visual proof

-

- The technical note distinguishes paper conventions from project conventions. - The builder page is the implementation contract for region geometry, - ownership, and black-box obligations. The bibliography records primary - sources. -

- - {% include document-list.html documents=reduction %} -
- -
-
-

Measured mechanisms

-

Solver optimization

-
- -

- Read the methodology first. The remaining pages are dated profile or - benchmark reports that preserve their corpus, environment, work counters, - timing method, and limitations. -

- - {% include document-list.html documents=optimization %} -
- -
-
-

Native C / Z3

-

Cross-engine benchmarks

-
+ {% include narrative-static.html asset_id="home_preview" image="/assets/narrative/pipeline-overview/home-preview.png" alt="A compact square Wang witness preview for the captured SAT source." width="760" height="430" label="observed" caption="Selected verified SAT square output for the captured instance." source="wang-solution-v1" %}

- The current protocol distinguishes solving the same prepared Wang region - from end-to-end decisions that begin with the same formula file. Dated - reports retain the measured source identity and interpretation limits. + The image is downstream of an independently checked square witness. Read + the named example for + its source identity and the + visualization component + for the transformation boundary.

- - {% include document-list.html documents=comparisons %}
-
+
-

Design history

-

Historical material

+

Reading path

+

Story, contracts, evidence

- Earlier proposals are retained to explain the project’s design trajectory. - They are not current API contracts. + Use the pipeline story to + understand responsibilities, the reference index + for maintained contracts and history, and the + evidence index for dated, + source-bound measurements. Reproducible captures remain separately indexed + under run dossiers.

- - {% include document-list.html documents=historical %}
diff --git a/docs/parser_fuzz_smoke_2026-08-22.md b/docs/parser_fuzz_smoke_2026-08-22.md index 0a2f8b0..2f9062c 100644 --- a/docs/parser_fuzz_smoke_2026-08-22.md +++ b/docs/parser_fuzz_smoke_2026-08-22.md @@ -2,6 +2,7 @@ layout: page title: CM13 parser fuzz smoke permalink: /parser_fuzz_smoke_2026-08-22/ +page_class: evidence description: Reproducible libFuzzer smoke coverage for the canonical CM13 parser. section: Architecture and correctness document_kind: Test report diff --git a/docs/pipeline.md b/docs/pipeline.md new file mode 100644 index 0000000..e5de333 --- /dev/null +++ b/docs/pipeline.md @@ -0,0 +1,57 @@ +--- +layout: story +title: The complete pipeline +permalink: /pipeline/ +page_class: story +owned_assets: pipeline_overview +description: Component order, data flow, independence, and trust boundaries from a CM1-in-3 formula to checked Wang presentations. +--- + +# The complete pipeline + +Tiling Foundry keeps construction, decision, verification, and presentation as +separate responsibilities. A result is useful only when its source identity, +component boundary, and independent checks remain visible. + +{% include narrative-animation.html asset_id="pipeline_overview" animation="/assets/narrative/pipeline-overview/trace.gif" fallback="/assets/narrative/pipeline-overview/frame-07.png" contact_sheet="/assets/narrative/pipeline-overview/contact-sheet.png" alt="The captured formula moves through Boolean Z3, Yang-Zhang reduction, both native solvers, Wang Z3, verification, and presentation." width="1080" height="620" label="observed" caption="One validated v2 capture in fixed component order." source="wang-run-dossier-v2#named-components" %} + +## Data flow + +The source formula enters two deliberately different paths. The +[Boolean Z3 component]({{ '/components/boolean-z3/' | relative_url }}) decides +the formula directly. Independently, the +[Yang–Zhang component]({{ '/components/yang-zhang/' | relative_url }}) constructs +a finite region over the fixed [tile vocabulary]({{ '/components/tileset/' | relative_url }}). +The reference solver, optimized solver, and Wang Z3 oracle consume that same +hash-bound region and tileset. + +| Step | Input | Output | Relationship | +| --- | --- | --- | --- | +| Boolean Z3 | canonical formula | status and optional assignment | independent source-level decision | +| Yang–Zhang | canonical formula | region, tileset, provenance | semantic construction | +| [Reference solver]({{ '/components/reference-solver/' | relative_url }}) | region and tileset | status and optional tiling | executable baseline | +| [Optimized solver]({{ '/components/optimized-solver/' | relative_url }}) | same region and tileset | status and optional tiling | independent invocation of the shared native core | +| [Wang Z3]({{ '/components/wang-z3/' | relative_url }}) | same region and tileset | status and optional model | independent finite-region oracle | +| [Verification]({{ '/components/verification/' | relative_url }}) | returned witnesses and original inputs | named checker receipts | independent cross-check | +| [Visualization]({{ '/components/visualization/' | relative_url }}) | verified square witness | square, generalized, and checked hex views | presentation-only | + +## Independence + +The reference path remains executable and understandable. The optimized path +retains the same public semantics while selecting six measured private +mechanisms. Boolean Z3 does not call the reduction, and Wang Z3 does not call a +native solver. Independent checkers consume returned assignments or tilings; +they do not trust a raster. + +## Trust boundaries + +- `SAT` is accepted only with the applicable witness checks. +- `UNSAT` from a solver is a terminal observation, not a standalone certificate. +- `UNKNOWN` is preserved where an oracle can return it; it is never rewritten as UNSAT. +- Trace replay presents recorded semantic events but does not solve again. +- Generalized and hex views are downstream transformations, not new solvers. + +The [worked example]({{ '/worked-example/' | relative_url }}) follows one named +SAT source through these boundaries. Maintained APIs and methods remain in the +[reference index]({{ '/reference/' | relative_url }}); measurements and dated +observations remain in [evidence]({{ '/evidence/' | relative_url }}). diff --git a/docs/plans/2026-08-31-narrative-migration-checklist.md b/docs/plans/2026-08-31-narrative-migration-checklist.md index c5374cb..7510e5c 100644 --- a/docs/plans/2026-08-31-narrative-migration-checklist.md +++ b/docs/plans/2026-08-31-narrative-migration-checklist.md @@ -70,18 +70,18 @@ Classification totals are one `story`, 15 `reference`, 11 `evidence`, and one ## 3. New story-page checklist -- [ ] Add `/pipeline/` only after its shared composition and source manifest +- [x] Add `/pipeline/` only after its shared composition and source manifest are validated. -- [ ] Add `/worked-example/` using only `pipeline_sat.cm13`; do not splice in +- [x] 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 +- [x] Add all eight component routes with the exact frozen section order. +- [x] 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, +- [x] Keep history visually distinct inside `/reference/`. +- [x] Keep `/run-dossiers/` an index; do not render `run.json` as Markdown. +- [x] 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. +- [x] Build Pages without generating any dossier or invoking LaTeX. ## 4. Public asset inventory @@ -120,7 +120,7 @@ checks prove the old files are unreferenced before deletion. - [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 +- [x] 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. @@ -182,29 +182,29 @@ checks prove the old files are unreferenced before deletion. keeping it secondary to observed trace output. 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 +6. [x] 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 +7. [x] 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 +- [x] 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 +- [x] Enforce the nine component sections in order. +- [x] Enforce one primary asset owner per component and uniqueness across Pages. -- [ ] Enforce the five allowed semantic labels and reject +- [x] Enforce the five allowed semantic labels and reject `canonical-example`. -- [ ] Enforce GIF owner, nonempty alt text, reduced-motion PNG, caption, +- [x] 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 +- [x] Preserve all current permalinks and validate all literal and generated links/anchors. -- [ ] Distinguish the general pipeline from the named SAT worked example in +- [x] Distinguish the general pipeline from the named SAT worked example in visible copy. -- [ ] Keep technical references and dated evidence available without +- [x] 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, +- [x] Build and check the site with no native build, renderer environment, dossier generation, or LaTeX installation. ## 10. V2 PDF implementation gates @@ -235,12 +235,12 @@ checks prove the old files are unreferenced before deletion. ## 12. Final migration audit -- [ ] The public catalog reports the expected counts for story, reference, +- [x] 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, +- [x] All 27 legacy technical routes and `/` resolve after the migration. +- [x] 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 +- [x] 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. @@ -249,6 +249,6 @@ checks prove the old files are unreferenced before deletion. - [ ] `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, +- [x] 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. diff --git a/docs/plans/2026-09-04-t97-pages-finish.md b/docs/plans/2026-09-04-t97-pages-finish.md new file mode 100644 index 0000000..67c792b --- /dev/null +++ b/docs/plans/2026-09-04-t97-pages-finish.md @@ -0,0 +1,234 @@ +# T97 Pages Narrative Completion Plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use +> superpowers:subagent-driven-development (recommended) or +> superpowers:executing-plans to implement this plan task-by-task. Steps use +> checkbox (`- [ ]`) syntax for tracking. + +**Goal:** Close the already-implemented T97 Pages narrative refactor with an +independent review, fresh reproducible evidence, an accurate migration +checklist, and a pull request against `main`. + +**Architecture:** Preserve the two existing implementation commits and audit +their complete `origin/main...HEAD` change as one coherent migration. Make only +review-driven corrections, keep authored Markdown and the small Jekyll +layout/include layer independent from dossier generation, and validate the +same source and generated-site contracts that CI runs. + +**Tech Stack:** Markdown, Jekyll/GitHub Pages, Liquid, Python 3.13 `unittest`, +the repository Makefile, `uv`, GCC/Clang, Docker using the pinned local +`ghcr.io/actions/jekyll-build-pages:v1.0.13` image, and GitHub CLI. + +**Spec:** `docs/plans/2026-08-31-narrative-architecture-contract.md` + +## Global Constraints + +- Preserve all 27 legacy technical permalinks and the frozen T97 sitemap. +- Every component page keeps the nine frozen H2 sections in order. +- Every narrative animation has exactly one owner, one allowed semantic label, + nonempty alt text, a caption, a reduced-motion PNG, and a contact sheet. +- Pages prose remains authored Markdown; neither `run.json` nor a dossier may + generate prose, navigation, or sitemap content. +- The Pages build must not invoke native solving, the renderer, dossier + generation, PDF/LaTeX, or network access. +- `pipeline_sat.cm13` remains the sole SAT narrative instance; + `unsat-search` remains visibly and cryptographically separate. +- Existing v1 dossier contracts, core models, algorithms, ABI, and ownership + remain unchanged. +- T98 PDF-v2 implementation and its checklist gates are outside this plan. +- Any behavioral correction follows red-green-refactor; documentation-only + evidence updates do not require synthetic tests. +- Do not commit generated Pages output, caches, screenshots, or review scratch + files. + +--- + +### Task 1: Audit and remediate the existing T97 migration + +**Files:** + +- Review: `docs/_includes/`, `docs/_layouts/`, `docs/assets/css/site.css` +- Review: `docs/index.md`, `docs/pipeline.md`, `docs/worked-example.md` +- Review: `docs/components/*.md`, `docs/reference.md`, `docs/evidence.md`, + `docs/run_dossiers.md` +- Review: `docs/assets/narrative/manifest.json` and tracked narrative assets +- Review: `tools/check_pages.py`, `tools/check_generated_pages.py` +- Test: `tests/python/test_pages_checker.py` +- Test: `tests/python/test_generated_pages.py` +- Test: `tests/python/test_multi_engine_dossier.py` +- Test: affected `renderer/test_wang_*.py` files +- Modify only when evidence requires it: the files above and + `docs/plans/2026-08-31-narrative-migration-checklist.md` + +**Interfaces:** + +- Consumes: the frozen narrative contract, the `wang-narrative-assets-v1` + manifest, the existing two T97 commits, and the 27 legacy routes. +- Produces: a reviewed source tree whose source checker and focused unit tests + enforce the frozen taxonomy, ownership, accessibility, identity, and link + contracts. + +- [ ] **Step 1: Review the complete branch diff against the frozen contract** + + Inspect `git diff --find-renames origin/main...HEAD` and record every + Critical, Important, and Minor finding with a file and line. Pay particular + attention to route compatibility, asset deletion/rename safety, unique + ownership, semantic labels, SAT/UNSAT separation, literal Liquid links, and + accidental Pages dependencies on dossier or renderer output. + +- [ ] **Step 2: Reproduce each behavioral finding with a focused failing test** + + Add the smallest real-behavior test to + `tests/python/test_pages_checker.py` or + `tests/python/test_generated_pages.py`. Run it directly with: + + ```bash + PYTHONPATH="$PWD/python" uv run --frozen python -m unittest \ + tests.python.test_pages_checker tests.python.test_generated_pages + ``` + + The new test must fail for the identified defect, not for fixture setup or a + source-text assertion. If the review is clean, do not invent a test or code + change. + +- [ ] **Step 3: Apply the minimal corrections and prove focused green** + + Change only the file responsible for each confirmed finding, then rerun: + + ```bash + make pages-check + PYTHONPATH="$PWD/python" uv run --frozen python -m unittest \ + tests.python.test_pages_checker tests.python.test_generated_pages + ``` + + Expected: the source checker reports 40 routes with the frozen class counts, + and all focused tests pass with no warnings. + +- [ ] **Step 4: Commit review-driven corrections, if any** + + Stage only reviewed source/test files. Use a result-oriented subject and do + not add co-author trailers. If the audit finds no defect, create no empty + commit. + +### Task 2: Rebuild, verify, and reconcile the T97 evidence + +**Files:** + +- Modify: `docs/plans/2026-08-31-narrative-migration-checklist.md` +- Verify: the complete repository tree +- Generate only outside Git: `/tmp/t97-pages-build-20260904/` + +**Interfaces:** + +- Consumes: the reviewed T97 source tree from Task 1 and the pinned GitHub + Pages builder image already present on the host. +- Produces: fresh source, generated-site, browser, compiler, sanitizer, + analyzer, dynamic-analysis, renderer, dossier-v1, and cleanliness evidence; + an evidence-accurate checklist; and a PR-ready branch. + +- [ ] **Step 1: Build Pages from a clean external destination without network** + + Create `/tmp/t97-pages-build-20260904`, mount the repository read-only, and + mount that directory at `/github/workspace/build/pages`. Run the pinned + image as uid/gid `1000:1000` with `--network none` and these exact inputs: + `GITHUB_WORKSPACE=/github/workspace`, `INPUT_SOURCE=docs`, + `INPUT_DESTINATION=build/pages`, `INPUT_VERBOSE=false`, + `INPUT_FUTURE=false`, `GITHUB_REPOSITORY=xtraid/tiling-foundry`, + `GITHUB_API_URL=https://api.github.com`, and `INPUT_BUILD_REVISION` equal to + the reviewed HEAD SHA. Pass an empty `INPUT_TOKEN`. + + Expected: the container exits zero and writes only to the external build + directory. + +- [ ] **Step 2: Validate generated output and browser-visible structure** + + Run: + + ```bash + python3 tools/check_generated_pages.py /tmp/t97-pages-build-20260904 + ``` + + Expected: 40 HTML pages and all emitted `href`, `src`, and `srcset` + references validate. Use the local Playwright image without network to + inspect `/`, `/pipeline/`, `/worked-example/`, and all eight component + routes at desktop and narrow widths; verify one H1, keyboard-reachable + navigation and links, visible focus, meaningful image alternatives, static + reduced-motion fallbacks, and no horizontal overflow. + +- [ ] **Step 3: Run the full repository verification matrix** + + Run each command on the reviewed HEAD and retain its exit status in the task + report: + + ```bash + make check + make strict-check CC=gcc + make strict-check CC=clang + make sanitizer-check + make analyzer-check + make valgrind-check + make cachegrind-check + make parser-fuzz-smoke + make coverage + make run-dossier-smoke + cd renderer && uv run --locked pytest -q + ``` + + Expected: every mandatory command exits zero. Coverage remains informative; + no host-specific timing threshold is introduced. + +- [ ] **Step 4: Reconcile only T97 checklist items proven by fresh evidence** + + Mark the duplicate section-3 Pages-build item complete after Steps 1-2. + Mark only the T97-owned portions of the final migration audit that the fresh + checks prove. Leave every T98 PDF-v2, cross-phase identity, or otherwise + unverified item open. + +- [ ] **Step 5: Perform publication hygiene checks and commit the evidence** + + Run: + + ```bash + git diff --check origin/main...HEAD + git status --short --branch + git diff --summary origin/main...HEAD + git ls-files build .uv-cache .venv | sed -n '1,20p' + ``` + + Confirm no generated build, cache, screenshot, credential, private key, or + unexpected executable mode is staged. Commit only the checklist and this + plan if they changed, using a result-oriented subject without co-author + trailers. + +### Task 3: Independent final review and pull request + +**Files:** + +- Review: `origin/main...HEAD` +- Read: `.github/pull_request_template.md` when present +- Create externally: one GitHub pull request against `main` + +**Interfaces:** + +- Consumes: the reviewed commits and complete fresh verification report. +- Produces: a published `feature/pages-narrative-v1` branch and a PR whose + description records scope, architecture boundaries, tests, and remaining + T98 exclusions. + +- [ ] **Step 1: Obtain an independent whole-branch review** + + Review `origin/main...HEAD` against this plan, the frozen contract, and the + migration checklist. Resolve all Critical and Important findings with a + focused test-first fix and scoped re-review before publication. + +- [ ] **Step 2: Verify the exact tree to publish** + + Re-run `make pages-check`, the external generated-site checker, + `git diff --check origin/main...HEAD`, and `git status --short --branch`. + Confirm HEAD and the verification report refer to the same SHA. + +- [ ] **Step 3: Push the feature branch and open the PR** + + Push `feature/pages-narrative-v1` to `origin` without force, then create one + PR against `main`. Do not merge it. Preserve the worktree for CI feedback + and report the PR URL. diff --git a/docs/post-template.md b/docs/post-template.md index ed5901e..94df524 100644 --- a/docs/post-template.md +++ b/docs/post-template.md @@ -28,12 +28,6 @@ Use normal Markdown structures: north(A) = south(B) ``` -## Figure - -![The edge convention of a Wang tile.]({{ "/assets/images/wang-edge-convention.svg" | relative_url }}) - -_Figure 1. Each triangle carries the label of one directed edge._ - ## Result Close with the evidence, limitations, and the next falsifiable question. diff --git a/docs/reduction_notes.md b/docs/reduction_notes.md index fcfde1c..fc0778c 100644 --- a/docs/reduction_notes.md +++ b/docs/reduction_notes.md @@ -2,6 +2,7 @@ layout: page title: "Yang–Zhang reduction: geometry and witness correspondence" permalink: /reduction_notes/ +page_class: reference description: Mathematical conventions, project-specific geometry, and witness-level evidence for the implemented reduction. section: Yang–Zhang reduction document_kind: Technical note diff --git a/docs/reference.md b/docs/reference.md new file mode 100644 index 0000000..a75e69a --- /dev/null +++ b/docs/reference.md @@ -0,0 +1,23 @@ +--- +layout: story +title: Reference +permalink: /reference/ +page_class: story +description: Maintained contracts, methods, implementation references, bibliography, and visibly separate historical context. +--- + +# Reference + +These documents define maintained interfaces, methods, identities, and +correctness boundaries. They are not generated from a captured run. + +{% assign references = site.pages | where: "page_class", "reference" | sort: "title" %} +{% include document-list.html documents=references %} + +## Historical context + +Historical material explains earlier decisions but does not define current +behavior. + +{% assign history = site.pages | where: "page_class", "history" | sort: "title" %} +{% include document-list.html documents=history %} diff --git a/docs/references.md b/docs/references.md index 289128e..ac1fdc7 100644 --- a/docs/references.md +++ b/docs/references.md @@ -2,6 +2,7 @@ layout: page title: Project references permalink: /references/ +page_class: reference description: Primary papers and authoritative references used by Tiling Foundry. section: Yang–Zhang reduction document_kind: Reference bibliography diff --git a/docs/run_dossiers.md b/docs/run_dossiers.md index 9415840..7b59c73 100644 --- a/docs/run_dossiers.md +++ b/docs/run_dossiers.md @@ -2,6 +2,7 @@ layout: page title: Observed-run dossiers and example index permalink: /run-dossiers/ +page_class: reference 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 @@ -49,8 +50,9 @@ 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 }}) +remains the canonical explanation of event semantics, truncation, and replay. +The [reference solver component]({{ '/components/reference-solver/' | relative_url }}) +owns the public reference animation. 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. diff --git a/docs/serial_solver_implementation_guide.md b/docs/serial_solver_implementation_guide.md index 4df2f81..1a267d6 100644 --- a/docs/serial_solver_implementation_guide.md +++ b/docs/serial_solver_implementation_guide.md @@ -2,6 +2,7 @@ layout: page title: Serial Wang solver and independent verification permalink: /serial_solver_implementation_guide/ +page_class: reference description: Domain propagation, deterministic search, ownership, diagnostics, and the independent verifier used by both native solver paths. section: Architecture and correctness document_kind: Technical reference @@ -19,13 +20,9 @@ result, the optional semantic event trace, and the optional failed-leaf diagnostics. Public headers and regression tests remain authoritative for exact ABI behavior. -
- - - Observed reference solver domains narrowing across root initialization, propagation, decisions, and the final SAT result. - -
Observed state. An offline consumer replays selected events from one complete 2,896-event reference run; skipped visual frames do not imply skipped solver events. The static contact sheet shows every rendered frame.
-
+The [reference solver component]({{ '/components/reference-solver/' | relative_url }}) +owns the observed trace animation. This page remains the detailed API, +ownership, and verification reference for both native paths. ## 1. Scope and dependency boundary @@ -554,7 +551,7 @@ The benchmark and profiler paths keep metrics runs separate from timings and measure MRV scans and packed-word probes, queue duplication, trail pressure, domain reductions, support aggregation, SAT-copy bytes, process peak RSS, and instruction/cache attribution. Dated reports in the -[solver optimization section]({{ '/#solver-optimization' | relative_url }}) +[evidence index]({{ '/evidence/' | relative_url }}) record the evidence for each retained optimized mechanism. ## 15. Current guarantees and limits diff --git a/docs/solver_byte_support_2026-08-20.md b/docs/solver_byte_support_2026-08-20.md index ed11f29..8085a16 100644 --- a/docs/solver_byte_support_2026-08-20.md +++ b/docs/solver_byte_support_2026-08-20.md @@ -2,6 +2,7 @@ layout: page title: Optimized solver byte-wise support tables permalink: /solver_byte_support_2026-08-20/ +page_class: evidence description: Evidence for aggregating Wang propagation support by domain byte. section: Solver optimization document_kind: Benchmark report @@ -12,13 +13,9 @@ nav_order: 60 # Optimized solver byte-wise support tables — 20 August 2026 -
- - - Didactic comparison of the reference solver baseline and the six retained optimized serial mechanisms. - -
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.
-
+The [optimized solver component]({{ '/components/optimized-solver/' | relative_url }}) +owns the six-mechanism overview. The measurements below, not that didactic +asset, establish the effect of byte-wise support aggregation. This report evaluates only the union of compatible neighbor tiles during propagation. The reference path retains the baseline loop over every set tile diff --git a/docs/solver_comparison_benchmark.md b/docs/solver_comparison_benchmark.md index 505f5a7..3a14762 100644 --- a/docs/solver_comparison_benchmark.md +++ b/docs/solver_comparison_benchmark.md @@ -2,6 +2,7 @@ layout: page title: Native and Z3 solver comparison benchmark permalink: /solver_comparison_benchmark/ +page_class: reference description: Reproducible protocol for comparing the native and Python Z3 decision paths. section: Cross-engine benchmarks document_kind: Benchmark protocol diff --git a/docs/solver_comparison_smoke_2026-08-21.md b/docs/solver_comparison_smoke_2026-08-21.md index c131f52..38389cd 100644 --- a/docs/solver_comparison_smoke_2026-08-21.md +++ b/docs/solver_comparison_smoke_2026-08-21.md @@ -2,6 +2,7 @@ layout: page title: Native and Z3 solver comparison smoke baseline permalink: /solver_comparison_smoke_2026-08-21/ +page_class: evidence description: Seven-sample native and Z3 baseline on the smallest shared SAT and UNSAT inputs. section: Cross-engine benchmarks document_kind: Benchmark report diff --git a/docs/solver_dynamic_stack_2026-08-17.md b/docs/solver_dynamic_stack_2026-08-17.md index 22fa709..5d6947a 100644 --- a/docs/solver_dynamic_stack_2026-08-17.md +++ b/docs/solver_dynamic_stack_2026-08-17.md @@ -2,6 +2,7 @@ layout: page title: Optimized solver dynamic DFS stack permalink: /solver_dynamic_stack_2026-08-17/ +page_class: evidence description: Evidence for the optimized solver's geometrically growing DFS stack. section: Solver optimization document_kind: Benchmark report @@ -12,13 +13,9 @@ nav_order: 30 # Optimized solver dynamic DFS stack — 17 August 2026 -
- - - Didactic comparison of the reference solver baseline and the six retained optimized serial mechanisms. - -
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.
-
+The [optimized solver component]({{ '/components/optimized-solver/' | relative_url }}) +owns the six-mechanism overview. The measurements below, not that didactic +asset, establish the effect of the dynamic DFS stack. This report evaluates only DFS stack storage. The reference path still allocates one `SearchFrame` per active cell. The optimized path starts with at diff --git a/docs/solver_initial_trail_2026-08-17.md b/docs/solver_initial_trail_2026-08-17.md index 6e743c2..c79227c 100644 --- a/docs/solver_initial_trail_2026-08-17.md +++ b/docs/solver_initial_trail_2026-08-17.md @@ -2,6 +2,7 @@ layout: page title: Optimized solver initial-trail removal permalink: /solver_initial_trail_2026-08-17/ +page_class: evidence description: Evidence for omitting rollback entries during non-rollbackable initial propagation. section: Solver optimization document_kind: Benchmark report @@ -12,13 +13,9 @@ nav_order: 40 # Optimized solver initial-trail removal — 17 August 2026 -
- - - Didactic comparison of the reference solver baseline and the six retained optimized serial mechanisms. - -
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.
-
+The [optimized solver component]({{ '/components/optimized-solver/' | relative_url }}) +owns the six-mechanism overview. The measurements below, not that didactic +asset, establish the effect of initial-trail omission. This report evaluates undo-trail recording during initial propagation. The reference path keeps the baseline behavior. The optimized path applies the diff --git a/docs/solver_mrv_index_2026-08-28.md b/docs/solver_mrv_index_2026-08-28.md index 1aaf217..973555b 100644 --- a/docs/solver_mrv_index_2026-08-28.md +++ b/docs/solver_mrv_index_2026-08-28.md @@ -2,6 +2,7 @@ layout: page title: Optimized solver MRV index permalink: /solver_mrv_index_2026-08-28/ +page_class: evidence description: Evidence for the optimized solver's private row-major MRV bucket index. section: Solver optimization document_kind: Benchmark report @@ -18,7 +19,8 @@ row-major scan. The optimized path derives 22 private buckets for domain sizes 2 through 23, stores bucket membership in packed cell-index bitsets, and keeps one cached domain-size byte per dense cell. Selecting the first nonempty size bucket and then its lowest set cell bit preserves the existing minimum-domain, -row-major tie break. +row-major tie break. The [optimized solver component]({{ '/components/optimized-solver/' | relative_url }}) owns the narrative trace +and the six-mechanism overview; this report remains dated evidence. The index is created lazily only after a root branch propagates successfully and search must descend to a child. Root conflicts, fully resolved regions, diff --git a/docs/solver_performance_scope.md b/docs/solver_performance_scope.md index 4b04e45..298ce96 100644 --- a/docs/solver_performance_scope.md +++ b/docs/solver_performance_scope.md @@ -2,6 +2,7 @@ layout: page title: Solver optimization methodology and execution paths permalink: /solver_performance_scope/ +page_class: reference description: Stable correctness boundaries, measurement rules, and current mechanisms for the reference and optimized Wang solver paths. section: Solver optimization document_kind: Methodology diff --git a/docs/solver_queue_dedup_2026-08-20.md b/docs/solver_queue_dedup_2026-08-20.md index ce0876f..8a4bf7e 100644 --- a/docs/solver_queue_dedup_2026-08-20.md +++ b/docs/solver_queue_dedup_2026-08-20.md @@ -2,6 +2,7 @@ layout: page title: Optimized solver queue deduplication permalink: /solver_queue_dedup_2026-08-20/ +page_class: evidence description: Evidence for the optimized solver's packed pending-cell index. section: Solver optimization document_kind: Benchmark report @@ -12,13 +13,9 @@ nav_order: 80 # Optimized solver queue deduplication — 20 August 2026 -
- - - Didactic comparison of the reference solver baseline and the six retained optimized serial mechanisms. - -
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.
-
+The [optimized solver component]({{ '/components/optimized-solver/' | relative_url }}) +owns the six-mechanism overview. The measurements below, not that didactic +asset, establish the effect of queue deduplication. This accepted mechanism changes only the optimized propagation queue. An enqueue request for a cell that already has an unconsumed FIFO occurrence is diff --git a/docs/solver_queue_trail_profile_2026-08-20.md b/docs/solver_queue_trail_profile_2026-08-20.md index cb4d79b..93c8dda 100644 --- a/docs/solver_queue_trail_profile_2026-08-20.md +++ b/docs/solver_queue_trail_profile_2026-08-20.md @@ -2,6 +2,7 @@ layout: page title: Optimized solver queue and trail profile permalink: /solver_queue_trail_profile_2026-08-20/ +page_class: evidence description: Queue, trail, Callgrind, and Cachegrind evidence used to select queue deduplication. section: Solver optimization document_kind: Profiling report diff --git a/docs/solver_reference_profile_2026-08-17.md b/docs/solver_reference_profile_2026-08-17.md index 8bb4ff1..d0184de 100644 --- a/docs/solver_reference_profile_2026-08-17.md +++ b/docs/solver_reference_profile_2026-08-17.md @@ -2,6 +2,7 @@ layout: page title: Serial solver reference profile permalink: /solver_reference_profile_2026-08-17/ +page_class: evidence description: Reproducible reference measurements for the serial Wang solver. section: Solver optimization document_kind: Benchmark report diff --git a/docs/solver_sat_ownership_2026-08-20.md b/docs/solver_sat_ownership_2026-08-20.md index 47448ee..e624c88 100644 --- a/docs/solver_sat_ownership_2026-08-20.md +++ b/docs/solver_sat_ownership_2026-08-20.md @@ -2,6 +2,7 @@ layout: page title: Optimized solver SAT ownership transfer permalink: /solver_sat_ownership_2026-08-20/ +page_class: evidence description: Evidence for transferring the verified SAT domain buffer without a redundant final copy. section: Solver optimization document_kind: Benchmark report @@ -12,13 +13,9 @@ nav_order: 50 # Optimized solver SAT ownership transfer — 20 August 2026 -
- - - Didactic comparison of the reference solver baseline and the six retained optimized serial mechanisms. - -
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.
-
+The [optimized solver component]({{ '/components/optimized-solver/' | relative_url }}) +owns the six-mechanism overview. The measurements below, not that didactic +asset, establish the effect of SAT ownership transfer. This report evaluates only construction of a successful solver result. The reference path retains the baseline behavior: after independent SAT diff --git a/docs/wang_explainability_snapshots.md b/docs/wang_explainability_snapshots.md index 37ba5ac..e596c97 100644 --- a/docs/wang_explainability_snapshots.md +++ b/docs/wang_explainability_snapshots.md @@ -2,6 +2,7 @@ layout: page title: Static pipeline snapshots and explainable Wang views permalink: /wang-explainability-snapshots/ +page_class: reference description: Versioned formula, tileset, and unassigned-region snapshots consumed by the isolated Wang renderer. section: Architecture and correctness document_kind: Data and rendering contract diff --git a/docs/wang_reduction_explanation.md b/docs/wang_reduction_explanation.md index 35160f8..e42527e 100644 --- a/docs/wang_reduction_explanation.md +++ b/docs/wang_reduction_explanation.md @@ -2,6 +2,7 @@ layout: page title: "Yang–Zhang reduction explanation contract" permalink: /wang-reduction-explanation/ +page_class: reference description: Native-produced signal, permutation, and gadget provenance for one formula-to-region construction. section: Yang–Zhang reduction document_kind: Data and rendering contract diff --git a/docs/wang_solution_v1.md b/docs/wang_solution_v1.md index b185fdc..cd2a94e 100644 --- a/docs/wang_solution_v1.md +++ b/docs/wang_solution_v1.md @@ -2,6 +2,7 @@ layout: page title: Wang solution v1 data contract permalink: /wang-solution-v1/ +page_class: reference description: Versioned JSON contract and independent semantic checks for square Wang SAT witnesses. section: Architecture and correctness document_kind: Data contract diff --git a/docs/wang_solver_trace.md b/docs/wang_solver_trace.md index f24605d..0d5f49d 100644 --- a/docs/wang_solver_trace.md +++ b/docs/wang_solver_trace.md @@ -2,6 +2,7 @@ layout: page title: Native solver event trace and offline replay permalink: /wang-solver-trace/ +page_class: reference description: Bounded semantic events, full-state checkpoints, hash-bound transport, and presentation-only replay for native Wang solves. section: Architecture and correctness document_kind: Data and rendering contract @@ -18,13 +19,9 @@ actually observed; it is not a reconstructed lesson, a profiler sample, or a claim about a different engine. Ordinary solve calls retain their original ABI and allocate no provenance storage. -
- - - Observed reference solver domains narrowing from the initial state through propagation and decisions to a verified SAT result. - -
Observed state. These frames are selected from one complete 2,896-event reference trace. The renderer replays the versioned deltas once; frame selection does not change their order. The static contact sheet shows all selected states.
-
+The [reference solver component]({{ '/components/reference-solver/' | relative_url }}) +owns and explains the observed reference animation. This contract remains the +authority for events, checkpoints, completeness, identity, and replay. ## Native boundary and ownership diff --git a/docs/wang_square_to_hex.md b/docs/wang_square_to_hex.md index 9df4b6b..a36c8c8 100644 --- a/docs/wang_square_to_hex.md +++ b/docs/wang_square_to_hex.md @@ -2,6 +2,7 @@ layout: page title: Square-to-hex presentation port permalink: /wang-square-to-hex/ +page_class: reference description: Algebra, coordinate convention, inverse proof, and raster boundary for the verified presentation-only square-to-hex port. section: Architecture and correctness document_kind: Technical reference @@ -34,13 +35,9 @@ The exact edge tuple, coordinate convention, deterministic fresh-color rule, and finite-region bijection below are Tiling Foundry's formalization of that construction. They are not attributed to either source's diagram notation. -
- - - Verified square-to-hex transformation preserving four source edges and adding the fresh kappa color. - -
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.
-
+The [visualization component]({{ '/components/visualization/' | relative_url }}) +owns the checked transformation animation. The algebra, inverse, and +raster-independent checker documented below remain the correctness boundary. ## Project convention diff --git a/docs/wang_z3_edge_table_2026-08-24.md b/docs/wang_z3_edge_table_2026-08-24.md index b66fab6..f27f233 100644 --- a/docs/wang_z3_edge_table_2026-08-24.md +++ b/docs/wang_z3_edge_table_2026-08-24.md @@ -2,6 +2,7 @@ layout: page title: Wang Z3 edge-table model permalink: /wang_z3_edge_table_2026-08-24/ +page_class: reference description: Constraint model, correctness evidence, and before/after smoke measurement for the Wang Z3 edge-table oracle. section: Cross-engine benchmarks document_kind: Oracle model report @@ -25,13 +26,9 @@ public `solve_tiling()` result contract. `SAT`, `UNSAT`, `UNKNOWN`, dense row-major witnesses, inactive cells, boundary colors, and generic tilesets are preserved. -
- - - Canonical Wang Z3 example progressing through the project-defined row-major encoding order to the returned model. - -
Encoding order. The frames replay the project-owned constraint construction and returned result; they do not claim to expose Z3's internal search or debug order. The static contact sheet shows all five stages.
-
+The [Wang Z3 component]({{ '/components/wang-z3/' | relative_url }}) owns the +encoding-order animation. It depicts project-owned construction and the +returned model, never Z3's internal search or debug order. ## Reproducible summary boundary diff --git a/docs/worked-example.md b/docs/worked-example.md new file mode 100644 index 0000000..5636397 --- /dev/null +++ b/docs/worked-example.md @@ -0,0 +1,57 @@ +--- +layout: story +title: Worked SAT example +permalink: /worked-example/ +page_class: story +owned_assets: worked_example, formula +description: One named pipeline_sat.cm13 instance followed from source bytes to independently checked square and hex presentations. +--- + +# Worked SAT example + +This page follows only `tests/instances/pipeline_sat.cm13`. Its SHA-256 is +`3caaa6b29ac988fb4f51cc7071202d83ea1591ba6170e683b6da449cb3641542`. +No initial-domain override is applied. The separate search-UNSAT example is +not spliced into this run. + +{% include narrative-static.html asset_id="worked_example" image="/assets/narrative/pipeline-overview/worked-example.png" alt="Eight static panels follow the captured source from formula to checked presentation." width="1080" height="940" label="observed" caption="Static t0 through tn component milestones for one SAT run." source="wang-run-dossier-v2#named-components" %} + +## Source formula + +The parser reads a canonical Cubic Monotone 1-in-3 SAT document with three +variables and three source-order clauses. The snapshot below is bound to those +source bytes; it is not reconstructed from a later tiling. + +{% include narrative-static.html asset_id="formula" image="/assets/narrative/formula.png" alt="The parsed CM1-in-3 formula and its source-order clauses." width="796" height="394" label="observed" caption="Parsed formula snapshot for the named canonical source." source="cm13-formula-snapshot-v1" %} + +## Decisions and construction + +Boolean Z3 returns SAT with a checked assignment. The native builder constructs +one region, one fixed tileset snapshot, and explicit construction provenance. +Reference, optimized, and Wang Z3 solves then report SAT over those shared +identities. Agreement means equal terminal status and independently valid +witnesses; different valid witnesses need not be byte-identical. + +## Verification and presentation + +Six named checker records cover the Boolean assignment, both native tilings, +the assignments extracted through the witness correspondence, and the Wang Z3 +tiling. Only after those checks does the presentation layer render the square +witness, recognize exact generalized contours, and apply the independently +checked square-to-hex mapping. + +The milestone sequence links to the owned explanations for the +[tileset]({{ '/components/tileset/' | relative_url }}), +[Boolean Z3]({{ '/components/boolean-z3/' | relative_url }}), +[Yang–Zhang reduction]({{ '/components/yang-zhang/' | relative_url }}), +[reference solver]({{ '/components/reference-solver/' | relative_url }}), +[optimized solver]({{ '/components/optimized-solver/' | relative_url }}), +[Wang Z3]({{ '/components/wang-z3/' | relative_url }}), +[verification]({{ '/components/verification/' | relative_url }}), and +[visualization]({{ '/components/visualization/' | relative_url }}). + +Raw durations belong to this capture and environment. They are not a benchmark +or a performance ranking. The [run dossier index]({{ '/run-dossiers/' | relative_url }}) +documents the immutable capture boundary, while the +[pipeline page]({{ '/pipeline/' | relative_url }}) separates the general +architecture from this one observed example. diff --git a/docs/yang_zhang_builder_design.md b/docs/yang_zhang_builder_design.md index fe460b0..f2f814a 100644 --- a/docs/yang_zhang_builder_design.md +++ b/docs/yang_zhang_builder_design.md @@ -2,6 +2,7 @@ layout: page title: "Yang–Zhang formula-to-region builder" permalink: /yang_zhang_builder_design/ +page_class: reference description: Data flow, geometry, ownership, and tested invariants of the implemented formula-to-region builder. section: Yang–Zhang reduction document_kind: Implementation contract @@ -44,13 +45,9 @@ Primary source: Text parsing, solving, independent verification, scheduling, oracles, solution transport, and rendering have separate contracts. -
- - - Canonical Yang–Zhang construction with native variable, forwarder, crossover, and clause gadget spans appearing in source order. - -
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.
-
+The [Yang–Zhang component]({{ '/components/yang-zhang/' | relative_url }}) owns +the canonical construction animation. This page remains the detailed builder +contract for geometry, provenance, lifetimes, and black-box obligations. ## 1. Module boundary diff --git a/docs/assets/images/square-to-hex/contact-sheet.png b/renderer/test_data/square-to-hex-animation/contact-sheet.png similarity index 100% rename from docs/assets/images/square-to-hex/contact-sheet.png rename to renderer/test_data/square-to-hex-animation/contact-sheet.png diff --git a/docs/assets/images/square-to-hex/frame-00.png b/renderer/test_data/square-to-hex-animation/frame-00.png similarity index 100% rename from docs/assets/images/square-to-hex/frame-00.png rename to renderer/test_data/square-to-hex-animation/frame-00.png diff --git a/docs/assets/images/square-to-hex/frame-01.png b/renderer/test_data/square-to-hex-animation/frame-01.png similarity index 100% rename from docs/assets/images/square-to-hex/frame-01.png rename to renderer/test_data/square-to-hex-animation/frame-01.png diff --git a/docs/assets/images/square-to-hex/frame-02.png b/renderer/test_data/square-to-hex-animation/frame-02.png similarity index 100% rename from docs/assets/images/square-to-hex/frame-02.png rename to renderer/test_data/square-to-hex-animation/frame-02.png diff --git a/docs/assets/images/square-to-hex/frame-03.png b/renderer/test_data/square-to-hex-animation/frame-03.png similarity index 100% rename from docs/assets/images/square-to-hex/frame-03.png rename to renderer/test_data/square-to-hex-animation/frame-03.png diff --git a/docs/assets/images/square-to-hex/trace.gif b/renderer/test_data/square-to-hex-animation/trace.gif similarity index 100% rename from docs/assets/images/square-to-hex/trace.gif rename to renderer/test_data/square-to-hex-animation/trace.gif diff --git a/renderer/test_wang_algorithm_animation.py b/renderer/test_wang_algorithm_animation.py index 3c9331f..bccfb13 100644 --- a/renderer/test_wang_algorithm_animation.py +++ b/renderer/test_wang_algorithm_animation.py @@ -18,7 +18,8 @@ ROOT / "tests/fixtures/pipeline_sat_reduction_explain/manifest.json" ) SQUARE_SOLUTION = ROOT / "tests/fixtures/wang_solution_v1_square_sat.json" -GOLDENS = ROOT / "docs/assets/images" +GOLDENS = ROOT / "docs/assets/narrative" +PRIVATE_GOLDENS = RENDERER / "test_data" def _tree_bytes(directory: Path) -> dict[str, bytes]: @@ -53,7 +54,7 @@ def test_builder_animation_uses_versioned_provenance_and_is_byte_stable(tmp_path _assert_stable_assets( tmp_path / "first", tmp_path / "second", - GOLDENS / "builder-routing", + GOLDENS / "region-construction", frame_count=6, fallback_name="frame-04.png", ) @@ -81,7 +82,7 @@ def test_hex_animation_checks_the_pure_port_and_is_byte_stable(tmp_path): _assert_stable_assets( tmp_path / "first", tmp_path / "second", - GOLDENS / "square-to-hex", + PRIVATE_GOLDENS / "square-to-hex-animation", frame_count=4, fallback_name="frame-02.png", ) diff --git a/renderer/test_wang_trace.py b/renderer/test_wang_trace.py index c63c94c..cde4d9d 100644 --- a/renderer/test_wang_trace.py +++ b/renderer/test_wang_trace.py @@ -20,7 +20,7 @@ ROOT = RENDERER.parent FIXTURE_DIRECTORY = ROOT / "tests/fixtures/pipeline_sat_solver_trace" MANIFEST = FIXTURE_DIRECTORY / "manifest.json" -GOLDENS = ROOT / "docs/assets/images/solver-trace" +GOLDENS = ROOT / "docs/assets/narrative/reference-trace" def _tree_bytes(directory: Path) -> dict[str, bytes]: @@ -99,12 +99,12 @@ def test_loads_and_replays_hash_bound_trace_without_solver_imports(): def test_one_composition_chain_is_byte_stable_for_png_sheet_and_gif(tmp_path): - first = render_trace_assets(MANIFEST, tmp_path / "first", max_frames=8) - second = render_trace_assets(MANIFEST, tmp_path / "second", max_frames=8) + first = render_trace_assets(MANIFEST, tmp_path / "first", max_frames=10) + second = render_trace_assets(MANIFEST, tmp_path / "second", max_frames=10) assert _tree_bytes(tmp_path / "first") == _tree_bytes(tmp_path / "second") assert _tree_bytes(tmp_path / "first") == _tree_bytes(GOLDENS) - assert len(first.frames) == 8 + assert len(first.frames) == 10 assert first.fallback.name == "frame-002517.png" assert first.animation.name == "trace.gif" assert first.contact_sheet.name == "contact-sheet.png" @@ -113,16 +113,16 @@ def test_one_composition_chain_is_byte_stable_for_png_sheet_and_gif(tmp_path): assert frame.size == (988, 414) with Image.open(first.animation) as animation: assert animation.format == "GIF" - assert animation.n_frames == 8 + assert animation.n_frames == 10 def test_semantic_milestones_precede_gap_filling(): bundle = load_trace_bundle(MANIFEST) - selected = select_semantic_milestones(bundle.trace.events, 8) + selected = select_semantic_milestones(bundle.trace.events, 10) - assert selected == (0, 1, 2516, 2517, 2518, 2893, 2894, 2895) + assert selected == (0, 1, 1258, 1887, 2516, 2517, 2518, 2893, 2894, 2895) assert selected != tuple( - slot * (len(bundle.trace.events) - 1) // 7 for slot in range(8) + slot * (len(bundle.trace.events) - 1) // 9 for slot in range(10) ) diff --git a/renderer/test_wang_z3_summary.py b/renderer/test_wang_z3_summary.py index 1f9b17d..f3fa5fc 100644 --- a/renderer/test_wang_z3_summary.py +++ b/renderer/test_wang_z3_summary.py @@ -18,7 +18,7 @@ RENDERER = Path(__file__).resolve().parent ROOT = RENDERER.parent FIXTURES = ROOT / "tests/fixtures/pipeline_sat_z3" -GOLDENS = ROOT / "docs/assets/images/z3-encoding" +GOLDENS = ROOT / "docs/assets/narrative" def _tree_bytes(directory: Path) -> dict[str, bytes]: @@ -50,7 +50,7 @@ def test_encoding_order_animation_is_byte_stable_and_matches_goldens(tmp_path): render_wang_z3_assets(source, tmp_path / "second") assert _tree_bytes(tmp_path / "first") == _tree_bytes(tmp_path / "second") - assert _tree_bytes(tmp_path / "first") == _tree_bytes(GOLDENS) + assert _tree_bytes(tmp_path / "first") == _tree_bytes(GOLDENS / "wang-z3") assert first.fallback.name == "frame-03.png" with Image.open(first.animation) as animation: assert animation.format == "GIF" @@ -63,6 +63,7 @@ def test_boolean_encoding_order_animation_is_byte_stable(tmp_path): render_boolean_z3_assets(source, tmp_path / "second") assert _tree_bytes(tmp_path / "first") == _tree_bytes(tmp_path / "second") + assert _tree_bytes(tmp_path / "first") == _tree_bytes(GOLDENS / "boolean-z3") assert first.fallback.name == "frame-02.png" with Image.open(first.animation) as animation: assert animation.format == "GIF" diff --git a/tests/python/test_generated_pages.py b/tests/python/test_generated_pages.py index 7082a73..cb62300 100644 --- a/tests/python/test_generated_pages.py +++ b/tests/python/test_generated_pages.py @@ -8,20 +8,36 @@ ROOT = Path(__file__).resolve().parents[2] sys.path.insert(0, str(ROOT / "tools")) -from check_generated_pages import REPRESENTATIVE_ROUTES, check_site # noqa: E402 +from check_generated_pages import ( # noqa: E402 + COMPONENT_HEADINGS, + COMPONENTS, + EXPECTED_ROUTE_CLASSES, + EXPECTED_ROUTES, + check_site, +) +from check_pages import ANIMATION_POLICY, STATIC_POLICY # noqa: E402 SITE_URL = "https://xtraid.github.io" BASEURL = "/tiling-foundry" -def _html(route: str, title: str, body: str, kind: str = "page") -> str: +def _html( + route: str, + title: str, + body: str, + *, + page_class: str, + kind: str = "page", + component_id: str = "", +) -> str: return f""" {title} - + Skip
{body}
""" @@ -37,16 +53,69 @@ def _valid_site(root: Path) -> None: (root / "assets").mkdir() (root / "assets/site.css").write_text("body {}\n", encoding="utf-8") (root / "assets/main.js").write_text("export {};\n", encoding="utf-8") - body = f"""

Tiling Foundry

-
-
-
+ home_body = f"""

Tiling Foundry

+
+
Principles""" - _write(root, "/", _html("/", "Tiling Foundry", body, "home")) - for route in REPRESENTATIVE_ROUTES[1:]: - label = route.strip("/").replace("_", " ").title() - body = f'

{label}

Home' - _write(root, route, _html(route, f"{label} · Tiling Foundry", body)) + _write( + root, + "/", + _html( + "/", + "Tiling Foundry", + home_body, + page_class="story", + kind="home", + ), + ) + for route in sorted(EXPECTED_ROUTES - {"/"}): + label = route.strip("/").replace("-", " ").replace("_", " ").title() + component_id = COMPONENTS[route][0] if route in COMPONENTS else "" + headings = "".join(f"

{heading}

" for heading in COMPONENT_HEADINGS) + body = f'

{label}

{headings}Home' + _write( + root, + route, + _html( + route, + f"{label} · Tiling Foundry", + body, + page_class=EXPECTED_ROUTE_CLASSES[route], + component_id=component_id, + ), + ) + + for asset_id, (route, _) in ANIMATION_POLICY.items(): + page = root / route.strip("/") / "index.html" if route != "/" else root / "index.html" + figure = f"""
+ +{asset_id} animation. +
{asset_id} caption. +Contact sheet +
""" + page.write_text( + page.read_text(encoding="utf-8").replace("", f"{figure}"), + encoding="utf-8", + ) + narrative = root / "assets/narrative" / asset_id + narrative.mkdir(parents=True, exist_ok=True) + for name in ("fallback.png", "animation.gif", "contact-sheet.png"): + (narrative / name).write_bytes(b"asset") + + for asset_id, (route, _) in STATIC_POLICY.items(): + if asset_id == "presentation_status": + continue + page = root / route.strip("/") / "index.html" if route != "/" else root / "index.html" + figure = f"""
+{asset_id} image. +
{asset_id} caption.
""" + page.write_text( + page.read_text(encoding="utf-8").replace("", f"{figure}"), + encoding="utf-8", + ) + narrative = root / "assets/narrative" / asset_id + narrative.mkdir(parents=True, exist_ok=True) + (narrative / "image.png").write_bytes(b"asset") def _contrast(foreground: str, background: str) -> float: @@ -65,12 +134,13 @@ def luminance(color: str) -> float: class GeneratedPagesTests(unittest.TestCase): - def test_accepts_semantic_pages_and_resolved_targets(self) -> None: + def test_accepts_all_routes_and_resolved_targets(self) -> None: with tempfile.TemporaryDirectory() as directory: root = Path(directory) _valid_site(root) result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) self.assertEqual(result.errors, ()) + self.assertEqual(result.page_count, 40) def test_rejects_the_known_home_regression_and_broken_links(self) -> None: with tempfile.TemporaryDirectory() as directory: @@ -94,6 +164,169 @@ def test_rejects_the_known_home_regression_and_broken_links(self) -> None: self.assertIn("unexpected home title", errors) self.assertIn("unresolved href target", errors) + def test_checks_generated_animation_fallback_contact_sheet_and_dimensions(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + _valid_site(root) + route = "/components/boolean-z3/" + page = root / route.strip("/") / "index.html" + html = page.read_text(encoding="utf-8") + figure = f"""
+ + +
Caption. +Contact sheet +
""" + page.write_text(html.replace("", f"{figure}"), encoding="utf-8") + narrative = root / "assets/narrative/boolean-z3" + narrative.mkdir(parents=True) + for name in ("fallback.png", "animation.gif", "contact-sheet.png"): + (narrative / name).write_bytes(b"asset") + good = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + self.assertEqual(good.errors, ()) + + broken = page.read_text(encoding="utf-8") + broken = broken.replace(' width="940" height="430"', "") + broken = broken.replace("contact-sheet.png", "frames.png") + page.write_text(broken, encoding="utf-8") + result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + errors = "\n".join(result.errors) + self.assertIn("lacks positive intrinsic dimensions", errors) + self.assertIn("requires one contact-sheet link", errors) + + def test_rejects_an_omitted_required_animation(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + _valid_site(root) + page = root / "components/boolean-z3/index.html" + html = page.read_text(encoding="utf-8") + start = html.index('
') + end = html.index("
", start) + len("") + page.write_text(html[:start] + html[end:], encoding="utf-8") + result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + + self.assertIn( + "missing narrative animation asset 'boolean_z3'", + "\n".join(result.errors), + ) + + def test_rejects_an_omitted_required_static(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + _valid_site(root) + page = root / "worked-example/index.html" + html = page.read_text(encoding="utf-8") + start = html.index('
') + end = html.index("
", start) + len("") + page.write_text(html[:start] + html[end:], encoding="utf-8") + result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + + self.assertIn( + "missing narrative static asset 'formula'", + "\n".join(result.errors), + ) + + def test_rejects_duplicate_and_wrong_route_asset_id(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + _valid_site(root) + page = root / "worked-example/index.html" + html = page.read_text(encoding="utf-8").replace( + 'data-asset-id="formula"', + 'data-asset-id="worked_example"', + ) + page.write_text(html, encoding="utf-8") + result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + + errors = "\n".join(result.errors) + self.assertIn("narrative asset 'worked_example' occurs 2 times", errors) + self.assertIn("missing narrative static asset 'formula'", errors) + + def test_rejects_an_asset_id_on_the_wrong_owner_route(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + _valid_site(root) + worked = root / "worked-example/index.html" + html = worked.read_text(encoding="utf-8") + start = html.index('
') + end = html.index("
", start) + len("") + worked.write_text(html[:start] + html[end:], encoding="utf-8") + boolean = root / "components/boolean-z3/index.html" + boolean.write_text( + boolean.read_text(encoding="utf-8").replace( + 'data-asset-id="boolean_z3"', + 'data-asset-id="formula"', + ), + encoding="utf-8", + ) + result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + + self.assertIn( + "narrative asset 'formula' is rendered on '/components/boolean-z3/', expected owner '/worked-example/'", + "\n".join(result.errors), + ) + + def test_rejects_wrong_narrative_asset_kind(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + _valid_site(root) + page = root / "components/boolean-z3/index.html" + html = page.read_text(encoding="utf-8").replace( + 'class="narrative-asset narrative-animation" data-asset-id="boolean_z3"', + 'class="narrative-asset narrative-static" data-asset-id="boolean_z3"', + ) + page.write_text(html, encoding="utf-8") + result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + + self.assertIn( + "narrative asset 'boolean_z3' must be an animation figure", + "\n".join(result.errors), + ) + + def test_rejects_narrative_animation_with_swapped_asset_roles(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + _valid_site(root) + route = "/components/boolean-z3/" + page = root / route.strip("/") / "index.html" + html = page.read_text(encoding="utf-8") + figure = f"""
+ + +
Caption. +Animation +
""" + page.write_text(html.replace("", f"{figure}"), encoding="utf-8") + narrative = root / "assets/narrative/boolean-z3" + narrative.mkdir(parents=True) + for name in ("fallback.png", "animation.gif", "contact-sheet.png"): + (narrative / name).write_bytes(b"asset") + + result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + + errors = "\n".join(result.errors) + self.assertIn("must contain exactly one GIF", errors) + self.assertIn("requires one contact-sheet link", errors) + + def test_rejects_missing_component_heading_and_body_identity(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + _valid_site(root) + page = root / "components/tileset/index.html" + html = page.read_text(encoding="utf-8") + html = html.replace("

Trust boundary

", "") + html = html.replace('data-component-id="tileset"', 'data-component-id="other"') + page.write_text(html, encoding="utf-8") + result = check_site(root, site_url=SITE_URL, baseurl=BASEURL) + errors = "\n".join(result.errors) + self.assertIn("expected component id", errors) + self.assertIn("component H2 sequence", errors) + def test_faint_and_comment_text_meet_normal_text_contrast(self) -> None: css = (ROOT / "docs/assets/css/site.css").read_text(encoding="utf-8") root_block = re.search(r":root\s*\{(.*?)\n\}", css, re.DOTALL) diff --git a/tests/python/test_multi_engine_dossier.py b/tests/python/test_multi_engine_dossier.py index ce29f0e..286a5de 100644 --- a/tests/python/test_multi_engine_dossier.py +++ b/tests/python/test_multi_engine_dossier.py @@ -359,6 +359,17 @@ def test_same_compositor_bytes_serve_run_and_canonical_pages(self) -> None: if path.is_file() and path.name != "manifest.json" } self.assertEqual(run_files, pages_files) + public_root = ROOT / "docs/assets/narrative" + public_manifest = load_narrative_assets( + public_root / "manifest.json", self.sat_document + ) + self.assertEqual(public_manifest["product"], "canonical-pages") + public_files = { + path.relative_to(public_root): path.read_bytes() + for path in public_root.rglob("*") + if path.is_file() and path.name != "manifest.json" + } + self.assertEqual(pages_files, public_files) def test_narrative_manifest_rejects_metadata_and_asset_tampering(self) -> None: copied = self.root / "narrative-tampered" diff --git a/tests/python/test_pages_checker.py b/tests/python/test_pages_checker.py new file mode 100644 index 0000000..25e1901 --- /dev/null +++ b/tests/python/test_pages_checker.py @@ -0,0 +1,230 @@ +from copy import deepcopy +import hashlib +from pathlib import Path +import sys +import tempfile +import unittest +from unittest import mock + + +ROOT = Path(__file__).resolve().parents[2] +sys.path.insert(0, str(ROOT / "tools")) + +import check_pages # noqa: E402 + + +def _documents() -> dict[str, check_pages.Document]: + errors: list[str] = [] + documents = check_pages.check_catalog(errors) + if errors: + raise AssertionError("\n".join(errors)) + return documents + + +class PagesCheckerTests(unittest.TestCase): + def test_repository_source_and_manifest_pass(self) -> None: + errors: list[str] = [] + documents = check_pages.check_catalog(errors) + check_pages.check_liquid_links(documents, errors) + animations, statics = check_pages.check_narrative_assets(documents, errors) + check_pages.check_site_structure(documents, errors) + self.assertEqual(errors, []) + self.assertEqual((animations, statics), (9, 8)) + + def test_artifact_rejects_unknown_extension_and_wrong_hash(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + payload = root / "asset.png" + payload.write_bytes(b"not the declared bytes") + errors: list[str] = [] + with ( + mock.patch.object(check_pages, "NARRATIVE_ROOT", root), + mock.patch.object(check_pages, "NARRATIVE_MANIFEST", root / "manifest.json"), + ): + check_pages._artifact( + { + "path": "asset.webp", + "sha256": hashlib.sha256(b"asset").hexdigest(), + "media_type": "image/png", + }, + "test.extension", + errors, + ) + check_pages._artifact( + { + "path": "asset.png", + "sha256": hashlib.sha256(b"different").hexdigest(), + "media_type": "image/png", + }, + "test.hash", + errors, + ) + joined = "\n".join(errors) + self.assertIn("must end in .png or .gif", joined) + self.assertIn("disagrees with manifest", joined) + + def test_manifest_closes_identity_and_pdf_milestone_structure(self) -> None: + documents = _documents() + manifest = check_pages._load_manifest([]) + self.assertIsNotNone(manifest) + + invalid_identity = deepcopy(manifest) + invalid_identity["identities"]["tileset"] = "not-a-digest" + errors: list[str] = [] + with mock.patch.object(check_pages, "_load_manifest", return_value=invalid_identity): + check_pages.check_narrative_assets(documents, errors) + self.assertIn("identities.tileset is not a SHA-256", "\n".join(errors)) + + invalid_milestone = deepcopy(manifest) + invalid_milestone["pdf_milestones"]["reference_trace"] = ["../escape.png"] + errors = [] + with mock.patch.object(check_pages, "_load_manifest", return_value=invalid_milestone): + check_pages.check_narrative_assets(documents, errors) + self.assertIn("pdf_milestones.reference_trace has invalid paths", "\n".join(errors)) + + def test_incomplete_asset_records_report_controlled_diagnostics(self) -> None: + documents = _documents() + manifest = check_pages._load_manifest([]) + self.assertIsNotNone(manifest) + + for collection, name in ( + ("animations", "boolean_z3"), + ("statics", "home_preview"), + ): + with self.subTest(collection=collection, name=name): + invalid = deepcopy(manifest) + del invalid[collection][name]["owner"] + errors: list[str] = [] + with mock.patch.object(check_pages, "_load_manifest", return_value=invalid): + check_pages.check_narrative_assets(documents, errors) + self.assertIn( + f"{collection}.{name} is not closed", + "\n".join(errors), + ) + + def test_public_image_inventory_rejects_an_unowned_file(self) -> None: + with tempfile.TemporaryDirectory() as directory: + images = Path(directory) + (images / "tile-mark.svg").write_text("\n", encoding="utf-8") + (images / "orphan.svg").write_text("\n", encoding="utf-8") + errors: list[str] = [] + + check_pages.check_public_image_inventory(images, errors) + + self.assertIn( + "unexpected public image assets: orphan.svg", + "\n".join(errors), + ) + + def test_primary_asset_must_be_in_primary_animation_section(self) -> None: + original = check_pages.split_front_matter + target = check_pages.DOCS / "components/boolean-z3.md" + + def without_primary(path: Path, errors: list[str]) -> tuple[dict[str, str], str]: + metadata, body = original(path, errors) + if path == target: + body = body.replace("boolean_z3", "other") + return metadata, body + + errors: list[str] = [] + with mock.patch.object(check_pages, "split_front_matter", side_effect=without_primary): + check_pages.check_catalog(errors) + self.assertIn( + "primary asset 'boolean_z3' must use a narrative include in the Primary animation section", + "\n".join(errors), + ) + + def test_primary_asset_include_must_be_in_primary_animation_section(self) -> None: + original = check_pages.split_front_matter + target = check_pages.DOCS / "components/boolean-z3.md" + + def moved_include(path: Path, errors: list[str]) -> tuple[dict[str, str], str]: + metadata, body = original(path, errors) + if path == target: + include = next(check_pages.NARRATIVE_INCLUDE.finditer(body)).group(0) + body = body.replace(include, "", 1) + body = body.replace( + "## Mechanism\n", + f"## Mechanism\n\n{include}\n", + 1, + ) + return metadata, body + + errors: list[str] = [] + with mock.patch.object(check_pages, "split_front_matter", side_effect=moved_include): + check_pages.check_catalog(errors) + self.assertIn( + "primary asset 'boolean_z3' must use a narrative include in the Primary animation section", + "\n".join(errors), + ) + + def test_animation_include_roles_are_bound_to_the_manifest_record(self) -> None: + original = check_pages.split_front_matter + target = check_pages.DOCS / "components/boolean-z3.md" + + def swapped_roles(path: Path, errors: list[str]) -> tuple[dict[str, str], str]: + metadata, body = original(path, errors) + if path == target: + body = body.replace( + 'animation="/assets/narrative/boolean-z3/trace.gif" ' + 'fallback="/assets/narrative/boolean-z3/frame-02.png" ' + 'contact_sheet="/assets/narrative/boolean-z3/contact-sheet.png"', + 'animation="/assets/narrative/boolean-z3/contact-sheet.png" ' + 'fallback="/assets/narrative/boolean-z3/frame-02.png" ' + 'contact_sheet="/assets/narrative/boolean-z3/trace.gif"', + ) + return metadata, body + + errors: list[str] = [] + with mock.patch.object( + check_pages, "split_front_matter", side_effect=swapped_roles + ): + documents = check_pages.check_catalog(errors) + check_pages.check_narrative_assets(documents, errors) + + joined = "\n".join(errors) + self.assertIn("include argument 'animation'", joined) + self.assertIn("include argument 'contact_sheet'", joined) + + def test_animation_include_metadata_is_bound_to_the_manifest_record(self) -> None: + original = check_pages.split_front_matter + target = check_pages.DOCS / "components/reference-solver.md" + + def wrong_label(path: Path, errors: list[str]) -> tuple[dict[str, str], str]: + metadata, body = original(path, errors) + if path == target: + body = body.replace( + 'label="observed" caption=', + 'label="didactic" caption=', + ) + return metadata, body + + errors: list[str] = [] + with mock.patch.object( + check_pages, "split_front_matter", side_effect=wrong_label + ): + documents = check_pages.check_catalog(errors) + check_pages.check_narrative_assets(documents, errors) + + self.assertIn("include argument 'label'", "\n".join(errors)) + + def test_frozen_cross_links_must_use_relative_url(self) -> None: + documents = _documents() + worked = documents["/worked-example/"] + documents["/worked-example/"] = check_pages.Document( + worked.path, + worked.metadata, + worked.body.replace("'/components/boolean-z3/' | relative_url", "'/missing/' | relative_url"), + ) + errors: list[str] = [] + + check_pages.check_site_structure(documents, errors) + + self.assertIn( + "/worked-example/ does not link frozen route /components/boolean-z3/", + "\n".join(errors), + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/check_generated_pages.py b/tools/check_generated_pages.py index d22eb46..c7b9634 100644 --- a/tools/check_generated_pages.py +++ b/tools/check_generated_pages.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""Check semantics and internal targets in generated GitHub Pages HTML.""" +"""Check semantics, accessibility, and targets in generated Pages HTML.""" from __future__ import annotations @@ -12,42 +12,75 @@ from pathlib import Path from urllib.parse import unquote, urljoin, urlsplit +from check_pages import ( + ANIMATION_POLICY, + COMPONENT_HEADINGS, + COMPONENTS, + EXPECTED_BY_CLASS, + STATIC_POLICY, +) + ROOT = Path(__file__).resolve().parents[1] DEFAULT_CONFIG = ROOT / "docs/_config.yml" -REPRESENTATIVE_ROUTES = ( - "/", - "/development_principles/", - "/coverage_baseline_2026-08-22/", - "/historical_architecture/", -) +EXPECTED_ROUTE_CLASSES = { + route: page_class + for page_class, routes in EXPECTED_BY_CLASS.items() + for route in routes +} +EXPECTED_ROUTES = frozenset(EXPECTED_ROUTE_CLASSES) HOME_IDS = { "main-content", + "project-map", + "verified-output", "reading-path", - "documentation", - "cross-engine-benchmarks", } REFERENCE_ATTRIBUTES = { "a": "href", "img": "src", "link": "href", "script": "src", - "source": "src", + "source": "srcset", +} +NARRATIVE_ASSET_POLICY = { + **{name: (route, "animation") for name, (route, _) in ANIMATION_POLICY.items()}, + **{ + name: (route, "static") + for name, (route, _) in STATIC_POLICY.items() + if name != "presentation_status" + }, } +@dataclass +class Figure: + asset_id: str = "" + narrative_kind: str = "" + narrative_animation: bool = False + gif_images: list[tuple[str, str]] = field(default_factory=list) + reduced_sources: list[str] = field(default_factory=list) + contact_sheets: list[str] = field(default_factory=list) + captions: list[str] = field(default_factory=list) + + @dataclass class Page: path: Path route: str titles: list[str] = field(default_factory=list) h1s: list[str] = field(default_factory=list) + h2s: list[str] = field(default_factory=list) descriptions: list[str] = field(default_factory=list) canonicals: list[str] = field(default_factory=list) ids: set[str] = field(default_factory=set) classes: set[str] = field(default_factory=set) page_kinds: list[str] = field(default_factory=list) + page_classes: list[str] = field(default_factory=list) + component_ids: list[str] = field(default_factory=list) references: list[tuple[str, str]] = field(default_factory=list) + images: list[tuple[str, str, str, str]] = field(default_factory=list) + figures: list[Figure] = field(default_factory=list) + gifs_outside_figures: list[str] = field(default_factory=list) @dataclass(frozen=True) @@ -62,6 +95,7 @@ def __init__(self, page: Page) -> None: super().__init__(convert_charrefs=True) self.page = page self.capture: tuple[str, list[str]] | None = None + self.figure: Figure | None = None def handle_starttag( self, tag: str, attrs: list[tuple[str, str | None]] @@ -71,7 +105,7 @@ def handle_starttag( if values.get("id"): self.page.ids.add(values["id"]) self.page.classes.update(values.get("class", "").split()) - if tag in {"title", "h1"}: + if tag in {"title", "h1", "h2", "figcaption"}: self.capture = (tag, []) if tag == "meta" and values.get("name", "").lower() == "description": self.page.descriptions.append(values.get("content", "")) @@ -79,6 +113,45 @@ def handle_starttag( self.page.canonicals.append(values.get("href", "")) if tag == "body": self.page.page_kinds.append(values.get("data-page-kind", "")) + self.page.page_classes.append(values.get("data-page-class", "")) + component = values.get("data-component-id", "") + if component: + self.page.component_ids.append(component) + if tag == "figure": + classes = set(values.get("class", "").split()) + kinds = classes & {"narrative-animation", "narrative-static"} + self.figure = Figure( + asset_id=values.get("data-asset-id", ""), + narrative_kind=( + "animation" + if kinds == {"narrative-animation"} + else "static" + if kinds == {"narrative-static"} + else "" + ), + narrative_animation="narrative-animation" in kinds, + ) + self.page.figures.append(self.figure) + if tag == "img": + source = values.get("src", "") + alt = values.get("alt", "") + width = values.get("width", "") + height = values.get("height", "") + self.page.images.append((source, alt, width, height)) + if source.lower().endswith(".gif"): + if self.figure is None: + self.page.gifs_outside_figures.append(source) + else: + self.figure.gif_images.append((source, alt)) + if tag == "source" and self.figure is not None: + source = values.get("srcset", "") + media = values.get("media", "").lower() + if source.lower().endswith(".png") and "prefers-reduced-motion: reduce" in media: + self.figure.reduced_sources.append(source) + if tag == "a" and self.figure is not None: + href = values.get("href", "") + if "contact-sheet.png" in href: + self.figure.contact_sheets.append(href) attribute = REFERENCE_ATTRIBUTES.get(tag) if attribute and attribute in values: self.page.references.append((attribute, values[attribute])) @@ -93,11 +166,20 @@ def handle_data(self, data: str) -> None: self.capture[1].append(data) def handle_endtag(self, tag: str) -> None: - if self.capture and tag.lower() == self.capture[0]: + tag = tag.lower() + if self.capture and tag == self.capture[0]: text = " ".join("".join(self.capture[1]).split()) - target = self.page.titles if tag.lower() == "title" else self.page.h1s - target.append(text) + if tag == "title": + self.page.titles.append(text) + elif tag == "h1": + self.page.h1s.append(text) + elif tag == "h2": + self.page.h2s.append(text) + elif self.figure is not None: + self.figure.captions.append(text) self.capture = None + if tag == "figure": + self.figure = None def _route(root: Path, path: Path) -> str: @@ -128,6 +210,47 @@ def _error(errors: list[str], root: Path, page: Page, message: str) -> None: errors.append(f"{page.path.relative_to(root).as_posix()}: {message}") +def _check_narrative_asset_topology( + root: Path, pages: dict[str, Page], errors: list[str] +) -> None: + rendered: dict[str, list[tuple[Page, int, Figure]]] = {} + for page in pages.values(): + for index, figure in enumerate(page.figures, start=1): + if figure.asset_id: + rendered.setdefault(figure.asset_id, []).append((page, index, figure)) + elif figure.narrative_kind: + _error(errors, root, page, f"figure {index} lacks data-asset-id") + + for asset_id, (owner, expected_kind) in NARRATIVE_ASSET_POLICY.items(): + occurrences = rendered.pop(asset_id, []) + if not occurrences: + errors.append(f"missing narrative {expected_kind} asset {asset_id!r}") + continue + if len(occurrences) != 1: + errors.append( + f"narrative asset {asset_id!r} occurs {len(occurrences)} times; expected exactly once" + ) + continue + page, index, figure = occurrences[0] + if page.route != owner: + _error( + errors, + root, + page, + f"narrative asset {asset_id!r} is rendered on {page.route!r}, expected owner {owner!r}", + ) + if figure.narrative_kind != expected_kind: + _error( + errors, + root, + page, + f"narrative asset {asset_id!r} must be an {expected_kind} figure", + ) + for asset_id, occurrences in sorted(rendered.items()): + for page, index, _ in occurrences: + _error(errors, root, page, f"figure {index} has unexpected data-asset-id {asset_id!r}") + + def _check_semantics( root: Path, pages: dict[str, Page], @@ -135,7 +258,14 @@ def _check_semantics( baseurl: str, errors: list[str], ) -> None: - for page in pages.values(): + missing_routes = sorted(EXPECTED_ROUTES - pages.keys()) + extra_routes = sorted(pages.keys() - EXPECTED_ROUTES) + if missing_routes: + errors.append(f"missing generated routes: {', '.join(missing_routes)}") + if extra_routes: + errors.append(f"unexpected generated routes: {', '.join(extra_routes)}") + + for route, page in pages.items(): for label, values in ( ("H1", page.h1s), ("title", page.titles), @@ -151,10 +281,65 @@ def _check_semantics( page, f"expected canonical {expected!r}, found {page.canonicals!r}", ) + expected_class = EXPECTED_ROUTE_CLASSES.get(route) + if expected_class and page.page_classes != [expected_class]: + _error( + errors, + root, + page, + f"expected page class {expected_class!r}, found {page.page_classes!r}", + ) + if route in COMPONENTS: + component_id = COMPONENTS[route][0] + if page.component_ids != [component_id]: + _error( + errors, + root, + page, + f"expected component id {component_id!r}, found {page.component_ids!r}", + ) + if tuple(page.h2s) != COMPONENT_HEADINGS: + _error(errors, root, page, f"component H2 sequence is {page.h2s!r}") + elif page.component_ids: + _error(errors, root, page, f"unexpected component id {page.component_ids!r}") + for source, alt, width, height in page.images: + if not alt.strip(): + _error(errors, root, page, f"image {source!r} has empty alt text") + if "/assets/narrative/" in source: + try: + valid_dimensions = int(width) > 0 and int(height) > 0 + except ValueError: + valid_dimensions = False + if not valid_dimensions: + _error( + errors, + root, + page, + f"narrative image {source!r} lacks positive intrinsic dimensions", + ) + if page.gifs_outside_figures: + _error( + errors, + root, + page, + f"GIFs outside figures: {page.gifs_outside_figures!r}", + ) + for index, figure in enumerate(page.figures, start=1): + if not figure.narrative_animation and not figure.gif_images: + continue + if len(figure.gif_images) != 1: + _error(errors, root, page, f"figure {index} must contain exactly one GIF") + if len(figure.reduced_sources) != 1: + _error(errors, root, page, f"figure {index} requires one reduced-motion PNG srcset") + if len(figure.contact_sheets) != 1: + _error(errors, root, page, f"figure {index} requires one contact-sheet link") + if len(figure.captions) != 1 or not figure.captions[0]: + _error(errors, root, page, f"figure {index} requires one non-empty caption") + + _check_narrative_asset_topology(root, pages, errors) home = pages.get("/") if not home: - errors.append("missing generated homepage route '/'") return if home.titles != ["Tiling Foundry"]: _error(errors, root, home, f"unexpected home title {home.titles!r}") @@ -165,17 +350,10 @@ def _check_semantics( missing = sorted(HOME_IDS - home.ids) if missing: _error(errors, root, home, f"missing home IDs: {', '.join(missing)}") - required_classes = {"layout-reading", "layout-presentation", "home-catalog-section"} + required_classes = {"layout-reading", "layout-presentation", "home-section"} missing_classes = sorted(required_classes - home.classes) if missing_classes: - _error( - errors, - root, - home, - f"missing home layout classes: {', '.join(missing_classes)}", - ) - if "home-index" in home.classes: - _error(errors, root, home, "legacy home-index layout class is still rendered") + _error(errors, root, home, f"missing home layout classes: {', '.join(missing_classes)}") def _local_target( @@ -214,18 +392,30 @@ def _check_references( errors: list[str], ) -> int: pages_by_path = {page.path.resolve(): page for page in pages.values()} + gif_owners: dict[str, str] = {} count = 0 for page in pages.values(): for attribute, value in page.references: count += 1 + candidate_value = value.split()[0] if attribute == "srcset" else value try: - target = _local_target(value, page.route, site_url, baseurl) + target = _local_target(candidate_value, page.route, site_url, baseurl) except ValueError as error: _error(errors, root, page, f"{attribute}={value!r}: {error}") continue if target is None: continue path, fragment = target + if path.endswith(".gif"): + previous = gif_owners.get(path) + if previous is not None: + _error( + errors, + root, + page, + f"GIF {path!r} is already embedded by {previous!r}", + ) + gif_owners[path] = page.route disk = root / path.lstrip("/") if path.endswith("/") or disk.is_dir(): disk /= "index.html" @@ -246,9 +436,6 @@ def check_site(root: Path, *, site_url: str, baseurl: str) -> Result: pages = _load_pages(root, errors) if not pages: return Result(tuple(errors + [f"no HTML pages found under {root}"]), 0, 0) - for route in REPRESENTATIVE_ROUTES: - if route not in pages: - errors.append(f"missing representative route {route!r}") _check_semantics(root, pages, site_url, baseurl, errors) references = _check_references(root, pages, site_url, baseurl, errors) return Result(tuple(errors), len(pages), references) @@ -281,7 +468,7 @@ def main(argv: list[str] | None = None) -> int: return 1 print( f"Generated Pages checks passed: {result.page_count} HTML pages and " - f"{result.reference_count} href/src references validated." + f"{result.reference_count} href/src/srcset references validated." ) return 0 diff --git a/tools/check_pages.py b/tools/check_pages.py index 20053ed..10556aa 100644 --- a/tools/check_pages.py +++ b/tools/check_pages.py @@ -1,18 +1,25 @@ #!/usr/bin/env python3 -"""Validate the GitHub Pages document catalog without third-party packages.""" +"""Validate the authored GitHub Pages site and its canonical narrative assets.""" from __future__ import annotations import hashlib +import json import re +import shlex import sys +from collections import Counter, defaultdict +from dataclasses import dataclass from datetime import date from pathlib import Path ROOT = Path(__file__).resolve().parents[1] DOCS = ROOT / "docs" +NARRATIVE_ROOT = DOCS / "assets/narrative" +NARRATIVE_MANIFEST = NARRATIVE_ROOT / "manifest.json" +PUBLIC_CLASSES = {"story", "reference", "evidence", "history"} SECTIONS = { "Architecture and correctness", "Yang–Zhang reduction", @@ -20,11 +27,76 @@ "Cross-engine benchmarks", "Historical material", } -REQUIRED_FIELDS = { - "layout", - "title", - "permalink", - "description", +COMPONENT_HEADINGS = ( + "What it is", + "Why it exists", + "Inputs and outputs", + "Mechanism", + "Primary animation", + "Position in the pipeline", + "Observed example", + "Trust boundary", + "Artifacts and references", +) +COMPONENTS = { + "/components/tileset/": ("tileset", 1, "generalized_sheet"), + "/components/boolean-z3/": ("boolean-z3", 2, "boolean_z3"), + "/components/yang-zhang/": ("yang-zhang", 3, "region_construction"), + "/components/reference-solver/": ("reference-solver", 4, "reference_trace"), + "/components/optimized-solver/": ("optimized-solver", 5, "optimized_trace"), + "/components/wang-z3/": ("wang-z3", 6, "wang_z3"), + "/components/verification/": ("verification", 7, "verification"), + "/components/visualization/": ("visualization", 8, "witness_presentation"), +} +STORY_ROUTES = { + "/", + "/pipeline/", + "/worked-example/", + "/reference/", + "/evidence/", + *COMPONENTS, +} +REFERENCE_ROUTES = { + "/development_principles/", + "/reduction_notes/", + "/references/", + "/run-dossiers/", + "/serial_solver_implementation_guide/", + "/solver_comparison_benchmark/", + "/solver_performance_scope/", + "/wang-explainability-snapshots/", + "/wang-reduction-explanation/", + "/wang-solution-v1/", + "/wang-solver-trace/", + "/wang-square-to-hex/", + "/wang_z3_edge_table_2026-08-24/", + "/yang_zhang_builder_design/", + "/witness_correspondence/", +} +EVIDENCE_ROUTES = { + "/coverage_baseline_2026-08-22/", + "/parser_fuzz_smoke_2026-08-22/", + "/solver_byte_support_2026-08-20/", + "/solver_comparison_smoke_2026-08-21/", + "/solver_dynamic_stack_2026-08-17/", + "/solver_initial_trail_2026-08-17/", + "/solver_mrv_index_2026-08-28/", + "/solver_queue_dedup_2026-08-20/", + "/solver_queue_trail_profile_2026-08-20/", + "/solver_reference_profile_2026-08-17/", + "/solver_sat_ownership_2026-08-20/", +} +HISTORY_ROUTES = {"/historical_architecture/"} +EXPECTED_BY_CLASS = { + "story": STORY_ROUTES, + "reference": REFERENCE_ROUTES, + "evidence": EVIDENCE_ROUTES, + "history": HISTORY_ROUTES, +} +EXPECTED_ROUTES = set().union(*EXPECTED_BY_CLASS.values()) + +COMMON_FIELDS = {"layout", "title", "permalink", "description", "page_class"} +TECHNICAL_FIELDS = { "section", "document_kind", "status", @@ -40,14 +112,132 @@ RELATIVE_URL = re.compile( r"\{\{\s*['\"](?P/[^'\"]+)['\"]\s*\|\s*relative_url\s*\}\}" ) +NARRATIVE_INCLUDE = re.compile( + r"\{%\s*include\s+(?P