The image is downstream of an independently checked square witness. Read diff --git a/docs/plans/2026-08-31-narrative-migration-checklist.md b/docs/plans/2026-08-31-narrative-migration-checklist.md index 7510e5c..014c65b 100644 --- a/docs/plans/2026-08-31-narrative-migration-checklist.md +++ b/docs/plans/2026-08-31-narrative-migration-checklist.md @@ -1,6 +1,6 @@ # Narrative migration checklist -**Status:** frozen inventory and migration map +**Status:** inventory retained; implementation frozen through T98 on 11 September 2026 **Baseline:** `17edabc5c956cb6f00cbb19266b7701a04e30ee2` on 31 August 2026 @@ -8,8 +8,9 @@ This checklist applies the [narrative architecture contract](2026-08-31-narrative-architecture-contract.md) to every current public page, public Pages asset, dossier/schema contract, and -known excluded documentation source. Unchecked implementation actions belong -to later work; this inventory itself makes no public-site or asset change. +known excluded documentation source. The inventory below retains its original +baseline; completed implementation checks are bound to the T98 evidence in +section 13. This checklist itself makes no public-site or asset change. ## 1. Baseline audit @@ -161,14 +162,14 @@ checks prove the old files are unreferenced before deletion. - [x] `sat-end-to-end` and `unsat-search` have no initial-domain overrides; the two constrained diagnostic cases remain explicitly configured Wang solves rather than claims about the unconstrained formula. -- [ ] Keep v1 schema bytes/meaning and current cases compatible through every +- [x] Keep v1 schema bytes/meaning and current cases compatible through every v2 change. -- [ ] Keep v1 formatter/template isolated from v2; share only focused helpers +- [x] Keep v1 formatter/template isolated from v2; share only focused helpers behind thin dispatch. -- [ ] Keep v1 atomic destination install, isolated pdfLaTeX, no-shell-escape, +- [x] Keep v1 atomic destination install, isolated pdfLaTeX, no-shell-escape, run-specific timing identity, and diagnostic-UNSAT boundary. -- [ ] Run the existing SAT and all three UNSAT v1 dossier tests after each v2 - contract, asset, and PDF change. +- [x] Pass the existing SAT and all three UNSAT v1 dossier regressions on the + final v2 contract, asset, and PDF implementation. ## 8. Shared-asset migration order @@ -209,18 +210,18 @@ checks prove the old files are unreferenced before deletion. ## 10. V2 PDF implementation gates -- [ ] Follow the nine-section order frozen in the architecture contract. -- [ ] Consume the same validated facts and static assets as the captured v2 +- [x] Follow the nine-section order frozen in the architecture contract. +- [x] Consume the same validated facts and static assets as the captured v2 run; do not consume Pages HTML or Markdown. -- [ ] Embed no GIF/video and perform no second render or replay. -- [ ] Mark assignment, witness, verification, generalized witness, and hex +- [x] Embed no GIF/video and perform no second render or replay. +- [x] Mark assignment, witness, verification, generalized witness, and hex witness not applicable for UNSAT without fabricating a certificate. -- [ ] Keep raw timings in their named component sections and full detail in the +- [x] Keep raw timings in their named component sections and full detail in the appendix; make no general performance comparison. -- [ ] Compile with isolated, reproducible, no-shell-escape pdfLaTeX rules. -- [ ] Validate self-containment, hashes, source identity, component agreement, +- [x] Compile with isolated, reproducible, no-shell-escape pdfLaTeX rules. +- [x] Validate self-containment, hashes, source identity, component agreement, static-template inputs, and partial-failure cleanup. -- [ ] Prove v1 cases and output contracts remain compatible. +- [x] Prove v1 cases and output contracts remain compatible. ## 11. Excluded documentation sources @@ -242,13 +243,62 @@ checks prove the old files are unreferenced before deletion. and expected page class. - [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, +- [x] No GIF is duplicated, embedded by two owners, missing a static fallback, or included in a PDF. -- [ ] `pipeline_sat.cm13` identities agree across the worked example, all +- [x] `pipeline_sat.cm13` identities agree across the worked example, all engines, verification, presentation, Pages assets, and v2 dossier. -- [ ] `unsat-search` remains visibly and cryptographically separate. -- [ ] Removing documentation and explainability leaves core build, solve, +- [x] `unsat-search` remains visibly and cryptographically separate. +- [x] Removing documentation and explainability leaves core build, solve, oracles, verifier, and standard export functional. - [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. + +## 13. T98 implementation freeze — 11 September 2026 + +The presentation implementation is frozen at `f728bbd`, relative to the T97 +base `b921e7d`. Independent whole-branch review and scoped re-reviews closed +the two Important PDF findings: missing component-local oracle timings and +an orphaned hex caption. No Critical or Important finding remains. This is +a local implementation freeze; publication and later roadmap tasks are separate. + +The complete local closing matrix passed: `make check`, `pages-check`, strict +GCC/Clang, sanitizer, analyzer, Valgrind, Cachegrind, parser fuzz smoke (2,000 +runs), coverage, both dossier smoke targets and the locked renderer suite. +Final coverage execution passed all 17 C binaries and **199 Python tests**, +including all **33 v1/v2 dossier tests**; the renderer passed **324 tests**. +Sanitizer and fuzz required an authorized execution outside the ptrace sandbox +with leak detection retained. Memcheck completed all 17 binaries and three +benchmark invocations with zero errors/leaks; its interrupted run was resumed +at the remaining commands with unchanged recipe, source and build identities. +Coverage is informational; no timing or coverage threshold was introduced. + +Pages evidence covers 40 generated pages, 799 internal references and 48 +browser cases. All 171 inputs to that accepted build remained unchanged through +the final formatter correction; this subsequent checklist edit is excluded +from the site. Both final v2 PDFs contain static figures only: **23 SAT pages** +and **26 search-UNSAT pages**. Every page was inspected at normal reading scale. +The fresh final smoke preserves all 162 narrative images and 43 page rasters +byte-for-byte; the six pages changed by captured timing/environment text were +individually re-inspected. Figure/caption pagination is protected by +`V2FigurePaginationTests.test_wide_figure_keeps_its_caption_on_the_image_page`. + +The frozen-input v1 TeX, PDF and entire output tree remain byte-identical; +v1 schema/case bytes, formatter and template remain compatible. A disposable +export without downstream documentation/explainability consumers passed all +17 C binaries and 62 core Python tests. Core, ABI, independent oracles, schemas +and dependency locks are unchanged. Final diff, bounded secret scan, file-mode +and artifact checks found no unexpected tracked output or mode change. + +Four non-blocking limitations are retained under the stopping criteria: + +- The MRV summary covers redundant lower legend lines; its large decision + summary still shows the minimum domain, ties and row-major winner. +- Raster tests protect semantic values and summary cards more directly than + every candidate/winner grid color and displayed active-only count. +- Some redundant-signal labels crowd their boxes in the search-UNSAT routing + figures; signal IDs and routing order remain readable. +- The didactic ownership panel's `caller owns` label slightly exceeds its card + border in both PDFs; its meaning and neighboring values remain readable. + +These limitations introduce no additional visual work into the frozen phase. diff --git a/docs/plans/2026-09-05-t98-visual-documentation.md b/docs/plans/2026-09-05-t98-visual-documentation.md new file mode 100644 index 0000000..70e2bcb --- /dev/null +++ b/docs/plans/2026-09-05-t98-visual-documentation.md @@ -0,0 +1,742 @@ +# T98 Visual Documentation, PDF v2 and README Routing Implementation 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:** Improve the existing narrative assets until they explain the real +algorithms clearly, compose readable static figures into a run-specific v2 +PDF, and route README readers into the canonical Pages documentation. + +**Architecture:** Rework the current named asset bundles in place from the +same validated run artifacts. Keep `wang-narrative-assets-v1`, the existing +owner routes, and the single validator/replay/compositor chain; use focused +observed frames or compact static panels instead of adding a visual framework. +Add a separate pure v2 TeX formatter and template while preserving the v1 +dossier exactly. + +**Tech Stack:** C17, Python 3.14, Pillow and NumPy through the locked renderer +environment, existing closed JSON contracts, Markdown/Jekyll, Liquid, +HTML/CSS, LaTeX/pdfLaTeX, `uv`, Make, Docker and Playwright. + +**Spec:** `docs/plans/2026-08-31-narrative-architecture-contract.md` + +## Global Constraints + +- Base all work on `origin/main` merge commit `b921e7d` or a verified + descendant containing the identical T97 tree. +- Preserve the current public permalinks, sitemap, and nine component-page H2 + sections. Do not deepen these editorial conventions into new architecture. +- Keep `tests/instances/pipeline_sat.cm13` as the sole canonical SAT narrative + and `tests/instances/pipeline_unsat_search.cm13` as a separately named + search diagnostic. +- Preserve reference and optimized solver behavior, native ABI, traces, + metrics, ownership and deterministic outputs. T98 changes no solver logic. +- Pages and PDF consume previously validated artifacts. Neither path may solve, + invoke Z3, rebuild the reduction, or independently verify a witness. +- Keep `wang-narrative-assets-v1`. The planned implementation adds no schema, + manifest version, generic asset registry, intermediate representation or + validator layer. +- If a required correctness claim cannot be represented by the current asset + boundary without a false owner, semantic label or source identity, stop the + affected task and report the concrete counterexample before changing a + contract. +- Treat visual requirements as reader outcomes, not a one-to-one list of + animations, modules or assets. Prefer static panels where time adds no + information. +- Visual quality is itself an acceptance criterion. Semantic correctness does + not justify retaining an existing GIF or image that is blurry, + low-resolution, hard to read, overly compressed or visually weak at its + actual Pages or PDF display size; regenerate, improve or replace it. +- MRV is the vertical slice that establishes the visual grammar, not the limit + of the rework. Apply the graphical-explanation requirement to every relevant + algorithm or technical mechanism, choosing the clearest static figure, + multi-panel sequence, comparison, observed state or animation. Animated + flowcharts and boxes that merely light up remain suitable for architecture + or pipeline views, but are not an adequate primary algorithm explanation + when the reader needs to see actual state, transformation, decisions or + data-structure behavior. +- Retain observed reference and optimized traces as evidence, including their + complete/selected/truncated semantics. A displayed subset never means trace + events were omitted from the source. +- Preserve the five asset labels: `observed`, `canonical-construction`, + `encoding-order`, `verified-transformation` and `didactic`. +- Keep the existing renderer modules unless an actual responsibility boundary + becomes unmanageable during implementation. Do not perform the proposed + file split mechanically. +- Render important raster figures at 2x source scale; do not enlarge existing + small bitmaps. Use 3x only after a visual comparison proves a benefit. +- Use `NEAREST` only for intentionally discrete pixel/block content. Use a + high-quality filter for text-heavy or presentation downsampling. +- Every animation keeps a meaningful static fallback and contact sheet. Every + important visual keeps adjacent alt text and a useful caption. +- Keep dossier v1 schemas, case semantics, formatter, output layout and CLI + behavior compatible. V2 remains an additive dispatch path. +- Do not implement profiling, `TaskPlan`, OpenMP, native JSON, another solver + optimization or a generalized presentation framework. +- Stop when the acceptance story is clear at desktop, 390 px and normal PDF + zoom. Do not add variants without a concrete consumer. + +## Existing Asset Disposition + +The implementation reuses these current records instead of adding asset IDs: + +| Existing record | T98 role | +|---|---| +| `reference_trace` | Observed MRV, propagation, decision, conflict and rollback states; complete trace remains evidence | +| `optimized_trace` | Observed optimized run using the same visual grammar | +| `optimized_mechanisms` | Compact didactic panels for the six retained mechanisms | +| `region_construction` | Source/target signals, adjacent swaps, one crossover, assembly and boundaries | +| `boolean_z3` | Project-owned formula-to-constraint order only | +| `wang_z3` | Project-owned finite-region edge and tile encoding only | +| `verification` | Receipt summary, tiling checks and witness extraction from already verified artifacts | +| `witness_presentation` | Square to generalized to checked-hex relationship | +| existing statics | Formula, tile vocabulary, worked example and final presentation quality pass | + +The current animation `frames`, `fallback`, `contact_sheet` and +`pdf_milestones` fields carry the print-ready panels. A frame remains within +the parent record's owner and semantic label; do not mix didactic content into +an `observed` record unless every displayed fact is derived from the validated +observed state. + +--- + +### Task 1: Freeze the visual grammar with an MRV vertical slice + +**Files:** + +- Modify: `renderer/wang_explain.py` +- Modify: `renderer/wang_trace_render.py` +- Test: `renderer/test_wang_trace.py` +- Generate only for review: a temporary `reference_trace` bundle outside Git + +**Interfaces:** + +- Consumes: `TraceBundle`, `TraceEvent` and states returned by + `replay_trace()` from `tests/fixtures/pipeline_sat_solver_trace/manifest.json`. +- Produces: the existing `render_trace_assets(...) -> AnimationOutputs` + interface with 2x source frames and an observed MRV decision frame. +- Adds no data model. MRV candidates are derived locally from active replayed + domains and discarded after composition. + +- [ ] **Step 1: Add a failing deterministic MRV test** + + Extend `renderer/test_wang_trace.py` with a test that loads the SAT trace, + finds the first search decision, computes the minimum unresolved domain size + from the replayed pre-decision state, and proves that the event cell is the + lowest row-major member of the tied candidate set. Render twice and assert + identical trees plus a physical fallback size of `1976 x 828` for the + logical `988 x 414` display. + + ```python + candidates = tuple( + index + for index, (active, domain) in enumerate(zip(region.active, before)) + if active and domain.bit_count() == minimum + ) + assert event.cell == min(candidates) + assert _tree_bytes(first_dir) == _tree_bytes(second_dir) + assert Image.open(first.fallback).size == (1976, 828) + ``` + +- [ ] **Step 2: Prove the new test fails for the current 1x output** + + Run: + + ```bash + cd renderer + uv run --locked pytest -q test_wang_trace.py -k 'mrv or deterministic' + ``` + + Expected: the new dimension assertion fails while existing semantic tests + remain green. + +- [ ] **Step 3: Add only the shared primitives needed by the prototype** + + Keep one render-scale constant and consistent treatments for unresolved, + singleton, selected MRV, propagation source/target, queued, decision, + conflict, trail mutation and restored state. Scale coordinates, fonts and + strokes at source; do not render at 1x and resize. + +- [ ] **Step 4: Compose the observed MRV explanation** + + In the decision frame show domain sizes, all minimum candidates, the + row-major winner and the selected cell. The side panel must expose values + derived from the replayed state, not hard-coded fixture numbers. + +- [ ] **Step 5: Verify focused tests and inspect the prototype** + + Run: + + ```bash + cd renderer + uv run --locked pytest -q test_wang_trace.py + ``` + + Generate to a `mktemp -d` destination and inspect the fallback and contact + sheet at original resolution. At intended `988 px` display width, domain + sizes and the tie-break statement must be readable without zoom. + +- [ ] **Step 6: Apply the stop rule** + + If desktop, 390 px and one-column PDF-size previews are readable, freeze the + grammar. Do not add themes, layout engines, vector backends or alternate MRV + variants. + +- [ ] **Step 7: Commit the vertical slice** + + ```bash + git add renderer/wang_explain.py renderer/wang_trace_render.py \ + renderer/test_wang_trace.py + git commit -m "Explain observed MRV selection clearly" + ``` + +### Task 2: Complete solver behavior and retain trace evidence + +**Files:** + +- Modify: `renderer/wang_trace_render.py` +- Test: `renderer/test_wang_trace.py` +- Test: `tests/python/test_multi_engine_dossier.py` +- Modify metadata only when wording changes: + `python/dossier/narrative_assets.py` + +**Interfaces:** + +- Consumes: the existing complete SAT reference/optimized traces and the + separately captured `examples/run-cases-v2/pipeline-unsat-search.json` run. +- Produces: focused observed sequences within `reference_trace` and + `optimized_trace`; the manifest shape and trace sources remain unchanged. + +- [ ] **Step 1: Add failing sequence-selection tests** + + Test that the SAT selection contains a real restriction, decision and + continuation, and that the separate search-UNSAT selection contains a + decision, propagation reduction, empty-domain conflict and reverse rollback + in source-event order. Assert the run-specific UNSAT manifest caption names + it an `observed search diagnostic` and states that it is + `not an UNSAT certificate`. + +- [ ] **Step 2: Run the focused tests and confirm the missing story** + + ```bash + cd renderer + uv run --locked pytest -q test_wang_trace.py + ``` + + Expected: new story assertions fail against the current generic milestone + composition. + +- [ ] **Step 3: Make propagation causal rather than decorative** + + For a real domain-reduction event show the restricted source, inspected + neighbor, removed candidate domain bits, shared-edge support reason and + resulting state. Use existing tile/domain data; do not introduce another + compatibility implementation. Do not present queue order as observed because + the current trace contract does not record it; queue behavior belongs to the + didactic optimized-mechanism bundle. + +- [ ] **Step 4: Make DFS and rollback visible in the same observed grammar** + + Show selected cell, candidate branch, depth, conflict, trail mark, reverse + restoration and next branch. Keep the grid primary and use only a compact + search-tree inset. + +- [ ] **Step 5: Preserve evidence semantics** + + Keep the original event sequence, complete trace identity and selected-frame + semantics. Assert generated manifests retain `semantic_label: observed`, + `complete: true`, `selected: true` and `truncated: false` for the canonical + trace bundles. + +- [ ] **Step 6: Run solver-renderer and dossier tests** + + ```bash + cd renderer + uv run --locked pytest -q test_wang_trace.py + cd .. + PYTHONPATH="$PWD/python" uv run --frozen python -m unittest \ + tests.python.test_multi_engine_dossier + ``` + +- [ ] **Step 7: Commit the focused observed trace story** + + ```bash + git add renderer/wang_trace_render.py renderer/test_wang_trace.py \ + python/dossier/narrative_assets.py \ + tests/python/test_multi_engine_dossier.py + git commit -m "Explain propagation and rollback from observed traces" + ``` + +### Task 3: Explain the reduction and local tile compatibility + +**Files:** + +- Modify: `renderer/wang_algorithm_animation.py` +- Modify: `renderer/wang_narrative.py` +- Test: `renderer/test_wang_algorithm_animation.py` +- Test: `renderer/test_wang_narrative.py` + +**Interfaces:** + +- Consumes: the validated reduction provenance already exposed by + `load_explainability_bundle()` and the canonical tile table. +- Produces: the existing `region_construction` frame sequence plus an improved + `atomic_legend`; no new asset record is added. + +- [ ] **Step 1: Add failing construction-content tests** + + Assert that rendered stages are byte-stable and sourced from the fixture's + exact `source_signals`, `target_signals`, adjacent-swap provenance and one + actual crossover. Assert the final construction panel distinguishes active, + inactive, exposed-boundary and internal edges. + +- [ ] **Step 2: Add a failing local-compatibility test** + + Render one valid and one invalid adjacency using actual canonical tile IDs. + Assert the shared colors agree in the valid example and differ in the + invalid example before checking output bytes and dimensions. + +- [ ] **Step 3: Implement the smallest coherent construction sequence** + + Use a few frames to show source versus target order, actual adjacent swaps, + one crossover, final region assembly and boundaries. Keep the existing + gadget-span view as provenance support rather than adding a second bundle. + +- [ ] **Step 4: Fold tile compatibility into the current vocabulary output** + + Add the valid/invalid adjacency panel to `atomic_legend` or the current tile + sheet, whichever remains readable at normal width. Do not create a new + manifest entry for it. + +- [ ] **Step 5: Run focused renderer tests** + + ```bash + cd renderer + uv run --locked pytest -q \ + test_wang_algorithm_animation.py test_wang_narrative.py + ``` + +- [ ] **Step 6: Commit the reduction explanation** + + ```bash + git add renderer/wang_algorithm_animation.py renderer/wang_narrative.py \ + renderer/test_wang_algorithm_animation.py renderer/test_wang_narrative.py + git commit -m "Explain Yang-Zhang routing and tile compatibility" + ``` + +### Task 4: Replace the optimized mechanism list with concrete panels + +**Files:** + +- Modify: `renderer/wang_algorithm_animation.py` +- Modify only if factual copy changes: + `renderer/data/optimized-mechanisms-v1.json` +- Test: `renderer/test_wang_algorithm_animation.py` +- Modify metadata only when wording changes: + `python/formats/narrative_assets.py` + `python/dossier/narrative_assets.py` + +**Interfaces:** + +- Consumes: the existing six-mechanism source and current implementation + semantics documented by their evidence pages. +- Produces: the existing `optimized_mechanisms` bundle with concrete didactic + panels and no benchmark claims. + +- [ ] **Step 1: Add failing mechanism-panel tests** + + Assert byte stability and the presence of exactly the six retained mechanism + IDs. Verify the lazy-MRV panel uses domain-size buckets and reverses one + bucket update during rollback; verify queue dedup permits a later enqueue + after dequeue. + +- [ ] **Step 2: Implement static comparisons where motion adds nothing** + + Use compact before/after panels for dynamic stack capacity, initial-trail + omission and SAT ownership transfer. Show the reference behavior beside the + optimized behavior without performance numbers. + +- [ ] **Step 3: Implement the stateful explanations** + + Show actual 23-bit byte-support aggregation, duplicate suppression while a + cell is pending, and the lazy-MRV bucket/index update and rollback. State + `domains = semantic source of truth` and `MRV index = private derived state`. + +- [ ] **Step 4: Stop at one owned bundle** + + Use frames and its static contact/fallback output; do not create six asset + records, six renderer modules or a mechanism plugin system. + +- [ ] **Step 5: Run focused tests and commit** + + ```bash + cd renderer + uv run --locked pytest -q test_wang_algorithm_animation.py + cd .. + git add renderer/wang_algorithm_animation.py \ + renderer/data/optimized-mechanisms-v1.json \ + renderer/test_wang_algorithm_animation.py \ + python/formats/narrative_assets.py python/dossier/narrative_assets.py + git commit -m "Show the optimized serial mechanisms concretely" + ``` + +### Task 5: Explain the two encodings, verification and witness extraction + +**Files:** + +- Modify: `renderer/wang_z3_summary.py` +- Modify: `renderer/wang_narrative.py` +- Modify: `python/dossier/narrative_assets.py` +- Modify: `python/formats/narrative_assets.py` +- Test: `renderer/test_wang_z3_summary.py` +- Test: `renderer/test_wang_narrative.py` +- Test: `tests/python/test_multi_engine_dossier.py` + +**Interfaces:** + +- Consumes: existing `z3-encoding-summary-v1` documents, the existing + explainability bundle, verified solution and v2 verification records. +- Produces: reworked existing `boolean_z3`, `wang_z3`, `verification` and + `witness_presentation` bundles. No renderer imports Z3 or native producers. + +- [ ] **Step 1: Add failing oracle-composition tests** + + Boolean frames must show real source clauses becoming `ExactlyOne` terms in + source order and the copied SAT assignment. Wang frames must show a real + active cell, shared internal term, canonical tile tuple, exposed boundary + equality and returned model projection. Both must display that they do not + expose Z3 internal search. + +- [ ] **Step 2: Add failing verifier and extraction tests** + + Validate that the receipt summary names the six existing checks, the tiling + panel shows valid tile IDs, `TILE_NONE`, internal equality and boundary + equality, and the extraction view places real variable-gadget cells beside + the already recorded extracted Boolean assignment and independent checker + result. The renderer must not recompute or decide that assignment. + +- [ ] **Step 3: Rework the Z3 frames from existing summaries** + + Improve geometry and typography without adding fields to + `z3-encoding-summary-v1` or implying internal Z3 decisions. + +- [ ] **Step 4: Rework verification from existing validated inputs** + + Pass the existing explainability manifest/solution alongside the current + verification receipts when composing the bundle. Reuse its loaders and + identities; do not create a verification-story JSON contract. + +- [ ] **Step 5: Update source identity only if the consumed identity set grows** + + If verification frames consume provenance and a verified solution, include + those existing hashes in `verification_source_sha256()`. Keep the manifest + field structure and semantic policy unchanged. + +- [ ] **Step 6: Run focused tests and import-boundary checks** + + ```bash + cd renderer + uv run --locked pytest -q test_wang_z3_summary.py test_wang_narrative.py + cd .. + PYTHONPATH="$PWD/python" uv run --frozen python -m unittest \ + tests.python.test_multi_engine_dossier + ``` + +- [ ] **Step 7: Commit the oracle and verification explanation** + + ```bash + git add renderer/wang_z3_summary.py renderer/wang_narrative.py \ + renderer/test_wang_z3_summary.py renderer/test_wang_narrative.py \ + python/dossier/narrative_assets.py python/formats/narrative_assets.py \ + tests/python/test_multi_engine_dossier.py + git commit -m "Explain oracle encodings and witness verification" + ``` + +### Task 6: Compose the additive v2 PDF without another semantic pass + +**Files:** + +- Create: `python/formats/run_report_v2_tex.py` +- Create: `templates/run-report-v2.tex` +- Create only for the shared TeX security boundary: + `python/dossier/tex_compile.py` +- Modify: `python/dossier/multi_engine.py` +- Modify: `tools/generate_run_dossier.py` +- Modify: `Makefile` +- Test: `tests/python/test_multi_engine_dossier.py` +- Test: `tests/python/test_run_dossier.py` + +**Interfaces:** + +- Produces: + `render_run_report_v2_tex(document: dict[str, object], + manifest: dict[str, object], template: str) -> str`. +- The v2 formatter validates the existing run and narrative manifest, selects + only their static artifacts/milestones and returns TeX. It performs no I/O + other than its caller reading the validated inputs. +- `tex_compile.py` owns the existing `-no-shell-escape`, restricted TeX home, + `SOURCE_DATE_EPOCH`, two-pass compilation and cleanup behavior. V1 and v2 + callers translate its single controlled error into their existing public + error types. + +- [ ] **Step 1: Freeze v1 behavior with focused tests** + + Add assertions that a v1 case still dispatches to the v1 formatter, keeps + its filenames/layout, rejects v2-only options and produces deterministic + TeX/PDF from the existing smoke case. + +- [ ] **Step 2: Add failing pure v2 formatter tests** + + For SAT, assert section order is summary, source, Boolean Z3, Yang--Zhang, + reference, optimized, Wang Z3, verification/presentation, reproducibility. + For UNSAT, assert witness-only figures are absent and explicitly not + applicable. Assert no trace contact sheet is used as the primary solver + figure. + +- [ ] **Step 3: Add explicit figure layouts** + + Implement small helpers local to `run_report_v2_tex.py` for wide, + multi-panel, tall and compact figures. Do not add a generic report layout + framework. Every helper emits a fixed `\includegraphics` policy appropriate + to its consumer. + +- [ ] **Step 4: Implement the v2 formatter and template** + + Read source text and validated values directly from the existing dossier; + use `pdf_milestones` and static artifacts for figures. Keep raw timings and + hashes in the reproducibility appendix and never infer semantic results from + pixels. + +- [ ] **Step 5: Share only the TeX compilation security boundary** + + Move the current isolated compilation behavior without changing v1 output. + Invoke it inside the v2 staging directory before the atomic install so a + TeX failure leaves no partial destination. + +- [ ] **Step 6: Add and run SAT/UNSAT PDF smoke** + + Add `run-dossier-v2-smoke` rather than making `run-dossier-smoke` silently + change meaning. + + ```bash + make run-dossier-smoke + make run-dossier-v2-smoke + PYTHONPATH="$PWD/python" uv run --frozen python -m unittest \ + tests.python.test_run_dossier tests.python.test_multi_engine_dossier + ``` + +- [ ] **Step 7: Commit the additive v2 report path** + + ```bash + git add python/formats/run_report_v2_tex.py templates/run-report-v2.tex \ + python/dossier/tex_compile.py python/dossier/multi_engine.py \ + tools/generate_run_dossier.py Makefile tests/python/test_run_dossier.py \ + tests/python/test_multi_engine_dossier.py + git commit -m "Compose readable static v2 run reports" + ``` + +### Task 7: Publish the improved assets through Pages and README + +**Files:** + +- Modify: `README.md` +- Modify: `docs/worked-example.md` +- Modify as required by changed figures: `docs/components/*.md` +- Modify only for responsive presentation: `docs/assets/css/site.css` +- Modify only if current includes cannot present the existing fallback cleanly: + `docs/_includes/narrative-animation.html` + `docs/_includes/narrative-static.html` +- Modify minimally if asset topology changes: + `tools/check_pages.py` + `tools/check_generated_pages.py` + `tests/python/test_pages_checker.py` + `tests/python/test_generated_pages.py` +- Regenerate from one canonical capture: `docs/assets/narrative/` + +**Interfaces:** + +- Consumes: one freshly validated canonical SAT v2 run and the current + `wang-narrative-assets-v1` generator. +- Produces: byte-identical run-specific/canonical compositor files, authored + Pages prose and README routing. Pages build remains render-free. + +- [ ] **Step 1: Add only tests required by actual integration changes** + + Preserve one primary owner and existing accessibility/link checks. If no + asset ID or include contract changes, do not add checker abstractions. Add a + regression only for a concrete failure such as swapped fallback roles, + missing intrinsic dimensions or horizontal overflow metadata. + +- [ ] **Step 2: Regenerate the canonical bundle from one clean capture** + + ```bash + T98_ASSET_TMP=$(mktemp -d /tmp/tiling-foundry-t98-assets.XXXXXX) + PYTHONPATH="$PWD/python" uv run --frozen python \ + tools/generate_run_dossier.py \ + examples/run-cases-v2/pipeline-sat.json "$T98_ASSET_TMP/run" + PYTHONPATH="$PWD/python" uv run --frozen python \ + tools/generate_narrative_assets.py \ + "$T98_ASSET_TMP/run/run.json" "$T98_ASSET_TMP/pages" \ + --product canonical-pages + rsync -a --delete "$T98_ASSET_TMP/pages/" docs/assets/narrative/ + ``` + + Validate the temporary manifest before replacing tracked output. Copy the + complete generated tree as one unit so file hashes and manifest cannot drift. + +- [ ] **Step 3: Place visuals next to the prose they explain** + + Keep the nine H2 sections. Focused visuals appear before the observed trace + evidence where both are present; avoid appending an asset gallery or + duplicating component explanations in the worked example. + +- [ ] **Step 4: Improve the worked example and final presentations** + + Keep the overview storyboard, but make formula, construction decision, + verified square witness, interpretation and final presentation readable at + useful sizes. Improve source resolution/downsampling without redesigning the + square/generalized/hex relationship. + +- [ ] **Step 5: Clean README routing and stale status** + + Add one prominent line linking Documentation, Pipeline, Worked example, + Reference, Evidence and Run dossiers. Retain project statement, scope, + quickstart, status, architecture, limitations, reference and license; reduce + duplicated algorithm narrative and remove rapidly stale exact test counts. + +- [ ] **Step 6: Build and validate Pages offline** + + ```bash + T98_PAGES_BUILD=$(mktemp -d /tmp/tiling-foundry-t98-pages.XXXXXX) + docker run --rm --network none --user 1000:1000 \ + -e GITHUB_WORKSPACE=/github/workspace \ + -e INPUT_SOURCE=docs -e INPUT_DESTINATION=build/pages \ + -e INPUT_VERBOSE=false -e INPUT_FUTURE=false \ + -e GITHUB_REPOSITORY=xtraid/tiling-foundry \ + -e GITHUB_API_URL=https://api.github.com -e INPUT_TOKEN= \ + -e INPUT_BUILD_REVISION="$(git rev-parse HEAD)" \ + -v "$PWD:/github/workspace:ro" \ + -v "$T98_PAGES_BUILD:/github/workspace/build/pages" \ + ghcr.io/actions/jekyll-build-pages:v1.0.13 + python3 tools/check_generated_pages.py "$T98_PAGES_BUILD" + ``` + +- [ ] **Step 7: Perform browser QA with the local Playwright image** + + Serve the external build locally and use + `mcr.microsoft.com/playwright:v1.62.0-noble` to inspect `/`, `/pipeline/`, + `/worked-example/` and all eight component routes at desktop and `390 px`. + Record screenshots outside Git. Check overflow, label readability, + reduced-motion fallback, stable aspect ratio, captions, focus and links. + +- [ ] **Step 8: Run Pages and renderer regressions, then commit** + + ```bash + make pages-check + cd renderer + uv run --locked pytest -q + cd .. + git add README.md docs tools/check_pages.py tools/check_generated_pages.py \ + tests/python/test_pages_checker.py tests/python/test_generated_pages.py + git commit -m "Route readers through publication-quality documentation" + ``` + +### Task 8: Inspect PDFs, run the complete closing gates and freeze T98 + +**Files:** + +- Review: complete `origin/main...HEAD` diff +- Modify only for evidence accuracy: + `docs/plans/2026-08-31-narrative-migration-checklist.md` +- Record task evidence under: `.superpowers/sdd/2026-09-05-t98-visual-documentation/` + +**Interfaces:** + +- Consumes: final SAT and search-UNSAT v2 dossiers plus the externally built + Pages site. +- Produces: reviewed publication output and a frozen presentation phase. It + does not begin T99, profiling, `TaskPlan` or OpenMP. + +- [ ] **Step 1: Inspect SAT and search-UNSAT PDFs at normal reading scale** + + ```bash + T98_PDF_QA=$(mktemp -d /tmp/tiling-foundry-t98-pdf.XXXXXX) + pdfinfo build/run-dossier-v2-sat/report.pdf + pdftoppm -png -r 144 build/run-dossier-v2-sat/report.pdf \ + "$T98_PDF_QA/sat" + pdfinfo build/run-dossier-v2-unsat-search/report.pdf + pdftoppm -png -r 144 build/run-dossier-v2-unsat-search/report.pdf \ + "$T98_PDF_QA/unsat" + ``` + + Inspect every rendered page. Reject pixelation, crushed wide figures, tiny + labels, overflow, broken whitespace, SAT-only witness figures in UNSAT, or + any description of a failed leaf as a certificate. + +- [ ] **Step 2: Run the complete repository closing matrix** + + ```bash + make check + make pages-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 + make run-dossier-v2-smoke + cd renderer + uv run --locked pytest -q + ``` + +- [ ] **Step 3: Review documentation ownership and duplication** + + Confirm README answers what the project is and how to enter it; Pages + explains how it works; reference defines contracts; evidence records + measurements; each PDF reports one captured run. Consolidate repeated + multi-paragraph explanations rather than maintaining copies. + +- [ ] **Step 4: Perform publication hygiene checks** + + ```bash + git diff --check origin/main...HEAD + git status --short --branch + git diff --summary origin/main...HEAD + git ls-files build .uv-cache .venv renderer/.venv + ``` + + Confirm no build output, screenshots, caches, credentials, private keys or + unexpected executable modes are tracked. + +- [ ] **Step 5: Obtain independent whole-branch review** + + Review the complete diff against this plan and the primary spec. Resolve all + Critical and Important findings with a focused test-first correction and a + scoped re-review. + +- [ ] **Step 6: Record the freeze and stop** + + Update only checklist items proven by the final evidence. Record remaining + minor visual issues separately; do not add another visual merely because it + is possible. Commit the evidence update with a result-oriented subject. + + ```bash + git add docs/plans/2026-08-31-narrative-migration-checklist.md \ + .superpowers/sdd/2026-09-05-t98-visual-documentation + git commit -m "Freeze the verified T98 presentation layer" + ``` + +## Definition of Done + +T98 is complete only when concrete visuals explain reduction routing, local +tile compatibility, propagation, MRV/tie-breaking, DFS, conflict, rollback, +the six optimized mechanisms, both project-owned Z3 encodings, tiling checks +and Boolean witness extraction; observed traces remain available as evidence; +SAT and search-UNSAT identities remain separate; Pages and PDFs are readable +at their intended sizes; v1 dossier behavior is unchanged; every required gate +is green; and no profiling, `TaskPlan` or OpenMP work has entered the branch. diff --git a/docs/run_dossiers.md b/docs/run_dossiers.md index 7b59c73..07acab1 100644 --- a/docs/run_dossiers.md +++ b/docs/run_dossiers.md @@ -149,9 +149,30 @@ records an explicit not-applicable panel and never fabricates a witness or certificate. The separate example is versioned at `examples/run-cases-v2/pipeline-unsat-search.json`. -No v2 PDF is produced yet. Its later formatter will consume only the validated -static milestone PNGs already named by the asset manifest, without solving, -checking, replaying, or rendering again. +The default v2 command stops after the validated capture and shared assets. It +does not import the LaTeX formatter, invoke a TeX compiler, or produce +`report.tex` and `report.pdf`. With pdfLaTeX available, add `--pdf` when a +static report is wanted: + +```sh +make shared +uv run --frozen python tools/generate_run_dossier.py \ + examples/run-cases-v2/pipeline-sat.json \ + build/run-dossiers/pipeline-sat-v2-pdf \ + --pdf +``` + +The v2 formatter consumes only the validated `run.json` and static PNGs already +named by the asset manifest. It does not solve, invoke Z3, verify, replay, or +render again. SAT reports include the checked witness presentations; +search-UNSAT reports mark witness-only sections not applicable and do not +invent a certificate. + +The opt-in compiler uses the same isolated, no-shell-escape execution and +private TeX state as v1. TeX and PDF files are staged with the complete dossier +and installed atomically; compilation failure leaves no partial destination. +The v1 command, formatter, output shape, and `--tex-engine` behavior remain +unchanged. All v2 durations use one monotonic nanosecond clock and are labelled `run-specific-observation-not-a-benchmark`. They are raw facts about that diff --git a/docs/worked-example.md b/docs/worked-example.md index 5636397..2addc6d 100644 --- a/docs/worked-example.md +++ b/docs/worked-example.md @@ -14,7 +14,11 @@ This page follows only `tests/instances/pipeline_sat.cm13`. Its SHA-256 is 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" %} +{% include narrative-static.html asset_id="worked_example" image="/assets/narrative/pipeline-overview/worked-example.png" alt="An eight-stage overview followed by enlarged Boolean decision, Yang-Zhang construction, six verification receipts, verified square witness, and checked hex presentation panels." width="1080" height="3440" label="observed" caption="Eight-stage overview with readable decision, construction, verification, square-witness, and checked-hex details." source="wang-run-dossier-v2#named-components" %} + +The opening grid is the component map. The enlarged panels retain the captured +decision, construction, checker interpretation, square witness, and final hex +view at a useful reading size; the component pages own their full explanations. ## Source formula @@ -26,19 +30,20 @@ source bytes; it is not reconstructed from a later tiling. ## 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. +The enlarged decision panel shows the copied Boolean model; the construction +panel shows the source-to-target signal order and final region vocabulary. +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 enlarged receipt panel distinguishes the six named checks and the copied +native extraction. Only after those checks does the presentation layer render +the enlarged square witness, recognize exact generalized contours, and apply +the checked square-to-hex mapping shown in the final panel. The milestone sequence links to the owned explanations for the [tileset]({{ '/components/tileset/' | relative_url }}), diff --git a/python/dossier/multi_engine.py b/python/dossier/multi_engine.py index 8e3413c..a529460 100644 --- a/python/dossier/multi_engine.py +++ b/python/dossier/multi_engine.py @@ -39,6 +39,7 @@ ROOT = Path(__file__).resolve().parents[2] +TEMPLATE = ROOT / "templates/run-report-v2.tex" class MultiEngineDossierError(RuntimeError): @@ -270,6 +271,8 @@ def _install_directory(staging: Path, destination: Path) -> None: def generate_multi_engine_dossier( case_path: str | Path, output_directory: str | Path, + *, + include_pdf: bool = False, ) -> Path: """Capture all named engines once and atomically install the complete v2 dossier.""" case: MultiEngineRunCase = load_run_case_v2(case_path, ROOT) @@ -435,7 +438,26 @@ def generate_multi_engine_dossier( f"shared narrative asset pass failed: {error}" ) from error _write_atomic(run_path, _encode_document(run_document)) - load_run_dossier_v2(run_path) + validated_document = load_run_dossier_v2(run_path) + if include_pdf: + from dossier.tex_compile import TexCompileError, compile_tex_pdf + from formats.narrative_assets import load_narrative_assets + from formats.run_report_v2_tex import render_run_report_v2_tex + + validated_narrative = load_narrative_assets( + narrative_manifest, + validated_document, + ) + report_tex = render_run_report_v2_tex( + validated_document, + validated_narrative, + TEMPLATE.read_text(encoding="utf-8"), + ) + _write_atomic(staging / "report.tex", report_tex.encode("utf-8")) + try: + compile_tex_pdf(staging, "pdflatex", captured_at) + except TexCompileError as error: + raise MultiEngineDossierError(str(error)) from error _install_directory(staging, destination) return destination except Exception: diff --git a/python/dossier/narrative_assets.py b/python/dossier/narrative_assets.py index b560a2a..74a5799 100644 --- a/python/dossier/narrative_assets.py +++ b/python/dossier/narrative_assets.py @@ -5,6 +5,7 @@ import argparse import copy import hashlib +import json import os from pathlib import Path import shutil @@ -24,6 +25,7 @@ OPTIMIZED_MECHANISMS_SHA256, SCHEMA_NAME, STATIC_NAMES, + boolean_z3_source_sha256, composite_source_sha256, generalized_source_sha256, generalized_presentation_source_sha256, @@ -31,6 +33,7 @@ load_narrative_assets, pipeline_source_sha256, verification_source_sha256, + wang_z3_source_sha256, witness_presentation_source_sha256, ) from formats.pipeline_snapshot import _encode_document, _write_atomic @@ -193,6 +196,62 @@ def _animation_metadata( run: dict[str, object], ) -> dict[str, dict[str, str]]: pipeline_digest = pipeline_source_sha256(identities, run) + search_diagnostic = run["case"]["expected_status"] == "unsat" + reference_trace_caption = ( + "Selected semantic milestones from the complete observed search " + "diagnostic; it is not an UNSAT certificate." + if search_diagnostic + else "Selected semantic milestones from the complete reference trace." + ) + optimized_trace_caption = ( + "Selected semantic milestones from the complete observed search " + "diagnostic; it is not an UNSAT certificate." + if search_diagnostic + else "Selected semantic milestones from the complete optimized trace." + ) + boolean_z3_caption = ( + "Source clauses retain occurrence-preserving exactly-one sums; " + "the assignment is not applicable for this UNSAT result." + if search_diagnostic + else "Real source clauses become occurrence-preserving exactly-one sums " + "before the copied assignment is shown." + ) + boolean_z3_alt = ( + "Four frames show source-order clauses and sums, then mark the Boolean " + "assignment not applicable because no SAT model was returned." + if search_diagnostic + else "Four frames place each source-order clause beside its occurrence-preserving " + "sum and then show the copied Boolean assignment." + ) + wang_z3_caption = ( + "The encoding is constructed, but cell, tile, boundary, and returned-model " + "examples are not applicable for this UNSAT result." + if search_diagnostic + else "A real cell shows its shared term, canonical tile tuple, boundary " + "equality, and returned model projection." + ) + wang_z3_alt = ( + "Five frames end with an UNSAT panel that makes no cell, tile tuple, " + "boundary, model, witness, or certificate claim." + if search_diagnostic + else "Five frames show adjacent canonical Wang tiles sharing an internal " + "edge, one exposed boundary equality, and the copied model projection." + ) + verification_caption = ( + "Six named checker receipts mark every witness check not applicable " + "because no SAT witness was returned." + if search_diagnostic + else "Six named checker receipts with concrete tiling rules and the recorded " + "native extraction beside its source cells." + ) + verification_alt = ( + "Six frames mark every witness check not applicable and state that no SAT " + "witness or certificate is fabricated." + if search_diagnostic + else "Six frames show all checker receipts, valid tile IDs, TILE_NONE, " + "internal and boundary equality, and copied extracted Boolean values " + "beside variable-gadget cells." + ) mechanism_digest = hashlib.sha256(MECHANISM_SOURCE.read_bytes()).hexdigest() if mechanism_digest != OPTIMIZED_MECHANISMS_SHA256: raise NarrativeAssetError( @@ -213,12 +272,15 @@ def _animation_metadata( "boolean_z3": _metadata( owner="/components/boolean-z3/", semantic_label="encoding-order", - caption="Project-owned Boolean constraint construction and returned assignment.", - alt_text="Four frames add Boolean variables and source-order exactly-one clauses before showing the copied result.", - source_contract="z3-encoding-summary-v1", - source_sha256=str(identities["boolean_z3_summary"]), + caption=boolean_z3_caption, + alt_text=boolean_z3_alt, + source_contract="z3-encoding-summary-v1+cm13-formula-snapshot-v1", + source_sha256=boolean_z3_source_sha256( + str(identities["boolean_z3_summary"]), + str(identities["formula_snapshot"]), + ), producer="formats.z3_encoding_summary.build_boolean_z3_summary", - validator="renderer.wang_z3_summary.load_z3_encoding_summary", + validator="renderer.wang_z3_summary.load_z3_encoding_summary+renderer.wang_snapshot.load_explainability_bundle", compositor="renderer.wang_z3_summary.render_boolean_z3_assets", ), "region_construction": _metadata( @@ -235,7 +297,7 @@ def _animation_metadata( "reference_trace": _metadata( owner="/components/reference-solver/", semantic_label="observed", - caption="Selected semantic milestones from the complete reference trace.", + caption=reference_trace_caption, alt_text="Observed reference domain states at root, propagation, decision, search, and result milestones.", source_contract="wang-explain-manifest-v3", source_sha256=str(identities["reference_trace_manifest"]), @@ -246,7 +308,7 @@ def _animation_metadata( "optimized_trace": _metadata( owner="/components/optimized-solver/", semantic_label="observed", - caption="Selected semantic milestones from the complete optimized trace.", + caption=optimized_trace_caption, alt_text="Observed optimized domain states at root, propagation, decision, search, and result milestones.", source_contract="wang-explain-manifest-v3", source_sha256=str(identities["optimized_trace_manifest"]), @@ -257,23 +319,27 @@ def _animation_metadata( "wang_z3": _metadata( owner="/components/wang-z3/", semantic_label="encoding-order", - caption="Project-owned Wang edge-term construction and returned model.", - alt_text="Five frames add edge terms, shared internal edges, tile relations, boundaries, and the copied result.", - source_contract="z3-encoding-summary-v1", - source_sha256=str(identities["wang_z3_summary"]), + caption=wang_z3_caption, + alt_text=wang_z3_alt, + source_contract="z3-encoding-summary-v1+wang-tileset-snapshot-v1+wang-region-snapshot-v1", + source_sha256=wang_z3_source_sha256( + str(identities["wang_z3_summary"]), + str(identities["tileset"]), + str(identities["region"]), + ), producer="formats.z3_encoding_summary.build_wang_z3_summary", - validator="renderer.wang_z3_summary.load_z3_encoding_summary", + validator="renderer.wang_z3_summary.load_z3_encoding_summary+renderer.wang_snapshot.load_explainability_bundle", compositor="renderer.wang_z3_summary.render_wang_z3_assets", ), "verification": _metadata( owner="/components/verification/", semantic_label="observed", - caption="The six named independent checker records from the captured run.", - alt_text="Six frames report Boolean, native, and Wang Z3 witness checks without rerunning a verifier.", + caption=verification_caption, + alt_text=verification_alt, source_contract="wang-run-dossier-v2#verification", source_sha256=verification_source_sha256(run), producer="formats.run_dossier_v2_builder.build_run_dossier_v2", - validator="formats.run_dossier_v2.validate_run_dossier_v2+renderer.wang_narrative._load_verification", + validator="formats.run_dossier_v2.validate_run_dossier_v2+renderer.wang_snapshot.load_explainability_bundle+renderer.wang_square.load_wang_presentation+renderer.wang_narrative._load_verification", compositor="renderer.wang_narrative.render_verification_assets", ), "witness_presentation": _metadata( @@ -292,8 +358,8 @@ def _animation_metadata( "optimized_mechanisms": _metadata( owner="/components/optimized-solver/", semantic_label="didactic", - caption="The six retained serial mechanisms, including the lazy MRV index.", - alt_text="Seven didactic frames contrast the reference baseline with six measured optimized mechanisms.", + caption="Six concrete panels show the retained serial mechanisms and their private state changes.", + alt_text="Seven didactic frames show stack, trail, ownership, byte-support, queue, and lazy-MRV state, ending with a static summary.", source_contract="wang-optimized-mechanisms-v1", source_sha256=mechanism_digest, producer="renderer/data/optimized-mechanisms-v1.json", @@ -325,8 +391,15 @@ def _static_metadata( "worked_example": _metadata( owner="/worked-example/", semantic_label="observed", - caption="Static t0 through tn component milestones for one SAT run.", - alt_text="Eight static panels follow the captured source from formula to checked presentation.", + caption=( + "Eight-stage overview with readable decision, construction, " + "verification, square-witness, and checked-hex details." + ), + alt_text=( + "An eight-stage overview followed by enlarged Boolean decision, " + "Yang-Zhang construction, six verification receipts, verified " + "square witness, and checked hex presentation panels." + ), source_contract="wang-run-dossier-v2#named-components", source_sha256=pipeline_source_sha256(identities, run), validator="formats.run_dossier_v2_bundle.load_run_dossier_v2", @@ -517,7 +590,12 @@ def generate_narrative_assets( ["wang_square.py", str(reference_manifest), str(formula_path), "--view", "formula"] ) boolean_outputs = _run_renderer( - ["wang_z3_summary.py", str(boolean_summary), str(staging / "boolean-z3")], + [ + "wang_z3_summary.py", + str(boolean_summary), + str(reference_manifest), + str(staging / "boolean-z3"), + ], required_outputs=("fallback",), ) region_outputs = _run_renderer( @@ -550,7 +628,12 @@ def generate_narrative_assets( required_outputs=("fallback",), ) wang_outputs = _run_renderer( - ["wang_z3_summary.py", str(wang_summary), str(staging / "wang-z3")], + [ + "wang_z3_summary.py", + str(wang_summary), + str(reference_manifest), + str(staging / "wang-z3"), + ], required_outputs=("fallback",), ) verification_receipts = staging / ".verification-receipts.json" @@ -558,13 +641,37 @@ def generate_narrative_assets( verification_receipts, _encode_document(_verification_receipts(run)), ) + verification_arguments = [ + "wang_narrative.py", + "verification", + str(verification_receipts), + str(staging / "verification"), + "--manifest", + str(reference_manifest), + ] + if run["case"]["expected_status"] == "sat": + reference_solution = _run_artifact( + run_root, run, "reference_solution" + ) + if reference_solution is None: + raise NarrativeAssetError( + "SAT verification explanation requires a reference solution" + ) + verification_arguments.extend( + [ + "--solution", + str(reference_solution), + "--assignment-json", + json.dumps( + run["reference"]["extracted_assignment"], + ensure_ascii=False, + allow_nan=False, + separators=(",", ":"), + ), + ] + ) verification_outputs = _run_renderer( - [ - "wang_narrative.py", - "verification", - str(verification_receipts), - str(staging / "verification"), - ], + verification_arguments, required_outputs=("fallback",), ) verification_receipts.unlink() diff --git a/python/dossier/tex_compile.py b/python/dossier/tex_compile.py new file mode 100644 index 0000000..48860aa --- /dev/null +++ b/python/dossier/tex_compile.py @@ -0,0 +1,109 @@ +"""Isolated, deterministic pdfLaTeX compilation for dossier callers.""" + +from __future__ import annotations + +import calendar +from datetime import datetime +import os +from pathlib import Path +import shutil +import subprocess + + +class TexCompileError(RuntimeError): + """The controlled dossier TeX compilation boundary failed.""" + + +def compile_tex_pdf( + dossier_root: Path, + tex_engine: str, + captured_at: datetime, +) -> None: + """Compile report.tex twice in an isolated TeX home without shell escape.""" + tex_home = dossier_root / ".tex-home" + private_home_created = False + compilation_completed = False + try: + try: + executable = shutil.which(tex_engine) + if executable is None: + raise TexCompileError(f"TeX engine not found: {tex_engine}") + tex_home.mkdir() + private_home_created = True + tex_var = tex_home / "var" + tex_config = tex_home / "config" + tex_fonts = tex_var / "fonts" + tex_var.mkdir() + tex_config.mkdir() + tex_fonts.mkdir() + environment = { + "PATH": os.environ.get("PATH", "/usr/bin:/bin"), + "HOME": str(tex_home), + "TEXMFHOME": str(tex_home / "texmf"), + "TEXMFVAR": str(tex_var), + "TEXMFCONFIG": str(tex_config), + "VARTEXFONTS": str(tex_fonts), + "SOURCE_DATE_EPOCH": str(calendar.timegm(captured_at.utctimetuple())), + "TZ": "UTC", + "openin_any": "p", + "openout_any": "p", + } + command = [ + executable, + "-interaction=nonstopmode", + "-halt-on-error", + "-file-line-error", + "-no-shell-escape", + "report.tex", + ] + for _ in range(2): + try: + subprocess.run( + command, + cwd=dossier_root, + env=environment, + check=True, + capture_output=True, + text=True, + timeout=120, + ) + except (OSError, subprocess.SubprocessError) as error: + detail = getattr(error, "stdout", "") or getattr( + error, "stderr", "" + ) + raise TexCompileError( + "LaTeX compilation failed without shell escape: " + f"{detail.strip()}" + ) from error + pdf = dossier_root / "report.pdf" + try: + if pdf.stat().st_size < 100 or not pdf.read_bytes().startswith( + b"%PDF-" + ): + raise TexCompileError( + "TeX engine did not produce a valid PDF header" + ) + except OSError as error: + raise TexCompileError(f"cannot inspect report.pdf: {error}") from error + for suffix in ("aux", "log", "out", "toc"): + auxiliary = dossier_root / f"report.{suffix}" + try: + auxiliary.unlink() + except FileNotFoundError: + pass + compilation_completed = True + except TexCompileError: + raise + except OSError as error: + raise TexCompileError( + f"TeX compilation filesystem operation failed: {error}" + ) from error + finally: + if private_home_created: + try: + shutil.rmtree(tex_home) + except OSError as error: + if compilation_completed: + raise TexCompileError( + f"cannot remove private TeX home: {error}" + ) from error diff --git a/python/formats/narrative_assets.py b/python/formats/narrative_assets.py index 27e69b0..376599b 100644 --- a/python/formats/narrative_assets.py +++ b/python/formats/narrative_assets.py @@ -159,7 +159,7 @@ ), "boolean_z3": ( "formats.z3_encoding_summary.build_boolean_z3_summary", - "renderer.wang_z3_summary.load_z3_encoding_summary", + "renderer.wang_z3_summary.load_z3_encoding_summary+renderer.wang_snapshot.load_explainability_bundle", "renderer.wang_z3_summary.render_boolean_z3_assets", ), "region_construction": ( @@ -179,12 +179,12 @@ ), "wang_z3": ( "formats.z3_encoding_summary.build_wang_z3_summary", - "renderer.wang_z3_summary.load_z3_encoding_summary", + "renderer.wang_z3_summary.load_z3_encoding_summary+renderer.wang_snapshot.load_explainability_bundle", "renderer.wang_z3_summary.render_wang_z3_assets", ), "verification": ( "formats.run_dossier_v2_builder.build_run_dossier_v2", - "formats.run_dossier_v2.validate_run_dossier_v2+renderer.wang_narrative._load_verification", + "formats.run_dossier_v2.validate_run_dossier_v2+renderer.wang_snapshot.load_explainability_bundle+renderer.wang_square.load_wang_presentation+renderer.wang_narrative._load_verification", "renderer.wang_narrative.render_verification_assets", ), "witness_presentation": ( @@ -253,6 +253,13 @@ def verification_source_sha256(run: dict[str, object]) -> str: { "verification": run["verification"], "agreement": run["agreement"], + "source_formula": run["source"]["sha256"], + "formula_snapshot": run["reduction"]["formula_sha256"], + "tileset": run["reduction"]["tileset_sha256"], + "region": run["reduction"]["region_sha256"], + "provenance": run["reduction"]["provenance_sha256"], + "reference_solution": run["reference"]["solution_sha256"], + "reference_assignment": run["reference"]["extracted_assignment"], } ) ).hexdigest() @@ -262,6 +269,24 @@ def composite_source_sha256(values: dict[str, str]) -> str: return hashlib.sha256(_encode_document(values)).hexdigest() +def boolean_z3_source_sha256(summary_sha256: str, formula_sha256: str) -> str: + return composite_source_sha256( + {"summary": summary_sha256, "formula_snapshot": formula_sha256} + ) + + +def wang_z3_source_sha256( + summary_sha256: str, tileset_sha256: str, region_sha256: str +) -> str: + return composite_source_sha256( + { + "summary": summary_sha256, + "tileset": tileset_sha256, + "region": region_sha256, + } + ) + + def generalized_source_sha256(tileset_sha256: str) -> str: return composite_source_sha256( { @@ -586,7 +611,13 @@ def load_narrative_assets( "wang-run-dossier-v2#named-components", pipeline_digest, ), - "boolean_z3": ("z3-encoding-summary-v1", expected_identities["boolean_z3_summary"]), + "boolean_z3": ( + "z3-encoding-summary-v1+cm13-formula-snapshot-v1", + boolean_z3_source_sha256( + expected_identities["boolean_z3_summary"], + expected_identities["formula_snapshot"], + ), + ), "region_construction": ( "wang-reduction-explanation-v1", expected_identities["provenance"], @@ -599,7 +630,14 @@ def load_narrative_assets( "wang-explain-manifest-v3", expected_identities["optimized_trace_manifest"], ), - "wang_z3": ("z3-encoding-summary-v1", expected_identities["wang_z3_summary"]), + "wang_z3": ( + "z3-encoding-summary-v1+wang-tileset-snapshot-v1+wang-region-snapshot-v1", + wang_z3_source_sha256( + expected_identities["wang_z3_summary"], + expected_identities["tileset"], + expected_identities["region"], + ), + ), "verification": ( "wang-run-dossier-v2#verification", verification_source_sha256(run_document), diff --git a/python/formats/run_report_v2_tex.py b/python/formats/run_report_v2_tex.py new file mode 100644 index 0000000..c9b9077 --- /dev/null +++ b/python/formats/run_report_v2_tex.py @@ -0,0 +1,448 @@ +"""Pure static LaTeX formatter for caller-validated v2 dossier inputs.""" + +from __future__ import annotations + +from pathlib import PurePosixPath +import re +from typing import Iterable + +from formats.run_dossier_v2 import validate_run_dossier_v2 + + +_SAFE_PATH = re.compile(r"[A-Za-z0-9._/-]+\Z") + + +def _tex(value: object) -> str: + text = str(value).replace("\u00a0", " ") + text = text.replace("–", "--").replace("—", "---").replace("→", " to ") + replacements = { + "\\": r"\textbackslash{}", + "{": r"\{", + "}": r"\}", + "$": r"\$", + "&": r"\&", + "#": r"\#", + "_": r"\_", + "%": r"\%", + "~": r"\textasciitilde{}", + "^": r"\textasciicircum{}", + } + return "".join(replacements.get(character, character) for character in text) + + +def _path(value: object, *, narrative: bool = False) -> str: + """Constrain already validated paths before placing them in TeX commands.""" + text = str(value) + parsed = PurePosixPath(text) + if ( + _SAFE_PATH.fullmatch(text) is None + or parsed.is_absolute() + or parsed.as_posix() != text + or any(part in ("", ".", "..") for part in parsed.parts) + ): + raise ValueError("report artifact path is not a safe normalized relative path") + return f"assets/narrative/{text}" if narrative else text + + +def _wide_figure(path: str, caption: str) -> str: + """Keep a bounded static image and its caption on the same page.""" + return "\n".join( + ( + r"\begin{center}", + r"\begin{minipage}{\textwidth}", + r"\centering", + rf"\includegraphics[width=\textwidth,height=0.48\textheight,keepaspectratio]{{{path}}}", + rf"\par\smallskip{{\small\itshape {_tex(caption)}}}", + r"\end{minipage}", + r"\end{center}", + ) + ) + + +def _multi_panel_figure(paths: Iterable[str], caption: str) -> str: + panels = [] + for path in paths: + panels.extend( + ( + r"\begin{center}", + r"\centering", + rf"\includegraphics[width=\textwidth,height=0.43\textheight,keepaspectratio]{{{path}}}", + r"\end{center}", + ) + ) + return "\n".join( + ( + *panels, + rf"\par\smallskip{{\small\itshape {_tex(caption)}}}", + ) + ) + + +def _tall_figure(path: str, caption: str) -> str: + return "\n".join( + ( + r"\begin{center}", + r"\centering", + rf"\includegraphics[width=0.82\textwidth,height=0.64\textheight,keepaspectratio]{{{path}}}", + rf"\par\smallskip{{\small\itshape {_tex(caption)}}}", + r"\end{center}", + ) + ) + + +def _compact_figure(path: str, caption: str) -> str: + return "\n".join( + ( + r"\begin{center}", + r"\centering", + rf"\includegraphics[width=0.72\textwidth,height=0.30\textheight,keepaspectratio]{{{path}}}", + rf"\par\smallskip{{\small\itshape {_tex(caption)}}}", + r"\end{center}", + ) + ) + + +def _atomic_legend_figure(path: str, caption: str) -> str: + """Show the fixed 1732x4184 atomic legend as two readable static crops.""" + return "\n".join( + ( + r"\clearpage", + r"\begin{center}", + rf"\includegraphics[viewport=0 2092 1732 4184,clip,width=0.92\textwidth]{{{path}}}", + r"\end{center}", + r"\clearpage", + r"\begin{center}", + rf"\includegraphics[viewport=0 0 1732 2092,clip,width=0.92\textwidth]{{{path}}}", + rf"\par\smallskip{{\small\itshape {_tex(caption)}}}", + r"\end{center}", + ) + ) + + +def _elapsed(value: object) -> str: + if value is None: + return "not applicable" + elapsed = int(value) + return f"{elapsed / 1_000_000:.3f} ms ({elapsed} ns)" + + +def _trace_summary(record: dict[str, object]) -> str: + trace = record["trace"] + assert isinstance(trace, dict) + return "\n".join( + ( + r"\begin{tabular}{@{}>{\bfseries}p{0.31\textwidth}p{0.61\textwidth}@{}}", + rf"Status & {_tex(record['status'])} \\", + rf"Solver & {_tex(trace['solver'])} \\", + rf"Observed events & {_tex(trace['observed_event_count'])} \\", + rf"Selected static milestones & {_tex(trace['selection']['selected_event_count'])} \\", + rf"Complete / truncated & {_tex(trace['complete'])} / {_tex(trace['truncated'])} \\", + rf"Checkpoints & {_tex(trace['checkpoint_count'])} \\", + r"\end{tabular}", + ) + ) + + +def _narrative_artifact(record: dict[str, object], field: str) -> str: + artifact = record[field] + assert isinstance(artifact, dict) + return _path(artifact["path"], narrative=True) + + +def _milestones(manifest: dict[str, object], name: str) -> tuple[str, ...]: + milestone_map = manifest["pdf_milestones"] + assert isinstance(milestone_map, dict) + paths = milestone_map[name] + assert isinstance(paths, list) + return tuple(_path(path, narrative=True) for path in paths) + + +def render_run_report_v2_tex( + document: dict[str, object], + manifest: dict[str, object], + template: str, +) -> str: + """Render TeX from a validated run and caller-validated narrative manifest. + + The caller must load the manifest through ``load_narrative_assets`` before + invoking this pure formatter. The formatter performs no file I/O, replay, + solving, witness checking, timing, or image composition. + """ + validate_run_dossier_v2(document) + if template.count("@@TITLE@@") != 1 or template.count("@@BODY@@") != 1: + raise ValueError("v2 report template must contain one title and one body marker") + if manifest.get("schema") != "wang-narrative-assets-v1": + raise ValueError("v2 report requires a caller-validated narrative manifest") + + case = document["case"] + source = document["source"] + environment = document["environment"] + boolean_z3 = document["boolean_z3"] + reduction = document["reduction"] + reference = document["reference"] + optimized = document["optimized"] + wang_z3 = document["wang_z3"] + verification = document["verification"] + agreement = document["agreement"] + timings = document["timings"] + artifacts = document["artifacts"] + animations = manifest["animations"] + statics = manifest["statics"] + assert all( + isinstance(item, dict) + for item in ( + case, + source, + environment, + boolean_z3, + reduction, + reference, + optimized, + wang_z3, + verification, + agreement, + timings, + artifacts, + animations, + statics, + ) + ) + status = str(case["expected_status"]) + + source_artifact = artifacts["source_input"] + assert isinstance(source_artifact, dict) + source_path = _path(source_artifact["path"]) + formula_static = statics["formula"] + generalized_sheet = statics["generalized_sheet"] + atomic_legend = statics["atomic_legend"] + assert isinstance(formula_static, dict) + assert isinstance(generalized_sheet, dict) + assert isinstance(atomic_legend, dict) + + boolean_animation = animations["boolean_z3"] + reference_animation = animations["reference_trace"] + optimized_animation = animations["optimized_trace"] + mechanisms_animation = animations["optimized_mechanisms"] + wang_animation = animations["wang_z3"] + verification_animation = animations["verification"] + assert all( + isinstance(item, dict) + for item in ( + boolean_animation, + reference_animation, + optimized_animation, + mechanisms_animation, + wang_animation, + verification_animation, + ) + ) + + boolean_assignment = ( + "not applicable for this UNSAT result" + if status == "unsat" + else ", ".join( + f"variable {index + 1}={'true' if value else 'false'}" + for index, value in enumerate(boolean_z3["assignment"]) + ) + ) + witness_note = ( + "Witness verification: not applicable. Witness presentations: not " + "applicable. No SAT witness or UNSAT certificate is fabricated. No UNSAT " + "certificate is claimed by the observed search trace." + if status == "unsat" + else ( + "All six named independent witness checks passed. Presentation follows " + "verification and does not establish satisfiability." + ) + ) + + verification_rows = [] + for name, check in verification.items(): + assert isinstance(check, dict) + result = "not applicable" if not check["performed"] else "passed" + verification_rows.append( + rf"{_tex(name)} & {_tex(check['checker'])} & {_tex(result)} \\" + ) + + timing_rows = [] + for name, elapsed in timings.items(): + if name in {"clock", "identity"}: + continue + timing_rows.append(rf"{_tex(name)} & {_tex(_elapsed(elapsed))} \\") + + hash_blocks = [] + for name, artifact in artifacts.items(): + if artifact is None: + continue + assert isinstance(artifact, dict) + hash_blocks.append( + "\n".join( + ( + r"\begin{samepage}", + rf"\textbf{{{_tex(name)}}}\par", + rf"Path: \path{{{_path(artifact['path'])}}}\par", + rf"SHA-256: \path{{{artifact['sha256']}}}\par\smallskip", + r"\end{samepage}", + ) + ) + ) + + presentation_block: list[str] + if status == "sat": + presentation_items = [] + for name in ("square", "generalized", "hex"): + record = statics[f"{name}_presentation"] + assert isinstance(record, dict) + presentation_items.append( + (_narrative_artifact(record, "artifact"), str(record["caption"])) + ) + presentation_block = [ + _wide_figure(path, caption) for path, caption in presentation_items + ] + else: + presentation_status = statics["presentation_status"] + assert isinstance(presentation_status, dict) + presentation_block = [ + _compact_figure( + _narrative_artifact(presentation_status, "artifact"), + str(presentation_status["caption"]), + ) + ] + + body = "\n".join( + ( + r"\section{Summary}", + _tex(case["purpose"]), + "", + r"\begin{tabular}{@{}>{\bfseries}p{0.27\textwidth}p{0.65\textwidth}@{}}", + rf"Case & {_tex(case['id'])} \\", + rf"Terminal status & {_tex(status.upper())} \\", + rf"All named statuses agree & {_tex(agreement['all_status_equal'])} \\", + rf"Agreement passed & {_tex(agreement['passed'])} \\", + r"\end{tabular}", + _multi_panel_figure( + _milestones(manifest, "end_to_end"), + "Static semantic milestones from this validated full-pipeline run.", + ), + r"\clearpage", + r"\section{Source instance}", + rf"Recorded source: \path{{{_path(source['path'])}}}.\par", + rf"Source SHA-256: \path{{{source['sha256']}}}.\par", + _wide_figure( + _narrative_artifact(formula_static, "artifact"), + "Parsed formula snapshot for this named source.", + ), + r"\verbatiminput{" + source_path + "}", + r"\section{Boolean Z3}", + rf"Status: {_tex(boolean_z3['status'])}. Random seed: {_tex(boolean_z3['configuration']['random_seed'])}. Threads: {_tex(boolean_z3['configuration']['threads'])}.", + ( + rf"\par Recorded elapsed time: {_tex(_elapsed(timings['boolean_z3_ns']))}. " + r"This run-specific observation is not a benchmark.\par" + ), + ( + "Source variables are written 1-based (1, 2, ...); the static " + "encoding figure labels stored zero-based IDs (x0, x1, ...)." + ), + rf"Assignment: {_tex(boolean_assignment)}.", + _tall_figure( + _narrative_artifact(boolean_animation, "fallback"), + str(boolean_animation["caption"]), + ), + r"\section{Yang--Zhang reduction}", + ( + "The native reduction is recorded once. The figures below reuse its " + "validated provenance and canonical generalized vocabulary." + ), + _multi_panel_figure( + _milestones(manifest, "region_construction"), + str(animations["region_construction"]["caption"]), + ), + _tall_figure( + _narrative_artifact(generalized_sheet, "artifact"), + str(generalized_sheet["caption"]), + ), + _atomic_legend_figure( + _narrative_artifact(atomic_legend, "artifact"), + str(atomic_legend["caption"]), + ), + r"\section{Reference solver}", + _trace_summary(reference), + _multi_panel_figure( + _milestones(manifest, "reference_trace"), + str(reference_animation["caption"]), + ), + r"\section{Optimized solver}", + _trace_summary(optimized), + _multi_panel_figure( + _milestones(manifest, "optimized_trace"), + str(optimized_animation["caption"]), + ), + _tall_figure( + _narrative_artifact(mechanisms_animation, "fallback"), + str(mechanisms_animation["caption"]), + ), + r"\section{Wang Z3}", + rf"Status: {_tex(wang_z3['status'])}. Random seed: {_tex(wang_z3['configuration']['random_seed'])}. Threads: {_tex(wang_z3['configuration']['threads'])}.", + ( + rf"\par Recorded elapsed time: {_tex(_elapsed(timings['wang_z3_ns']))}. " + r"This run-specific observation is not a benchmark.\par" + ), + _tall_figure( + _narrative_artifact(wang_animation, "fallback"), + str(wang_animation["caption"]), + ), + r"\section{Verification and presentation}", + witness_note, + r"\begin{longtable}{@{}p{0.24\textwidth}p{0.52\textwidth}p{0.16\textwidth}@{}}", + r"\textbf{Check} & \textbf{Independent checker} & \textbf{Result} \\", + *verification_rows, + r"\end{longtable}", + _tall_figure( + _narrative_artifact(verification_animation, "fallback"), + str(verification_animation["caption"]), + ), + *presentation_block, + r"\clearpage", + r"\section{Reproducibility appendix}", + ( + "These are raw observations from one captured environment, not a " + "benchmark. The PDF consumes the validated run and static narrative " + "assets; it does not solve, invoke Z3, replay traces, compose images, " + "recount events, or independently verify a witness." + ), + r"\par\medskip", + rf"\textbf{{Git commit:}} \path{{{environment['git_commit']}}}\par", + rf"\textbf{{Captured UTC:}} {_tex(environment['captured_at_utc'])}\par", + rf"\textbf{{Platform:}} {_tex(environment['platform'])}\par", + rf"\textbf{{Python:}} {_tex(environment['python'])}\par", + rf"\textbf{{Timing identity:}} {_tex(timings['identity'])}\par", + ( + rf"\textbf{{Narrative manifest:}} {_tex(manifest['schema'])}; " + rf"product {_tex(manifest['product'])}; selector " + rf"{_tex(manifest['pdf_milestones']['selector'])}.\par" + ), + ( + r"\textbf{Reference trace parameters:} " + rf"event capacity {_tex(reference['configuration']['event_capacity'])}; " + rf"checkpoint interval {_tex(reference['configuration']['checkpoint_interval'])}; " + rf"checkpoint capacity {_tex(reference['configuration']['checkpoint_capacity'])}.\par" + ), + ( + r"\textbf{Optimized trace parameters:} " + rf"event capacity {_tex(optimized['configuration']['event_capacity'])}; " + rf"checkpoint interval {_tex(optimized['configuration']['checkpoint_interval'])}; " + rf"checkpoint capacity {_tex(optimized['configuration']['checkpoint_capacity'])}.\par" + ), + r"\subsection{Raw timings}", + r"\begin{tabular}{@{}p{0.38\textwidth}p{0.54\textwidth}@{}}", + *timing_rows, + r"\end{tabular}", + r"\subsection{Artifact identities}", + r"\footnotesize", + *hash_blocks, + r"\normalsize", + ) + ) + return template.replace("@@TITLE@@", _tex(case["title"])).replace( + "@@BODY@@", body + ) diff --git a/renderer/test_wang_algorithm_animation.py b/renderer/test_wang_algorithm_animation.py index bccfb13..878a4d6 100644 --- a/renderer/test_wang_algorithm_animation.py +++ b/renderer/test_wang_algorithm_animation.py @@ -1,15 +1,18 @@ from __future__ import annotations +from dataclasses import replace from pathlib import Path -from PIL import Image +from PIL import Image, ImageDraw +import wang_algorithm_animation from wang_algorithm_animation import ( main, render_builder_assets, render_hex_assets, render_optimized_assets, ) +from wang_snapshot import load_explainability_bundle RENDERER = Path(__file__).resolve().parent @@ -47,30 +50,403 @@ def _assert_stable_assets( def test_builder_animation_uses_versioned_provenance_and_is_byte_stable(tmp_path): + bundle = load_explainability_bundle(BUILDER_MANIFEST) + reduction = bundle.reduction + assert reduction is not None + assert tuple(signal.token_id for signal in reduction.source_signals) == ( + 0, 1, 2, 9, 3, 4, 5, 10, 6, 7, 8 + ) + assert tuple(signal.token_id for signal in reduction.target_signals) == ( + 0, 1, 3, 9, 2, 4, 6, 10, 5, 7, 8 + ) + crossovers = tuple( + gadget for gadget in reduction.gadgets if gadget.kind == "crossover" + ) + assert tuple(gadget.swap_row for gadget in crossovers) == (3, 2, 3, 7, 6, 7) + assert tuple((gadget.x_begin, gadget.x_end) for gadget in crossovers) == ( + (3, 7), (7, 10), (10, 14), (14, 22), (22, 29), (29, 37) + ) + + replay_orders = getattr(wang_algorithm_animation, "_replay_signal_orders", None) + assert replay_orders is not None + assert tuple( + signal.token_id for signal in replay_orders(reduction)[1] + ) == (0, 1, 2, 3, 9, 4, 5, 10, 6, 7, 8) + first = render_builder_assets(BUILDER_MANIFEST, tmp_path / "first") render_builder_assets(BUILDER_MANIFEST, tmp_path / "second") - assert first.fallback.name == "frame-04.png" - _assert_stable_assets( - tmp_path / "first", - tmp_path / "second", - GOLDENS / "region-construction", - frame_count=6, - fallback_name="frame-04.png", + assert first.fallback.name == "frame-05.png" + assert _tree_bytes(tmp_path / "first") == _tree_bytes(tmp_path / "second") + with Image.open(first.animation) as animation: + assert animation.format == "GIF" + assert animation.n_frames == 6 + with Image.open(first.fallback) as fallback: + assert fallback.size == (1976, 828) + + frame = getattr(wang_algorithm_animation, "_builder_frame") + source_changed = replace( + bundle, + reduction=replace( + reduction, + source_signals=tuple(reversed(reduction.source_signals)), + ), + ) + target_changed = replace( + bundle, + reduction=replace( + reduction, + target_signals=tuple(reversed(reduction.target_signals)), + ), + ) + crossover_changed = replace( + bundle, + reduction=replace( + reduction, + gadgets=tuple( + replace(gadget, swap_row=4) + if gadget is crossovers[0] + else gadget + for gadget in reduction.gadgets + ), + ), + ) + assert frame(bundle, 0).tobytes() != frame(source_changed, 0).tobytes() + assert frame(bundle, 1).tobytes() != frame(target_changed, 1).tobytes() + assert frame(bundle, 2).tobytes() != frame(crossover_changed, 2).tobytes() + + +def test_builder_final_panel_distinguishes_region_and_boundary_states(): + bundle = load_explainability_bundle(BUILDER_MANIFEST) + frame = getattr(wang_algorithm_animation, "_builder_frame")(bundle, 5) + assert frame.size == (1976, 828) + + # Hand-checked fixture cells: (1, 1) is active with internal edges, + # (40, 0) is inactive, and the north side of (0, 0) exposes color 0. + grid_x, grid_y, cell = 36, 348, 30 + assert frame.getpixel((grid_x + cell + 15, grid_y + cell + 15)) == ( + 238, 241, 246 + ) + assert frame.getpixel((grid_x + 40 * cell + 10, grid_y + 15)) in { + (226, 230, 236), + (190, 197, 207), + } + assert frame.getpixel((grid_x + 15, grid_y + 2)) == (81, 237, 39) + assert frame.getpixel((grid_x + 2 * cell - 1, grid_y + cell + 15)) == ( + 174, 181, 193 ) +def test_builder_handles_a_valid_reduction_that_needs_no_crossover(): + bundle = load_explainability_bundle(BUILDER_MANIFEST) + reduction = bundle.reduction + assert reduction is not None + no_swap_bundle = replace( + bundle, + reduction=replace( + reduction, + target_signals=reduction.source_signals, + gadgets=tuple( + gadget + for gadget in reduction.gadgets + if gadget.kind != "crossover" + ), + ), + ) + frame = getattr(wang_algorithm_animation, "_builder_frame") + + assert frame(no_swap_bundle, 2).size == (1976, 828) + assert frame(no_swap_bundle, 3).size == (1976, 828) + + +def test_builder_preserves_noncanonical_region_capture_scope(): + bundle = load_explainability_bundle(BUILDER_MANIFEST) + wide_region = replace( + bundle.region, + max_x=399, + max_y=0, + active=(False,) * 400, + boundary=(None,) * 400, + ) + wide_bundle = replace(bundle, region=wide_region) + + assert getattr(wang_algorithm_animation, "_builder_frame")( + wide_bundle, 5 + ).size == (1976, 828) + + +def test_builder_summarizes_a_valid_44_variable_signal_strip(): + bundle = load_explainability_bundle(BUILDER_MANIFEST) + reduction = bundle.reduction + assert reduction is not None + variable = next( + signal for signal in reduction.source_signals if signal.kind == "variable" + ) + redundant = next( + signal for signal in reduction.source_signals if signal.kind == "redundant" + ) + signals_list = [] + for variable_id in range(44): + for occurrence in range(3): + signals_list.append( + replace( + variable, + row=len(signals_list), + token_id=3 * variable_id + occurrence, + variable=variable_id, + occurrence=occurrence, + ) + ) + if variable_id < 43: + signals_list.append( + replace( + redundant, + row=len(signals_list), + token_id=132 + variable_id, + variable=None, + occurrence=None, + ) + ) + signals = tuple(signals_list) + assert len(signals) == 4 * 44 - 1 + strip_items = getattr(wang_algorithm_animation, "_signal_strip_items") + items = strip_items(signals, (86, 87)) + + shown_rows = tuple(row for row, signal, _ in items if signal is not None) + assert shown_rows == (0, 1, 2, 85, 86, 87, 88, 172, 173, 174) + assert sum(omitted for _, _, omitted in items) == 165 + assert tuple( + signal.token_id + for row, signal, _ in items + if row in {86, 87} + ) == (65, 153) + + image = Image.new("RGB", (1976, 828), "white") + getattr(wang_algorithm_animation, "_draw_signal_order")( + ImageDraw.Draw(image), + y=140, + label="source", + signals=signals, + highlighted_rows=(86, 87), + ) + assert image.size == (1976, 828) + box_width, gap = 134, 10 + for position in range(len(items) - 1): + gap_x = 220 + position * (box_width + gap) + box_width + gap // 2 + assert all( + max(image.getpixel((gap_x, pixel_y))) >= 180 + for pixel_y in range(148, 191) + ) + + display = image.resize((390, 164), Image.Resampling.LANCZOS) + display_scale = 390 / image.width + for position in range(len(items) - 1): + gap_x = round( + (220 + position * (box_width + gap) + box_width + gap // 2) + * display_scale + ) + assert all( + max(display.getpixel((gap_x, pixel_y))) >= 180 + for pixel_y in range(round(148 * display_scale), round(191 * display_scale)) + ) + + def test_optimized_didactic_animation_is_byte_stable(tmp_path): + mechanisms = getattr(wang_algorithm_animation, "_load_optimizations")() + assert tuple(mechanism.identifier for mechanism in mechanisms) == ( + "dynamic-dfs-stack", + "initial-trail-omission", + "sat-ownership-transfer", + "byte-support-table", + "queue-deduplication", + "lazy-mrv-index", + ) + first = render_optimized_assets(tmp_path / "first") render_optimized_assets(tmp_path / "second") assert first.fallback.name == "frame-06.png" - _assert_stable_assets( - tmp_path / "first", - tmp_path / "second", - GOLDENS / "optimized-mechanisms", - frame_count=7, - fallback_name="frame-06.png", + assert _tree_bytes(tmp_path / "first") == _tree_bytes(tmp_path / "second") + assert tuple(path.name for path in first.frames) == tuple( + f"frame-{index:02d}.png" for index in range(7) + ) + assert len({path.read_bytes() for path in first.frames}) == 7 + with Image.open(first.animation) as animation: + assert animation.format == "GIF" + assert animation.n_frames == 7 + with Image.open(first.fallback) as fallback: + assert fallback.size == (1920, 1040) + with Image.open(first.contact_sheet) as contact_sheet: + assert contact_sheet.size == (5760, 3120) + + +def test_byte_support_panel_aggregates_three_bytes_of_a_23_bit_domain(): + example = getattr(wang_algorithm_animation, "_byte_support_example")() + + assert example == { + "domain": 0x400401, + "chunks": (0x01, 0x04, 0x40), + "source_tiles": (0, 10, 22), + "source_east_edges": (2, 3, 3), + "supported_tiles": ( + 4, 5, 6, 7, 8, 9, 10, 11, 13, 15, 16, 17, 18, 19, 20, 21, 22 + ), + } + + +def test_essential_byte_support_and_mrv_labels_survive_mobile_downsampling(): + frame = getattr(wang_algorithm_animation, "_optimized_frame") + + def mobile_ink_height(image: Image.Image, source_box: tuple[int, int, int, int]) -> int: + scale = 390 / image.width + preview = image.resize( + (390, round(image.height * scale)), + Image.Resampling.LANCZOS, + ) + box = tuple(round(value * scale) for value in source_box) + crop = preview.crop(box) + ink_rows = [ + y + for y in range(crop.height) + if any(max(crop.getpixel((x, y))) < 140 for x in range(crop.width)) + ] + return max(ink_rows) - min(ink_rows) + 1 if ink_rows else 0 + + byte_support = frame(3) + assert mobile_ink_height(byte_support, (65, 315, 390, 380)) >= 7 + assert mobile_ink_height(byte_support, (65, 375, 430, 445)) >= 7 + assert mobile_ink_height(byte_support, (65, 435, 370, 495)) >= 7 + + lazy_mrv = frame(5) + assert mobile_ink_height(lazy_mrv, (60, 430, 220, 520)) >= 7 + assert mobile_ink_height(lazy_mrv, (50, 600, 160, 670)) >= 7 + assert mobile_ink_height(lazy_mrv, (40, 900, 1850, 955)) >= 7 + + summary = getattr(wang_algorithm_animation, "_optimized_summary")() + assert mobile_ink_height(summary, (65, 155, 560, 220)) >= 8 + assert mobile_ink_height(summary, (650, 245, 915, 325)) >= 7 + + trail = frame(1) + arrow_corridor = trail.crop((535, 295, 588, 400)) + assert not any( + max(arrow_corridor.getpixel((x, y))) < 140 + for y in range(arrow_corridor.height) + for x in range(arrow_corridor.width) + ) + + bucket_row = lazy_mrv.crop((48, 755, 620, 815)) + assert (111, 82, 176) not in bucket_row.get_flattened_data() + + ownership = frame(2) + for corridor in ( + (60, 275, 99, 365), + (170, 665, 204, 765), + (696, 665, 730, 765), + (1010, 275, 1049, 365), + (1120, 665, 1154, 765), + (1646, 665, 1680, 765), + ): + outside_box = ownership.crop(corridor) + assert not any( + max(outside_box.getpixel((x, y))) < 140 + for y in range(outside_box.height) + for x in range(outside_box.width) + ) + + +def test_static_summary_names_the_omitted_initial_undo_entry_positively(monkeypatch): + labels: list[str] = [] + original_centered_text = wang_algorithm_animation.centered_text + + def record_centered_text(draw, box, text, **kwargs): + labels.append(text) + return original_centered_text(draw, box, text, **kwargs) + + monkeypatch.setattr(wang_algorithm_animation, "centered_text", record_centered_text) + + summary = getattr(wang_algorithm_animation, "_optimized_summary")() + + assert "initial undo entry" in (label.replace("\n", " ") for label in labels) + assert "no undo entry" not in labels + mobile = summary.resize((390, round(summary.height * 390 / summary.width)), Image.Resampling.LANCZOS) + label_box = mobile.crop(tuple(round(value * 390 / summary.width) for value in (1604, 248, 1774, 328))) + ink_rows = [ + y + for y in range(label_box.height) + if any(max(label_box.getpixel((x, y))) < 140 for x in range(label_box.width)) + ] + assert max(ink_rows) - min(ink_rows) + 1 >= 12 + + +def test_static_summary_support_union_stays_out_of_incoming_arrow(): + summary = getattr(wang_algorithm_animation, "_optimized_summary")() + + for width in (1920, 390, 720): + scale = width / summary.width + preview = summary.resize( + (width, round(summary.height * scale)), + Image.Resampling.LANCZOS, + ) + arrow_only_corridor = preview.crop( + tuple(round(value * scale) for value in (1374, 515, 1519, 595)) + ) + assert not any( + max(arrow_only_corridor.getpixel((x, y))) < 140 + for y in range(arrow_only_corridor.height) + for x in range(arrow_only_corridor.width) + ) + + +def test_optimized_ownership_outcome_clears_panel_bottom_border(): + ownership = getattr(wang_algorithm_animation, "_optimized_frame")(2) + + for width in (1920, 390, 720): + scale = width / ownership.width + preview = ownership.resize( + (width, round(ownership.height * scale)), + Image.Resampling.LANCZOS, + ) + bottom_safety_band = preview.crop( + tuple(round(value * scale) for value in (1001, 890, 1872, 910)) + ) + assert not any( + max(bottom_safety_band.getpixel((x, y))) < 140 + for y in range(bottom_safety_band.height) + for x in range(bottom_safety_band.width) + ) + + +def test_queue_panel_suppresses_only_while_a_cell_is_pending(): + assert getattr(wang_algorithm_animation, "_queue_dedup_steps")() == ( + ("enqueue c7", "append", (7,)), + ("enqueue c7 again", "suppress", (7,)), + ("dequeue c7", "clear pending", ()), + ("enqueue c7 later", "append", (7,)), + ) + + +def test_lazy_mrv_panel_moves_a_domain_bucket_and_reverses_it_on_rollback(): + steps = getattr(wang_algorithm_animation, "_mrv_bucket_steps")() + + assert steps == ( + ( + "after lazy build", + ((2, 4), (5, 2), (9, 3)), + ((2, (5,)), (3, (9,)), (4, (2,))), + 5, + ), + ( + "restrict c2: 4 -> 2", + ((2, 2), (5, 2), (9, 3)), + ((2, (2, 5)), (3, (9,))), + 2, + ), + ( + "rollback c2: 2 -> 4", + ((2, 4), (5, 2), (9, 3)), + ((2, (5,)), (3, (9,)), (4, (2,))), + 5, + ), ) diff --git a/renderer/test_wang_narrative.py b/renderer/test_wang_narrative.py index 88d60f9..d4b46f1 100644 --- a/renderer/test_wang_narrative.py +++ b/renderer/test_wang_narrative.py @@ -1,13 +1,16 @@ from __future__ import annotations +from dataclasses import replace import hashlib import json from pathlib import Path +import re import sys -from PIL import Image +from PIL import Image, ImageDraw import pytest +import wang_narrative from wang_hex_port import WangSquareRenderError from wang_generalized import generalized_specification_sha256 from wang_narrative import ( @@ -17,12 +20,19 @@ render_verification_assets, render_witness_assets, ) +from wang_snapshot import load_explainability_bundle +from wang_square import load_wang_presentation RENDERER = Path(__file__).resolve().parent ROOT = RENDERER.parent MANIFEST = ROOT / "tests/fixtures/pipeline_sat_reduction_explain/manifest.json" SOLUTION = ROOT / "tests/fixtures/wang_solution_v1_square_sat.json" +TRACE_MANIFEST = ROOT / "tests/fixtures/pipeline_sat_solver_trace/manifest.json" +TRACE_SOLUTION = next( + (ROOT / "tests/fixtures/pipeline_sat_solver_trace").glob("solution-*.json") +) +ASSIGNMENT = (False, True, False) def _tree_bytes(directory: Path) -> dict[str, bytes]: @@ -33,7 +43,38 @@ def _tree_bytes(directory: Path) -> dict[str, bytes]: } -def _run_record(status: str) -> dict[str, object]: +def _encoded(document: dict[str, object]) -> bytes: + return ( + json.dumps(document, ensure_ascii=False, allow_nan=False, indent=2) + "\n" + ).encode("utf-8") + + +def _witness_digest(values: tuple[bool, ...]) -> str: + return hashlib.sha256(_encoded({"witness": list(values)})).hexdigest() + + +def _mobile_ink_height( + image: Image.Image, source_box: tuple[int, int, int, int] +) -> int: + scale = 390 / image.width + mobile = image.resize( + (390, round(image.height * scale)), Image.Resampling.LANCZOS + ) + crop = mobile.crop(tuple(round(value * scale) for value in source_box)) + rows = [ + y + for y in range(crop.height) + if sum(max(crop.getpixel((x, y))) < 175 for x in range(crop.width)) >= 3 + ] + return max(rows) - min(rows) + 1 if rows else 0 + + +def _run_record( + status: str, + *, + manifest: Path | None = None, + assignment: tuple[bool, ...] | None = None, +) -> dict[str, object]: performed = status == "sat" checks = {} specifications = ( @@ -45,11 +86,14 @@ def _run_record(status: str) -> dict[str, object]: ("wang_z3_tiling", "oracles.tiling_check.is_valid_tiling"), ) for name, checker in specifications: + digest = "1" * 64 if performed else None + if name == "reference_assignment" and assignment is not None: + digest = _witness_digest(assignment) checks[name] = { "checker": checker, "performed": performed, "passed": True if performed else None, - "witness_sha256": "1" * 64 if performed else None, + "witness_sha256": digest, } agreement = { "expected_status": status, @@ -61,22 +105,44 @@ def _run_record(status: str) -> dict[str, object]: "sat_witnesses_valid": True if status == "sat" else None, "passed": True, } - payload = {"verification": checks, "agreement": agreement} - source_sha256 = hashlib.sha256( - (json.dumps(payload, ensure_ascii=False, allow_nan=False, indent=2) + "\n").encode( - "utf-8" + receipt_payload: dict[str, object] = { + "verification": checks, + "agreement": agreement, + } + source_payload = dict(receipt_payload) + if manifest is not None: + source = json.loads(manifest.read_text(encoding="utf-8")) + artifacts = source["artifacts"] + source_payload.update( + { + "source_formula": source["source_formula_sha256"], + "formula_snapshot": artifacts["formula"]["sha256"], + "tileset": artifacts["tileset"]["sha256"], + "region": artifacts["region"]["sha256"], + "provenance": artifacts["reduction"]["sha256"], + "reference_solution": ( + None + if artifacts["solution"] is None + else artifacts["solution"]["sha256"] + ), + "reference_assignment": ( + None if assignment is None else list(assignment) + ), + } ) + source_sha256 = hashlib.sha256( + _encoded(source_payload) ).hexdigest() return { "schema": "wang-verification-receipts-v1", "expected_status": status, - **payload, + **receipt_payload, "source_sha256": source_sha256, } def test_verification_composition_is_deterministic_for_sat_and_unsat(tmp_path): - for status in ("sat", "unsat"): + for status in ("unsat",): run = tmp_path / f"{status}.json" run.write_text(json.dumps(_run_record(status)) + "\n", encoding="utf-8") first = render_verification_assets(run, tmp_path / f"{status}-first") @@ -89,6 +155,177 @@ def test_verification_composition_is_deterministic_for_sat_and_unsat(tmp_path): assert animation.n_frames == 6 +def test_verification_shows_checker_rules_and_copied_native_extraction(tmp_path): + bundle = load_explainability_bundle(TRACE_MANIFEST) + presentation = load_wang_presentation(TRACE_SOLUTION) + tiling = getattr(wang_narrative, "_tiling_evidence")( + bundle, presentation + ) + assert ( + tiling.active_index, + tiling.inactive_index, + tiling.tile_id, + tiling.right_id, + tiling.tile_edges, + tiling.right_edges, + tiling.required_n, + tiling.maximum_tile_id, + ) == (0, 40, 0, 7, (0, 2, 7, 1), (0, 2, 0, 2), 0, 22) + extraction = getattr(wang_narrative, "_extraction_evidence")( + bundle, presentation, ASSIGNMENT + ) + assert tuple( + (item.variable, item.tile_ids, item.value) + for item in extraction + ) == ( + (0, (0, 1, 2), False), + (1, (3, 3, 3), True), + (2, (0, 1, 2), False), + ) + + receipts = tmp_path / "sat.json" + receipts.write_text( + json.dumps( + _run_record("sat", manifest=TRACE_MANIFEST, assignment=ASSIGNMENT) + ) + + "\n", + encoding="utf-8", + ) + first = render_verification_assets( + receipts, + tmp_path / "sat-first", + manifest_path=TRACE_MANIFEST, + solution_path=TRACE_SOLUTION, + extracted_assignment=ASSIGNMENT, + ) + render_verification_assets( + receipts, + tmp_path / "sat-second", + manifest_path=TRACE_MANIFEST, + solution_path=TRACE_SOLUTION, + extracted_assignment=ASSIGNMENT, + ) + assert _tree_bytes(tmp_path / "sat-first") == _tree_bytes( + tmp_path / "sat-second" + ) + assert first.fallback.name == "frame-05.png" + with Image.open(first.fallback) as fallback: + assert fallback.size == (1920, 1040) + + +def test_verification_rejects_cross_source_solution_and_assignment(tmp_path): + receipts = tmp_path / "sat.json" + receipts.write_text( + json.dumps( + _run_record("sat", manifest=TRACE_MANIFEST, assignment=ASSIGNMENT) + ) + + "\n", + encoding="utf-8", + ) + with pytest.raises(WangSquareRenderError, match="solution identity"): + render_verification_assets( + receipts, + tmp_path / "wrong-solution", + manifest_path=TRACE_MANIFEST, + solution_path=SOLUTION, + extracted_assignment=ASSIGNMENT, + ) + with pytest.raises(WangSquareRenderError, match="assignment identity"): + render_verification_assets( + receipts, + tmp_path / "wrong-assignment", + manifest_path=TRACE_MANIFEST, + solution_path=TRACE_SOLUTION, + extracted_assignment=(True, False, True), + ) + + +def test_verification_bounds_a_larger_copied_assignment(tmp_path): + receipts = tmp_path / "sat.json" + receipts.write_text( + json.dumps( + _run_record("sat", manifest=TRACE_MANIFEST, assignment=ASSIGNMENT) + ) + + "\n", + encoding="utf-8", + ) + status, records, bundle, presentation, _ = getattr( + wang_narrative, "_load_verification" + )( + receipts, + manifest_path=TRACE_MANIFEST, + solution_path=TRACE_SOLUTION, + extracted_assignment=ASSIGNMENT, + ) + assert bundle is not None and bundle.reduction is not None + source_gadgets = tuple( + gadget for gadget in bundle.reduction.gadgets if gadget.kind == "variable" + ) + gadgets = tuple( + replace(source_gadgets[index % 3], ordinal=index) for index in range(7) + ) + large_bundle = replace( + bundle, + formula=replace(bundle.formula, variable_count=7), + reduction=replace( + bundle.reduction, + variable_count=7, + gadgets=gadgets, + ), + ) + values = (False, True, False, True, False, True, False) + frame = getattr(wang_narrative, "_verification_frame")( + status, records, 5, large_bundle, presentation, values + ) + + assert getattr(wang_narrative, "_bounded_variable_indices")(7) == (0, 1, 6) + assert frame.size == (1920, 1040) + assert _mobile_ink_height(frame, (1470, 790, 1860, 890)) >= 8 + + +def test_unsat_summary_starts_below_all_receipt_labels(monkeypatch): + records = tuple(_run_record("unsat")["verification"].values()) + state_boxes: list[tuple[int, int, int, int]] = [] + summary_boxes: list[tuple[int, int, int, int]] = [] + original_draw = wang_narrative.ImageDraw.Draw + + class RecordingDraw: + def __init__(self, image): + self._draw = original_draw(image) + + def text(self, xy, value, **kwargs): + if value == "not applicable: no SAT witness": + state_boxes.append( + self._draw.textbbox( + xy, + value, + font=kwargs.get("font"), + anchor=kwargs.get("anchor"), + stroke_width=kwargs.get("stroke_width", 0), + ) + ) + return self._draw.text(xy, value, **kwargs) + + def rounded_rectangle(self, xy, **kwargs): + if xy[0] == 170 and xy[2] == 1750: + summary_boxes.append(tuple(xy)) + return self._draw.rounded_rectangle(xy, **kwargs) + + def __getattr__(self, name): + return getattr(self._draw, name) + + monkeypatch.setattr( + wang_narrative.ImageDraw, "Draw", lambda image: RecordingDraw(image) + ) + getattr(wang_narrative, "_verification_frame")( + "unsat", records, 5, None, None, None + ) + + assert len(state_boxes) == 6 + assert len(summary_boxes) == 1 + assert max(box[3] for box in state_boxes) + 24 <= summary_boxes[0][1] + + def test_verification_composition_rejects_partial_or_forged_receipts(tmp_path): source = tmp_path / "forged.json" document = _run_record("sat") @@ -105,11 +342,17 @@ def test_witness_and_generalized_assets_reuse_checked_presentations(tmp_path): tmp_path / "witness-second" ) assert first.animation.fallback.name == "frame-03.png" + with Image.open(first.animation.fallback) as fallback: + assert fallback.size == (1920, 1040) assert first.square.is_file() assert first.generalized.is_file() assert first.hex.is_file() generalized = render_generalized_assets(MANIFEST, tmp_path / "generalized") + render_generalized_assets(MANIFEST, tmp_path / "generalized-second") + assert _tree_bytes(tmp_path / "generalized") == _tree_bytes( + tmp_path / "generalized-second" + ) assert generalized.sheet.is_file() assert generalized.legend.is_file() assert generalized_specification_sha256() == ( @@ -117,6 +360,150 @@ def test_witness_and_generalized_assets_reuse_checked_presentations(tmp_path): ) +def test_atomic_legend_shows_canonical_valid_and_invalid_adjacency(tmp_path): + bundle = load_explainability_bundle(MANIFEST) + edges = bundle.tileset.tile_edges + + # Canonical horizontal examples: #0 E meets #4 W, while #0 E cannot + # meet #3 W. These literal values are from the checked fixture table. + assert edges[0][1] == edges[4][3] == 2 + assert edges[0][1] == 2 + assert edges[3][3] == 1 + + first = render_generalized_assets(MANIFEST, tmp_path / "first") + render_generalized_assets(MANIFEST, tmp_path / "second") + assert _tree_bytes(tmp_path / "first") == _tree_bytes(tmp_path / "second") + + with Image.open(first.legend) as legend: + assert legend.mode == "RGB" + assert legend.size == (1732, 4184) + # Valid pair #0/#4 has the same brown logical-color band on both + # sides of its gap; invalid pair #0/#3 has brown versus magenta. + assert legend.getpixel((216, 3900)) == legend.getpixel((252, 3900)) == ( + 142, 92, 25 + ) + assert legend.getpixel((1062, 3900)) == (142, 92, 25) + assert legend.getpixel((1098, 3900)) == (240, 36, 160) + + +def test_atomic_vocabulary_remains_readable_at_390_px(tmp_path): + outputs = render_generalized_assets(MANIFEST, tmp_path / "generalized") + with Image.open(outputs.legend) as source: + scale = 390 / source.width + display = source.resize( + (390, round(source.height * scale)), Image.Resampling.LANCZOS + ) + # The first card's semantic role and edge rows must survive the actual + # mobile-width downsample; three dark pixels per row filters borders. + for source_box in ((184, 164, 790, 288), (184, 330, 790, 390)): + box = tuple(round(value * scale) for value in source_box) + crop = display.crop(box) + ink_rows = [ + y + for y in range(crop.height) + if sum( + max(crop.getpixel((x, y))) < 210 for x in range(crop.width) + ) >= 3 + ] + runs: list[list[int]] = [] + for row in ink_rows: + if not runs or row != runs[-1][-1] + 1: + runs.append([row]) + else: + runs[-1].append(row) + assert max((len(run) for run in runs), default=0) >= 8 + + +def test_home_preview_retains_native_detail_at_twice_its_pages_display_width(): + css = (ROOT / "docs/assets/css/site.css").read_text(encoding="utf-8") + home_rule = re.search( + r'\.narrative-asset\[data-asset-id="home_preview"\]\s*\{([^}]+)\}', + css, + ) + assert home_rule is not None + display_limit = re.search(r"max-width:\s*(\d+)px", home_rule.group(1)) + assert display_limit is not None + display_width = int(display_limit.group(1)) + + # Match the actual validated square source dimensions. Fine color detail + # exposes a low-resolution intermediate enlarged into a bigger canvas. + square = Image.new("RGB", (1538, 422)) + draw = ImageDraw.Draw(square) + for x in range(square.width): + draw.line( + (x, 0, x, square.height - 1), + fill=((x * 73) % 256, (x * 29) % 256, (x * 13) % 256), + ) + preview = wang_narrative._home_preview(square) + assert preview.width >= 2 * display_width + + # The witness spans the display minus 20 px of margin on each side, at + # two source pixels per CSS pixel. Compare those pixels with a direct + # high-quality downsample, so upscaling the old 720 px witness cannot pass. + expected = square.copy() + expected.thumbnail( + (2 * (display_width - 40), square.height), + resample=Image.Resampling.LANCZOS, + ) + left = (preview.width - expected.width) // 2 + top = 164 + assert preview.crop( + (left, top, left + expected.width, top + expected.height) + ).tobytes() == expected.tobytes() + + +def test_worked_example_keeps_overview_and_expands_selected_case_panels( + tmp_path, +): + colors = ( + (180, 30, 60), + (30, 160, 70), + (50, 80, 190), + (200, 120, 20), + (130, 50, 180), + (20, 150, 160), + (220, 70, 30), + (90, 120, 40), + ) + source_paths = [] + for index, color in enumerate(colors): + path = tmp_path / f"source-{index}.png" + Image.new("RGB", (1920, 1040), color).save(path) + source_paths.append(path) + square_color = (40, 120, 220) + square = tmp_path / "square.png" + Image.new("RGB", (1538, 422), square_color).save(square) + + outputs = render_overview_assets( + tuple(source_paths), square, tmp_path / "overview" + ) + assert outputs.worked_example is not None + with Image.open(outputs.worked_example) as source: + mobile = source.resize( + (390, round(source.height * 390 / source.width)), + Image.Resampling.LANCZOS, + ) + + def color_span(color): + columns = [ + x + for y in range(mobile.height) + for x in range(mobile.width) + if all( + abs(channel - expected) <= 2 + for channel, expected in zip(mobile.getpixel((x, y)), color) + ) + ] + return max(columns) - min(columns) + 1 if columns else 0 + + # Every source remains in the compact eight-stage overview. The selected + # decision, construction, checker, square, and final-presentation panels + # additionally occupy nearly the full mobile width. + assert all(color_span(color) > 0 for color in colors) + for color in (colors[1], colors[2], colors[6], square_color, colors[7]): + assert color_span(color) >= 350 + + def test_overview_and_unsat_status_are_static_fallback_safe(tmp_path): status = render_presentation_status("unsat", tmp_path / "status.png") sources = (status,) * 8 diff --git a/renderer/test_wang_trace.py b/renderer/test_wang_trace.py index cde4d9d..c242405 100644 --- a/renderer/test_wang_trace.py +++ b/renderer/test_wang_trace.py @@ -8,19 +8,29 @@ import subprocess import sys -from PIL import Image +from PIL import Image, ImageDraw import pytest +import wang_trace_render +from wang_explain import ( + EXPLAIN_DECISION_RGB, + EXPLAIN_PROPAGATION_SOURCE_RGB, + EXPLAIN_SELECTED_MRV_RGB, + EXPLAIN_UNRESOLVED_RGB, +) from wang_hex_port import WangSquareRenderError from wang_trace import TraceEvent, TraceSnapshot, load_trace_bundle, replay_trace -from wang_trace_render import render_trace_assets, select_semantic_milestones +from wang_trace_render import ( + _active_domain_counts, + render_trace_assets, + select_semantic_milestones, +) RENDERER = Path(__file__).resolve().parent ROOT = RENDERER.parent FIXTURE_DIRECTORY = ROOT / "tests/fixtures/pipeline_sat_solver_trace" MANIFEST = FIXTURE_DIRECTORY / "manifest.json" -GOLDENS = ROOT / "docs/assets/narrative/reference-trace" def _tree_bytes(directory: Path) -> dict[str, bytes]: @@ -84,6 +94,62 @@ def _small_trace(): ) +def _display_ink_height(image: Image.Image, box: tuple[int, int, int, int]) -> int: + display_width = 390 + scale = display_width / image.width + display = image.resize( + (display_width, round(image.height * scale)), Image.Resampling.LANCZOS + ) + display_box = tuple(round(coordinate * scale) for coordinate in box) + crop = display.crop(display_box) + ink_rows = [ + y + for y in range(crop.height) + if sum( + max(crop.getpixel((x, y))) < 210 for x in range(crop.width) + ) + >= 3 + ] + runs: list[list[int]] = [] + for row in ink_rows: + if not runs or row != runs[-1][-1] + 1: + runs.append([row]) + else: + runs[-1].append(row) + return max((len(run) for run in runs), default=0) + + +def _search_story_panel(bundle, event_index, restored=()): + events = ( + TraceEvent(0, "root", "initial", None, 0, None, 0, None, None, None), + TraceEvent(1, "decision", "search", None, 2, 492, 3990, 9, 1, None), + TraceEvent(2, "conflict", "search", None, 2, 614, 4114, None, None, None), + TraceEvent(3, "backtrack", "search", None, 2, 492, 3990, None, None, None), + TraceEvent(4, "decision", "search", None, 2, 492, 3990, 9, 8, None), + ) + trace = replace( + bundle.trace, + events=events, + event_capacity=len(events), + observed_event_count=len(events), + ) + story_bundle = replace(bundle, trace=trace) + image = Image.new("RGB", (1976, 972), (255, 255, 255)) + draw_story = getattr(wang_trace_render, "_draw_search_summary", None) + assert draw_story is not None + draw_story( + ImageDraw.Draw(image), + story_bundle, + events[event_index], + event_index, + restored, + top=744, + width=image.width, + height=image.height, + ) + return image + + def test_loads_and_replays_hash_bound_trace_without_solver_imports(): bundle = load_trace_bundle(MANIFEST) @@ -103,27 +169,165 @@ def test_one_composition_chain_is_byte_stable_for_png_sheet_and_gif(tmp_path): 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) == 10 assert first.fallback.name == "frame-002517.png" assert first.animation.name == "trace.gif" assert first.contact_sheet.name == "contact-sheet.png" with Image.open(first.frames[0]) as frame: assert frame.mode == "RGB" - assert frame.size == (988, 414) + assert frame.size == (1976, 828) with Image.open(first.animation) as animation: assert animation.format == "GIF" assert animation.n_frames == 10 -def test_semantic_milestones_precede_gap_filling(): +def test_observed_mrv_selection_is_row_major_and_deterministic(tmp_path): + bundle = load_trace_bundle(MANIFEST) + states = replay_trace(bundle.trace) + decision_index, event = next( + (index, event) + for index, event in enumerate(bundle.trace.events) + if event.kind == "decision" and event.phase == "search" + ) + before = states[decision_index - 1] + region = bundle.explanation.region + minimum = min( + domain.bit_count() + for active, domain in zip(region.active, before, strict=True) + if active and domain.bit_count() > 1 + ) + candidates = tuple( + index + for index, (active, domain) in enumerate(zip(region.active, before)) + if active and domain.bit_count() == minimum + ) + + assert event.cell == min(candidates) + + first_dir = tmp_path / "first" + second_dir = tmp_path / "second" + first = render_trace_assets(MANIFEST, first_dir, max_frames=10) + render_trace_assets(MANIFEST, second_dir, max_frames=10) + + assert _tree_bytes(first_dir) == _tree_bytes(second_dir) + assert Image.open(first.fallback).size == (1976, 828) + + +def test_active_domain_counts_exclude_inactive_positions(): + bundle = load_trace_bundle(MANIFEST) + states = replay_trace(bundle.trace) + decision_index = next( + index + for index, event in enumerate(bundle.trace.events) + if event.kind == "decision" and event.phase == "search" + ) + assert _active_domain_counts( + bundle.explanation.region.active, states[decision_index - 1] + ) == (74, 0) + + +def test_mrv_legend_uses_the_unresolved_grid_color(tmp_path): + rendered = render_trace_assets(MANIFEST, tmp_path / "rendered", max_frames=10) + with Image.open(rendered.fallback) as fallback: + assert fallback.getpixel((1548, 304)) == EXPLAIN_UNRESOLVED_RGB + + +def test_decision_fallback_has_large_focused_mrv_summary_cards(tmp_path): + rendered = render_trace_assets(MANIFEST, tmp_path / "rendered", max_frames=10) + with Image.open(rendered.fallback) as fallback: + assert fallback.getpixel((1630, 660)) == EXPLAIN_SELECTED_MRV_RGB + assert fallback.getpixel((1804, 660)) == EXPLAIN_DECISION_RGB + + +def test_sat_selection_keeps_a_decision_restriction_and_its_continuation(): bundle = load_trace_bundle(MANIFEST) selected = select_semantic_milestones(bundle.trace.events, 10) + # Hand-checked contiguous search events: select cell 0, restrict it, + # then remove tile 8 from its neighbor cell 1. + assert {2517, 2518, 2519, 2894, 2895} <= set(selected) + assert selected == tuple(sorted(set(selected))) + + +def test_propagation_reason_uses_unique_shared_edge_in_observed_before_state(): + bundle = load_trace_bundle(MANIFEST) + before = replay_trace(bundle.trace)[2518] + reason = getattr(wang_trace_render, "_propagation_reason", None) + assert reason is not None, "the observed reduction needs a derived edge reason" + assert reason(bundle, bundle.trace.events[2519], before) == (0, "E", "W", (2,)) + + +def test_propagation_frame_marks_the_uniquely_derived_source(tmp_path): + rendered = render_trace_assets(MANIFEST, tmp_path / "rendered", max_frames=10) + propagation = tmp_path / "rendered/frame-002519.png" + assert propagation in rendered.frames + with Image.open(propagation) as frame: + assert frame.getpixel((30, 182)) == EXPLAIN_PROPAGATION_SOURCE_RGB + + +def test_trace_story_facts_remain_readable_at_390_px(tmp_path): + bundle = load_trace_bundle(MANIFEST) + rendered = render_trace_assets(MANIFEST, tmp_path / "rendered", max_frames=10) + propagation = tmp_path / "rendered/frame-002519.png" + assert propagation in rendered.frames + with Image.open(propagation) as frame: + assert _display_ink_height(frame, (52, 676, 1400, 734)) >= 8 + assert _display_ink_height(frame, (52, 726, 1400, 784)) >= 8 + + conflict = _search_story_panel(bundle, 2) + assert _display_ink_height(conflict, (52, 828, 1400, 900)) >= 8 + + rollback = _search_story_panel( + bundle, + 3, + ((614, 0, 1 << 8), (614, 1 << 8, (1 << 6) | (1 << 8))), + ) + assert _display_ink_height(rollback, (52, 820, 1400, 884)) >= 8 + assert _display_ink_height(rollback, (52, 880, 1400, 944)) >= 8 - assert selected == (0, 1, 1258, 1887, 2516, 2517, 2518, 2893, 2894, 2895) - assert selected != tuple( - slot * (len(bundle.trace.events) - 1) // 9 for slot in range(10) + +def test_ambiguous_propagation_source_is_not_presented_as_observed(): + bundle = load_trace_bundle(MANIFEST) + before = list(replay_trace(bundle.trace)[2518]) + # Both west cell 0 and east cell 2 now independently imply {7,8}->{7}. + before[2] = 128 + reason = getattr(wang_trace_render, "_propagation_reason", None) + assert reason is not None, "ambiguous sources must remain unidentified" + assert reason(bundle, bundle.trace.events[2519], tuple(before)) is None + + +def test_rollback_focus_restores_repeated_changes_in_reverse_trail_order(): + trace = _small_trace() + events = trace.events[:5] + ( + TraceEvent( + 5, "domain_reduction", "search", "propagation", 1, 1, 3, 3, 2, None + ), + TraceEvent( + 6, "domain_reduction", "search", "propagation", 1, 1, 4, 2, 0, None + ), + TraceEvent(7, "conflict", "search", None, 1, 1, 4, None, None, None), + TraceEvent(8, "backtrack", "search", None, 1, 0, 1, None, None, None), + TraceEvent(9, "result", None, None, 0, 1, 1, None, None, "unsat"), + ) + trace = replace( + trace, + width=2, + initial_domains=((1 << 23) - 1, 3), + events=events, + status="unsat", + solution_sha256=None, + event_capacity=10, + observed_event_count=10, ) + assert replay_trace(trace)[8] == (3, 3) + restore = getattr(wang_trace_render, "_restored_changes", None) + assert restore is not None, "rollback focus needs the reversed observed deltas" + assert restore(events, 8) == ((1, 0, 2), (1, 2, 3), (0, 1, 3)) + + +def test_tall_search_grid_retains_room_for_the_rollback_story(): + frame_height = getattr(wang_trace_render, "_frame_height", None) + assert frame_height is not None, "tall traces need a visible story panel" + assert frame_height(15 * 18 * 2) == 972 def test_rejects_hash_tampering_before_parsing_trace(tmp_path): diff --git a/renderer/test_wang_z3_summary.py b/renderer/test_wang_z3_summary.py index f3fa5fc..f2acb4b 100644 --- a/renderer/test_wang_z3_summary.py +++ b/renderer/test_wang_z3_summary.py @@ -1,24 +1,29 @@ from __future__ import annotations import json +from dataclasses import replace from pathlib import Path +import shutil import sys from PIL import Image import pytest +import wang_z3_summary from wang_hex_port import WangSquareRenderError from wang_z3_summary import ( load_z3_encoding_summary, render_boolean_z3_assets, render_wang_z3_assets, ) +from wang_snapshot import load_explainability_bundle RENDERER = Path(__file__).resolve().parent ROOT = RENDERER.parent FIXTURES = ROOT / "tests/fixtures/pipeline_sat_z3" GOLDENS = ROOT / "docs/assets/narrative" +MANIFEST = ROOT / "tests/fixtures/pipeline_sat_reduction_explain/manifest.json" def _tree_bytes(directory: Path) -> dict[str, bytes]: @@ -29,6 +34,22 @@ def _tree_bytes(directory: Path) -> dict[str, bytes]: } +def _mobile_ink_height( + image: Image.Image, source_box: tuple[int, int, int, int] +) -> int: + scale = 390 / image.width + mobile = image.resize( + (390, round(image.height * scale)), Image.Resampling.LANCZOS + ) + crop = mobile.crop(tuple(round(value * scale) for value in source_box)) + rows = [ + y + for y in range(crop.height) + if sum(max(crop.getpixel((x, y))) < 175 for x in range(crop.width)) >= 3 + ] + return max(rows) - min(rows) + 1 if rows else 0 + + def test_loads_both_closed_summaries_without_z3_or_native_imports(): boolean = load_z3_encoding_summary(FIXTURES / "boolean-z3.json") wang = load_z3_encoding_summary(FIXTURES / "wang-z3.json") @@ -44,32 +65,235 @@ def test_loads_both_closed_summaries_without_z3_or_native_imports(): assert not any(name.startswith("native") for name in sys.modules) -def test_encoding_order_animation_is_byte_stable_and_matches_goldens(tmp_path): +def test_wang_encoding_uses_real_cell_term_tuple_boundary_and_model(tmp_path): source = FIXTURES / "wang-z3.json" - first = render_wang_z3_assets(source, tmp_path / "first") - render_wang_z3_assets(source, tmp_path / "second") + summary = load_z3_encoding_summary(source) + bundle = load_explainability_bundle(MANIFEST) + + evidence = getattr(wang_z3_summary, "_wang_example_evidence")( + summary, bundle + ) + assert ( + evidence.x, + evidence.y, + evidence.tile_id, + evidence.right_id, + evidence.tile_edges, + evidence.right_edges, + evidence.required_n, + ) == (0, 0, 0, 7, (0, 2, 7, 1), (0, 2, 0, 2), 0) + + frame = getattr(wang_z3_summary, "_compose_wang_frame")(summary, bundle, 4) + changed_tile = replace( + bundle, + tileset=replace( + bundle.tileset, + tile_edges=((0, 2, 9, 1), *bundle.tileset.tile_edges[1:]), + ), + ) + assert frame.tobytes() != getattr(wang_z3_summary, "_compose_wang_frame")( + summary, changed_tile, 4 + ).tobytes() + + first = render_wang_z3_assets(source, MANIFEST, tmp_path / "first") + render_wang_z3_assets(source, MANIFEST, tmp_path / "second") assert _tree_bytes(tmp_path / "first") == _tree_bytes(tmp_path / "second") - assert _tree_bytes(tmp_path / "first") == _tree_bytes(GOLDENS / "wang-z3") - assert first.fallback.name == "frame-03.png" + assert first.fallback.name == "frame-04.png" + with Image.open(first.fallback) as fallback: + assert fallback.size == (1880, 1040) with Image.open(first.animation) as animation: assert animation.format == "GIF" assert animation.n_frames == 5 -def test_boolean_encoding_order_animation_is_byte_stable(tmp_path): +def test_boolean_encoding_uses_source_occurrences_and_copied_assignment(tmp_path): source = FIXTURES / "boolean-z3.json" - first = render_boolean_z3_assets(source, tmp_path / "first") - render_boolean_z3_assets(source, tmp_path / "second") + summary = load_z3_encoding_summary(source) + bundle = load_explainability_bundle(MANIFEST) + assert getattr(wang_z3_summary, "_boolean_clause_lines")(bundle) == ( + ("c0 source positions: x0, x0, x1", "If(x0) + If(x0) + If(x1) = 1"), + ("c1 source positions: x0, x1, x2", "If(x0) + If(x1) + If(x2) = 1"), + ("c2 source positions: x1, x2, x2", "If(x1) + If(x2) + If(x2) = 1"), + ) + + frame = getattr(wang_z3_summary, "_compose_boolean_frame")(summary, bundle, 3) + changed_formula = replace( + bundle, + formula=replace( + bundle.formula, + clauses=((0, 1, 0), *bundle.formula.clauses[1:]), + ), + ) + changed_summary = replace(summary, assignment=(True, False, True)) + assert frame.tobytes() != getattr(wang_z3_summary, "_compose_boolean_frame")( + summary, changed_formula, 3 + ).tobytes() + assert frame.tobytes() != getattr(wang_z3_summary, "_compose_boolean_frame")( + changed_summary, bundle, 3 + ).tobytes() + + first = render_boolean_z3_assets(source, MANIFEST, tmp_path / "first") + render_boolean_z3_assets(source, MANIFEST, 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" + assert first.fallback.name == "frame-03.png" + with Image.open(first.fallback) as fallback: + assert fallback.size == (1880, 1040) with Image.open(first.animation) as animation: assert animation.format == "GIF" assert animation.n_frames == 4 +def test_oracle_fallback_core_labels_remain_readable_at_390_px(): + bundle = load_explainability_bundle(MANIFEST) + boolean = load_z3_encoding_summary(FIXTURES / "boolean-z3.json") + wang = load_z3_encoding_summary(FIXTURES / "wang-z3.json") + boolean_frame = getattr(wang_z3_summary, "_compose_boolean_frame")( + boolean, bundle, 3 + ) + wang_frame = getattr(wang_z3_summary, "_compose_wang_frame")( + wang, bundle, 4 + ) + + assert _mobile_ink_height(boolean_frame, (1040, 350, 1800, 430)) >= 8 + assert _mobile_ink_height(boolean_frame, (340, 884, 1540, 940)) >= 8 + assert _mobile_ink_height(wang_frame, (70, 770, 850, 850)) >= 8 + assert _mobile_ink_height(wang_frame, (990, 735, 1770, 860)) >= 9 + + +def test_wang_unsat_frame_visibly_marks_cell_and_model_as_not_applicable(tmp_path): + frames = {} + for status in ("unsat", "unknown"): + document = json.loads( + (FIXTURES / "wang-z3.json").read_text(encoding="utf-8") + ) + document["status"] = status + document["model"]["cells"] = None + document["statistics"][-1]["value"] = 0 + source = tmp_path / f"wang-{status}.json" + source.write_text(json.dumps(document) + "\n", encoding="utf-8") + output = render_wang_z3_assets( + source, MANIFEST, tmp_path / status + ) + with Image.open(output.fallback) as fallback: + frames[status] = fallback.copy() + + # These crops were blank in the SAT-only composition. They cover the body + # of the two panels where the explicit non-SAT/N/A explanation appears. + assert _mobile_ink_height(frames["unsat"], (110, 390, 870, 670)) >= 8 + assert _mobile_ink_height(frames["unsat"], (1020, 390, 1780, 670)) >= 8 + # UNKNOWN remains a distinct supported result rather than being mislabeled + # as UNSAT. + assert frames["unsat"].tobytes() != frames["unknown"].tobytes() + + +def test_boolean_fallback_bounds_a_large_source_formula(): + bundle = load_explainability_bundle(MANIFEST) + clauses = tuple((variable, variable, variable) for variable in range(44)) + large_bundle = replace( + bundle, + formula=replace(bundle.formula, variable_count=44, clauses=clauses), + ) + summary = replace( + load_z3_encoding_summary(FIXTURES / "boolean-z3.json"), + variable_count=44, + assertion_count=44, + assignment=(False,) * 44, + ) + frame = getattr(wang_z3_summary, "_compose_boolean_frame")( + summary, large_bundle, 3 + ) + changed_last = replace( + large_bundle, + formula=replace( + large_bundle.formula, + clauses=(*clauses[:-1], (43, 42, 43)), + ), + ) + + assert frame.size == (1880, 1040) + assert frame.tobytes() != getattr(wang_z3_summary, "_compose_boolean_frame")( + summary, changed_last, 3 + ).tobytes() + changed_assignment = replace( + summary, + assignment=(*summary.assignment[:-1], True), + ) + assert frame.tobytes() != getattr(wang_z3_summary, "_compose_boolean_frame")( + changed_assignment, large_bundle, 3 + ).tobytes() + + +def test_boolean_fallback_separates_omission_note_from_heading_and_rows( + monkeypatch, +): + bundle = load_explainability_bundle(MANIFEST) + clauses = tuple((variable, variable, variable) for variable in range(44)) + large_bundle = replace( + bundle, + formula=replace(bundle.formula, variable_count=44, clauses=clauses), + ) + summary = replace( + load_z3_encoding_summary(FIXTURES / "boolean-z3.json"), + variable_count=44, + assertion_count=44, + assignment=(False,) * 44, + ) + text_boxes: dict[str, tuple[int, int, int, int]] = {} + row_tops: list[int] = [] + original_draw = wang_z3_summary.ImageDraw.Draw + + class RecordingDraw: + def __init__(self, image): + self._draw = original_draw(image) + + def text(self, xy, value, **kwargs): + text_boxes[str(value)] = self._draw.textbbox( + xy, + value, + font=kwargs.get("font"), + anchor=kwargs.get("anchor"), + stroke_width=kwargs.get("stroke_width", 0), + ) + return self._draw.text(xy, value, **kwargs) + + def rounded_rectangle(self, xy, **kwargs): + if xy[0] == 72 and xy[2] == 800: + row_tops.append(xy[1]) + return self._draw.rounded_rectangle(xy, **kwargs) + + def __getattr__(self, name): + return getattr(self._draw, name) + + monkeypatch.setattr( + wang_z3_summary.ImageDraw, "Draw", lambda image: RecordingDraw(image) + ) + getattr(wang_z3_summary, "_compose_boolean_frame")( + summary, large_bundle, 3 + ) + + heading = text_boxes["Actual sum asserted equal to one"] + omission = text_boxes[ + "41 source clauses omitted between c1 and c43" + ] + assert heading[3] + 8 <= omission[1] + assert omission[3] + 8 <= min(row_tops) + + +def test_oracle_composition_rejects_cross_source_substitution(tmp_path): + source = FIXTURES / "boolean-z3.json" + copied = tmp_path / "bundle" + shutil.copytree(MANIFEST.parent, copied) + path = copied / "manifest.json" + forged = json.loads(path.read_text(encoding="utf-8")) + forged["source_formula_sha256"] = "0" * 64 + path.write_text(json.dumps(forged) + "\n", encoding="utf-8") + + with pytest.raises(WangSquareRenderError, match="source_formula_sha256"): + render_boolean_z3_assets(source, path, tmp_path / "output") + + def test_rejects_unknown_fields_and_cross_engine_region_identity(tmp_path): source = json.loads( (FIXTURES / "boolean-z3.json").read_text(encoding="utf-8") diff --git a/renderer/wang_algorithm_animation.py b/renderer/wang_algorithm_animation.py index 828ed3a..e24f347 100644 --- a/renderer/wang_algorithm_animation.py +++ b/renderer/wang_algorithm_animation.py @@ -3,23 +3,31 @@ from __future__ import annotations import argparse +from dataclasses import dataclass import json from pathlib import Path +import textwrap from PIL import Image, ImageDraw from wang_animation import AnimationOutputs, write_animation_assets from wang_explain import ( EXPLAIN_ACTIVE_RGB, + EXPLAIN_INACTIVE_DARK_RGB, + EXPLAIN_INACTIVE_LIGHT_RGB, EXPLAIN_MUTED_RGB, EXPLAIN_PANEL_RGB, + EXPLAIN_RENDER_SCALE, EXPLAIN_TEXT_RGB, + centered_text, draw_explain_heading, explain_font, + square_inactive_tile, + square_region_tile, ) from wang_hex_port import WangSquareRenderError, check_square_to_hex, reduce_square_to_hex -from wang_snapshot import load_explainability_bundle -from wang_square import load_wang_presentation +from wang_snapshot import ReductionExplanationSnapshot, load_explainability_bundle +from wang_square import _build_palette_from_edges, load_wang_presentation _GADGET_COLORS = { @@ -30,9 +38,25 @@ "clause": (214, 91, 91), } _OPTIMIZATION_SOURCE = Path(__file__).resolve().parent / "data/optimized-mechanisms-v1.json" +_OPTIMIZATION_IDS = ( + "dynamic-dfs-stack", + "initial-trail-omission", + "sat-ownership-transfer", + "byte-support-table", + "queue-deduplication", + "lazy-mrv-index", +) + + +@dataclass(frozen=True, slots=True) +class _Optimization: + identifier: str + title: str + description: str + evidence_route: str -def _load_optimizations() -> tuple[tuple[str, str], ...]: +def _load_optimizations() -> tuple[_Optimization, ...]: try: document = json.loads(_OPTIMIZATION_SOURCE.read_text(encoding="utf-8")) except (OSError, UnicodeError, json.JSONDecodeError) as error: @@ -46,7 +70,7 @@ def _load_optimizations() -> tuple[tuple[str, str], ...]: mechanisms = document["mechanisms"] if type(mechanisms) is not list or len(mechanisms) != 6: raise WangSquareRenderError("optimized mechanism source must contain six entries") - result: list[tuple[str, str]] = [] + result: list[_Optimization] = [] identifiers: list[str] = [] for index, item in enumerate(mechanisms): if type(item) is not dict or set(item) != { @@ -68,8 +92,15 @@ def _load_optimizations() -> tuple[tuple[str, str], ...]: f"optimized mechanism entry {index} has an invalid evidence route" ) identifiers.append(item["id"]) - result.append((item["title"], item["description"])) - if len(set(identifiers)) != len(identifiers) or identifiers[-1] != "lazy-mrv-index": + result.append( + _Optimization( + identifier=item["id"], + title=item["title"], + description=item["description"], + evidence_route=item["evidence_route"], + ) + ) + if tuple(identifiers) != _OPTIMIZATION_IDS: raise WangSquareRenderError("optimized mechanism IDs are invalid or incomplete") return tuple(result) @@ -84,65 +115,367 @@ def _base_frame(title: str, subtitle: str, size: tuple[int, int]) -> tuple[Image return image, draw +def _builder_signal_label(signal: object, *, compact: bool) -> str: + if signal.kind == "redundant": + return f"r #{signal.token_id}" + if compact: + return f"#{signal.token_id}" + return f"x{signal.variable}.{signal.occurrence}" + + +def _replay_signal_orders( + reduction: ReductionExplanationSnapshot, +) -> tuple[tuple[object, ...], ...]: + """Project the loader-validated adjacent swaps for presentation.""" + current = list(reduction.source_signals) + orders = [tuple(current)] + for crossover in ( + gadget for gadget in reduction.gadgets if gadget.kind == "crossover" + ): + assert crossover.swap_row is not None + row = crossover.swap_row + current[row], current[row + 1] = current[row + 1], current[row] + orders.append(tuple(current)) + return tuple(orders) + + +def _signal_strip_items( + signals: tuple[object, ...], + highlighted_rows: tuple[int, ...], +) -> tuple[tuple[int | None, object | None, int], ...]: + """Keep bounded endpoint/swap context and account for every hidden row.""" + if len(signals) <= 15: + return tuple((row, signal, 0) for row, signal in enumerate(signals)) + + selected = {0, 1, 2, len(signals) - 3, len(signals) - 2, len(signals) - 1} + for row in highlighted_rows: + selected.update( + candidate + for candidate in (row - 1, row, row + 1) + if 0 <= candidate < len(signals) + ) + ordered = sorted(selected) + items: list[tuple[int | None, object | None, int]] = [] + previous = -1 + for row in ordered: + omitted = row - previous - 1 + if omitted: + items.append((None, None, omitted)) + items.append((row, signals[row], 0)) + previous = row + trailing = len(signals) - previous - 1 + if trailing: + items.append((None, None, trailing)) + return tuple(items) + + +def _draw_signal_order( + draw: ImageDraw.ImageDraw, + *, + y: int, + label: str, + signals: tuple[object, ...], + highlighted_rows: tuple[int, ...] = (), + muted: bool = False, +) -> None: + scale = EXPLAIN_RENDER_SCALE + draw.text( + (36, y + 12), + label, + font=explain_font(22 * scale), + fill=EXPLAIN_MUTED_RGB if muted else EXPLAIN_TEXT_RGB, + ) + items = _signal_strip_items(signals, highlighted_rows) + gap = 10 + box_width = min( + 140, + (1720 - max(0, len(items) - 1) * gap) // len(items), + ) + for position, (row, signal, omitted) in enumerate(items): + x = 220 + position * (box_width + gap) + highlighted = row in highlighted_rows + draw.rounded_rectangle( + (x, y, x + box_width, y + 58), + radius=8, + fill=(255, 232, 188) if highlighted else (239, 242, 246), + outline=(217, 119, 6) if highlighted else (181, 188, 199), + width=4 if highlighted else 2, + ) + text = ( + f"+{omitted} rows" + if signal is None + else _builder_signal_label(signal, compact=box_width < 120) + ) + font_size = 16 if signal is None else 28 + font = explain_font(font_size * scale) + if len(signals) > 15: + inner_width = box_width - 8 + while font_size > 12: + text_box = draw.textbbox((0, 0), text, font=font) + if text_box[2] - text_box[0] <= inner_width: + break + font_size -= 1 + font = explain_font(font_size * scale) + centered_text( + draw, + (x + 4, y + 3, x + box_width - 4, y + 55), + text, + font=font, + fill=( + EXPLAIN_MUTED_RGB + if muted or signal is None + else EXPLAIN_TEXT_RGB + ), + ) + + def _builder_frame(bundle: object, stage: int) -> Image.Image: reduction = bundle.reduction assert reduction is not None + crossovers = tuple( + gadget for gadget in reduction.gadgets if gadget.kind == "crossover" + ) + if crossovers: + first_swap = crossovers[0] + assert first_swap.swap_row is not None + first_swap_title = ( + f"crossover X{first_swap.ordinal} swaps adjacent rows " + f"{first_swap.swap_row} and {first_swap.swap_row + 1}" + ) + routing_title = ( + f"{len(crossovers)} validated adjacent swaps reach the target order" + ) + else: + first_swap_title = "source order already matches the target order" + routing_title = "routing requires no crossover swaps" + stage_titles = ( + "source signals leave the variable gadgets", + "target signals follow clause order", + first_swap_title, + routing_title, + "native gadget spans assemble the final Region", + "active, inactive, internal-edge, and exposed-boundary states", + ) image, draw = _base_frame( - "Yang-Zhang construction provenance", - f"canonical-construction stage {stage + 1}/6 | actual gadget spans, not a timed builder trace", - (980, 390), + "Yang-Zhang routing and Region construction", + f"canonical-construction {stage + 1}/6 | {stage_titles[stage]}", + (1976, 828), + ) + # _base_frame uses the legacy 1x heading; redraw the shared heading at 2x. + draw.rectangle((0, 0, image.width, 126), fill=EXPLAIN_PANEL_RGB) + draw_explain_heading( + draw, + (36, 28), + title="Yang-Zhang routing and Region construction", + subtitle=f"canonical-construction {stage + 1}/6 | {stage_titles[stage]}", + scale=EXPLAIN_RENDER_SCALE, ) - origin_x, origin_y, cell = 18, 92, 15 + + replay_orders = _replay_signal_orders(reduction) + first_swap_row = crossovers[0].swap_row if crossovers else None + _draw_signal_order( + draw, + y=140, + label="source", + signals=reduction.source_signals, + highlighted_rows=( + (first_swap_row, first_swap_row + 1) + if stage == 2 and first_swap_row is not None + else () + ), + ) + if stage == 0: + _draw_signal_order( + draw, + y=216, + label="target", + signals=reduction.target_signals, + muted=True, + ) + elif stage == 2: + _draw_signal_order( + draw, + y=216, + label=f"after X{crossovers[0].ordinal}" if crossovers else "target", + signals=replay_orders[1] if crossovers else reduction.target_signals, + highlighted_rows=( + (first_swap_row, first_swap_row + 1) + if first_swap_row is not None + else () + ), + ) + else: + _draw_signal_order( + draw, + y=216, + label="target", + signals=reduction.target_signals, + ) + + origin_x, origin_y = 36, 348 + cell = max(1, min( + 30, + 1230 // bundle.region.width, + 330 // bundle.region.height, + )) grid_width = bundle.region.width * cell grid_height = bundle.region.height * cell + palette = _build_palette_from_edges(bundle.tileset.tile_edges) for index, active in enumerate(bundle.region.active): x = origin_x + (index % bundle.region.width) * cell y = origin_y + (index // bundle.region.width) * cell - fill = (232, 235, 240) if active else (198, 204, 214) - draw.rectangle((x, y, x + cell - 1, y + cell - 1), fill=fill, outline=(187, 193, 203)) - - visible_kinds = ( - (), - ("variable",), - ("variable", "left_forward"), - ("variable", "left_forward", "crossover"), - ("variable", "left_forward", "crossover", "right_forward"), - tuple(_GADGET_COLORS), - )[stage] + if stage >= 4: + if active: + sides = bundle.region.boundary[index] + assert sides is not None + tile = square_region_tile(cell, sides, palette) + else: + tile = square_inactive_tile(cell) + image.paste(tile, (x, y)) + else: + fill = EXPLAIN_ACTIVE_RGB if active else EXPLAIN_INACTIVE_LIGHT_RGB + draw.rectangle( + (x, y, x + cell - 1, y + cell - 1), + fill=fill, + outline=(174, 181, 193), + ) + for gadget in reduction.gadgets: - if gadget.kind not in visible_kinds: + visible = ( + (stage == 0 and gadget.kind == "variable") + or (stage == 1 and gadget.kind in {"variable", "left_forward"}) + or ( + stage == 2 + and ( + gadget.kind in {"variable", "left_forward"} + or (crossovers and gadget is crossovers[0]) + ) + ) + or (stage == 3 and gadget.kind == "crossover") + or stage == 4 + ) + if not visible: continue x0 = origin_x + gadget.x_begin * cell y0 = origin_y + gadget.y_begin * cell x1 = origin_x + gadget.x_end * cell - 1 y1 = origin_y + gadget.y_end * cell - 1 - draw.rectangle((x0, y0, x1, y1), outline=_GADGET_COLORS[gadget.kind], width=3) + width = 7 if stage == 2 and crossovers and gadget is crossovers[0] else 4 + draw.rectangle( + (x0, y0, x1, y1), + outline=_GADGET_COLORS[gadget.kind], + width=width, + ) + if gadget.kind == "crossover" and stage in {2, 3}: + crossover_label = ( + f"X{gadget.ordinal}: swap rows " + f"{gadget.swap_row}/{gadget.swap_row + 1}" + if stage == 2 + else f"X{gadget.ordinal}:s{gadget.swap_row}" + ) + draw.text( + (x0 + 8, y0 + 5), + crossover_label, + font=explain_font(14 * EXPLAIN_RENDER_SCALE), + fill=_GADGET_COLORS["crossover"], + stroke_width=3, + stroke_fill=EXPLAIN_PANEL_RGB, + ) legend_x = origin_x + grid_width + 24 - draw.text((legend_x, 92), "Native sidecar spans", font=explain_font(14), fill=EXPLAIN_TEXT_RGB) - y = 126 - for kind, color in _GADGET_COLORS.items(): - draw.rectangle((legend_x, y, legend_x + 18, y + 18), fill=color) - count = sum(gadget.kind == kind for gadget in reduction.gadgets) + if stage == 5: draw.text( - (legend_x + 27, y + 2), - f"{kind.replace('_', ' ')}: {count}", - font=explain_font(10), - fill=EXPLAIN_TEXT_RGB if kind in visible_kinds else EXPLAIN_MUTED_RGB, + (legend_x, origin_y), + "Final Region vocabulary", + font=explain_font(20 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_TEXT_RGB, + ) + key_y = origin_y + 68 + draw.rectangle( + (legend_x, key_y, legend_x + 36, key_y + 36), + fill=EXPLAIN_ACTIVE_RGB, + outline=(174, 181, 193), + ) + draw.text( + (legend_x + 54, key_y - 3), + "active cell", + font=explain_font(22 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_TEXT_RGB, + ) + key_y += 64 + image.paste( + square_inactive_tile(36), + (legend_x, key_y), + ) + draw.text( + (legend_x + 54, key_y - 3), + "inactive / outside", + font=explain_font(22 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_TEXT_RGB, + ) + key_y += 64 + draw.line( + (legend_x, key_y + 18, legend_x + 36, key_y + 18), + fill=(174, 181, 193), + width=7, + ) + draw.text( + (legend_x + 54, key_y - 3), + "internal edge (no boundary)", + font=explain_font(22 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_TEXT_RGB, + ) + key_y += 64 + draw.line( + (legend_x, key_y + 18, legend_x + 36, key_y + 18), + fill=palette[0], + width=11, + ) + draw.text( + (legend_x + 54, key_y - 3), + "exposed boundary color", + font=explain_font(22 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (legend_x, key_y + 70), + f"{sum(bundle.region.active)} active / " + f"{bundle.region.active.count(False)} inactive\n" + "internal sides stay uncolored", + font=explain_font(16 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_MUTED_RGB, + spacing=10, + ) + else: + draw.text( + (legend_x, origin_y), + "Construction evidence", + font=explain_font(18 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_TEXT_RGB, + ) + y = origin_y + 52 + for kind, color in _GADGET_COLORS.items(): + draw.rectangle((legend_x, y, legend_x + 28, y + 28), fill=color) + count = sum(gadget.kind == kind for gadget in reduction.gadgets) + draw.text( + (legend_x + 42, y), + f"{kind.replace('_', ' ')}: {count}", + font=explain_font(14 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_TEXT_RGB, + ) + y += 42 + draw.text( + (legend_x, y + 8), + f"source signals: {len(reduction.source_signals)}\nadjacent swaps: " + + ", ".join(str(gadget.swap_row) for gadget in crossovers), + font=explain_font(14 * EXPLAIN_RENDER_SCALE), + fill=EXPLAIN_TEXT_RGB, + spacing=12, ) - y += 29 - draw.text( - (legend_x, y + 10), - f"signals: {len(reduction.source_signals)}\nswaps: " - f"{sum(g.kind == 'crossover' for g in reduction.gadgets)}", - font=explain_font(10), - fill=EXPLAIN_TEXT_RGB, - spacing=7, - ) draw.text( - (18, 368), - "The provenance describes construction; Region remains presentation-neutral.", - font=explain_font(9), + (36, 794), + "Spans and swaps are canonical construction provenance; boundary colors are constraints, not tile assignments.", + font=explain_font(13 * EXPLAIN_RENDER_SCALE), fill=EXPLAIN_MUTED_RGB, ) return image @@ -162,72 +495,501 @@ def render_builder_assets( frames, tuple(f"frame-{stage:02d}.png" for stage in range(6)), output_directory, - fallback_index=4, + fallback_index=5, duration_ms=duration_ms, ) -def _optimized_frame(stage: int) -> Image.Image: - image, draw = _base_frame( - "Optimized serial mechanisms", - f"didactic stage {stage + 1}/7 | storage/work changes only; search semantics stay shared", - (960, 500), +def _byte_support_example() -> dict[str, object]: + """Return one hand-sized aggregation derived from canonical tile edges.""" + source_tiles = (0, 10, 22) + source_east_edges = (2, 3, 3) + canonical_west_edges = ( + 1, 1, 1, 1, 2, 3, 2, 2, 3, 2, 3, 2, + 10, 3, 11, 2, 2, 3, 2, 2, 3, 3, 3, + ) + domain = sum(1 << tile for tile in source_tiles) + chunks = tuple((domain >> (8 * byte)) & 0xFF for byte in range(3)) + supported_edges = frozenset(source_east_edges) + supported_tiles = tuple( + tile + for tile, west in enumerate(canonical_west_edges) + if west in supported_edges ) + return { + "domain": domain, + "chunks": chunks, + "source_tiles": source_tiles, + "source_east_edges": source_east_edges, + "supported_tiles": supported_tiles, + } + + +def _queue_dedup_steps() -> tuple[tuple[str, str, tuple[int, ...]], ...]: + queue: list[int] = [] + pending: set[int] = set() + steps: list[tuple[str, str, tuple[int, ...]]] = [] + for label, operation in ( + ("enqueue c7", "enqueue"), + ("enqueue c7 again", "enqueue"), + ("dequeue c7", "dequeue"), + ("enqueue c7 later", "enqueue"), + ): + if operation == "dequeue": + queue.pop(0) + pending.remove(7) + action = "clear pending" + elif 7 in pending: + action = "suppress" + else: + queue.append(7) + pending.add(7) + action = "append" + steps.append((label, action, tuple(queue))) + return tuple(steps) + + +def _mrv_bucket_steps() -> tuple[ + tuple[ + str, + tuple[tuple[int, int], ...], + tuple[tuple[int, tuple[int, ...]], ...], + int, + ], + ..., +]: + domains = {2: 4, 5: 2, 9: 3} + + def snapshot(label: str) -> tuple[ + str, + tuple[tuple[int, int], ...], + tuple[tuple[int, tuple[int, ...]], ...], + int, + ]: + buckets: dict[int, list[int]] = {} + for cell, size in domains.items(): + if 2 <= size <= 23: + buckets.setdefault(size, []).append(cell) + packed = tuple( + (size, tuple(sorted(cells))) + for size, cells in sorted(buckets.items()) + ) + selected = packed[0][1][0] + return label, tuple(sorted(domains.items())), packed, selected + + steps = [snapshot("after lazy build")] + domains[2] = 2 + steps.append(snapshot("restrict c2: 4 -> 2")) + domains[2] = 4 + steps.append(snapshot("rollback c2: 2 -> 4")) + return tuple(steps) + + +def _optimized_canvas(mechanism: _Optimization, index: int) -> tuple[Image.Image, ImageDraw.ImageDraw]: + image = Image.new("RGB", (1920, 1040), EXPLAIN_PANEL_RGB) + draw = ImageDraw.Draw(image) + draw_explain_heading( + draw, + (48, 34), + title=mechanism.title, + subtitle=( + f"didactic mechanism {index + 1}/6 | {mechanism.identifier} | " + "same solver semantics" + ), + scale=EXPLAIN_RENDER_SCALE, + ) + return image, draw + + +def _draw_panel( + draw: ImageDraw.ImageDraw, + box: tuple[int, int, int, int], + title: str, + *, + fill: tuple[int, int, int] = (239, 242, 246), + outline: tuple[int, int, int] = (174, 181, 193), +) -> None: + draw.rounded_rectangle(box, radius=18, fill=fill, outline=outline, width=3) draw.text( - (18, 82), - "Reference baseline", - font=explain_font(14), + (box[0] + 28, box[1] + 22), + title, + font=explain_font(48), fill=EXPLAIN_TEXT_RGB, ) - draw.rounded_rectangle( - (18, 106, 245, 462), - radius=7, - fill=(239, 241, 245), - outline=(170, 177, 190), - ) - baseline = ( - "direct set-tile support loop", - "duplicate-accepting FIFO", - "initial trail entries", - "full DFS frame reserve", - "verified SAT result copy", - "linear MRV scan after the root", + + +def _draw_wrapped( + draw: ImageDraw.ImageDraw, + origin: tuple[int, int], + text: str, + *, + width: int, + size: int = 28, + fill: tuple[int, int, int] = EXPLAIN_TEXT_RGB, + spacing: int = 10, +) -> None: + lines = [ + wrapped + for paragraph in text.splitlines() + for wrapped in (textwrap.wrap(paragraph, width=width) or [""]) + ] + draw.multiline_text( + origin, + "\n".join(lines), + font=explain_font(size), + fill=fill, + spacing=spacing, ) - y = 130 - for line in baseline: - draw.text((34, y), line, font=explain_font(10), fill=EXPLAIN_MUTED_RGB) - y += 48 - - draw.text((276, 82), "Retained optimized path", font=explain_font(14), fill=EXPLAIN_TEXT_RGB) - for index, (name, description) in enumerate(_OPTIMIZATIONS): - y = 106 + index * 57 - active = index < stage - current = index == stage - 1 - draw.rounded_rectangle( - (276, y, 928, y + 45), - radius=6, - fill=(213, 237, 224) if active else (240, 242, 246), - outline=(52, 145, 94) if current else (181, 188, 199), - width=2 if current else 1, + + +def _draw_arrow( + draw: ImageDraw.ImageDraw, + start: tuple[int, int], + end: tuple[int, int], + *, + fill: tuple[int, int, int] = (55, 126, 168), +) -> None: + draw.line((*start, *end), fill=fill, width=7) + if abs(end[0] - start[0]) >= abs(end[1] - start[1]): + direction = 1 if end[0] >= start[0] else -1 + head = ( + end, + (end[0] - direction * 20, end[1] - 13), + (end[0] - direction * 20, end[1] + 13), ) - draw.text( - (290, y + 6), - name, - font=explain_font(11), - fill=EXPLAIN_TEXT_RGB if active else EXPLAIN_MUTED_RGB, + else: + direction = 1 if end[1] >= start[1] else -1 + head = ( + end, + (end[0] - 13, end[1] - direction * 20), + (end[0] + 13, end[1] - direction * 20), ) - draw.text( - (472, y + 8), - description, - font=explain_font(9), - fill=EXPLAIN_TEXT_RGB if active else EXPLAIN_MUTED_RGB, + draw.polygon(head, fill=fill) + + +def _draw_stack_frame( + draw: ImageDraw.ImageDraw, + x: int, + y: int, + *, + capacity: int, + used: int, + columns: int, +) -> None: + cell_width, cell_height, gap = 64, 44, 8 + for slot in range(capacity): + row, column = divmod(slot, columns) + left = x + column * (cell_width + gap) + top = y + row * (cell_height + gap) + draw.rounded_rectangle( + (left, top, left + cell_width, top + cell_height), + radius=5, + fill=(199, 231, 212) if slot < used else (255, 255, 255), + outline=(52, 145, 94) if slot < used else (181, 188, 199), + width=2, ) - draw.text( - (276, 468), - "Measured reports establish benefit separately; this animation claims no speedup.", - font=explain_font(9), + if slot < used: + centered_text( + draw, + (left, top, left + cell_width, top + cell_height), + str(slot), + font=explain_font(32), + ) + + +def _draw_dynamic_stack(draw: ImageDraw.ImageDraw) -> None: + _draw_panel(draw, (48, 154, 920, 910), "Reference: reserve active-cell limit") + _draw_panel(draw, (1000, 154, 1872, 910), "Optimized: grow within the same limit") + _draw_stack_frame(draw, 100, 270, capacity=40, used=11, columns=8) + _draw_wrapped( + draw, + (100, 565), + "capacity = active-cell limit (40 shown)\nused frames = 11", + width=43, + size=42, + ) + _draw_stack_frame(draw, 1050, 270, capacity=16, used=11, columns=8) + _draw_wrapped( + draw, + (1050, 430), + "start capacity = min(16, limit)\nused frames = 11", + width=43, + size=42, + ) + _draw_arrow(draw, (1240, 575), (1510, 575)) + draw.text((1080, 620), "when count reaches 16", font=explain_font(38), fill=EXPLAIN_MUTED_RGB) + draw.text((1515, 548), "16 -> 32 -> limit", font=explain_font(42), fill=EXPLAIN_TEXT_RGB) + _draw_wrapped( + draw, + (1050, 730), + "Only capacity changes. Both stacks hold the same DFS frames in the same order.", + width=38, + size=42, + ) + + +def _draw_initial_trail(draw: ImageDraw.ImageDraw) -> None: + _draw_panel(draw, (48, 154, 920, 910), "Reference: record initial undo entries") + _draw_panel(draw, (1000, 154, 1872, 910), "Optimized: omit unusable undo entries") + for x, label, color in ( + (100, "D[c3]\n23 -> 8", (210, 229, 244)), + (345, "trail\n(c3, 23)", (246, 216, 232)), + (590, "trace\nchange", (255, 232, 188)), + ): + draw.rounded_rectangle((x, 280, x + 190, 410), radius=12, fill=color, outline=(150, 158, 172), width=3) + centered_text(draw, (x, 280, x + 190, 410), label, font=explain_font(40)) + _draw_arrow(draw, (292, 345), (332, 345)) + _draw_arrow(draw, (537, 345), (577, 345)) + for x, label, color in ( + (1050, "D[c3]\n23 -> 8", (210, 229, 244)), + (1295, "no initial\ntrail entry", (239, 242, 246)), + (1540, "trace\nchange", (255, 232, 188)), + ): + draw.rounded_rectangle((x, 280, x + 190, 410), radius=12, fill=color, outline=(150, 158, 172), width=3) + centered_text(draw, (x, 280, x + 190, 410), label, font=explain_font(40)) + _draw_arrow(draw, (1242, 345), (1282, 345)) + _draw_arrow(draw, (1487, 345), (1527, 345)) + draw.line((100, 590, 820, 590), fill=(55, 126, 168), width=7) + draw.line((1050, 590, 1770, 590), fill=(55, 126, 168), width=7) + for x in (100, 1050): + draw.ellipse((x - 9, 581, x + 9, 599), fill=(55, 126, 168)) + draw.ellipse((x + 711, 581, x + 729, 599), fill=(55, 126, 168)) + draw.text((100, 620), "initial propagation", font=explain_font(38), fill=EXPLAIN_MUTED_RGB) + draw.text((570, 620), "clear initial trail", font=explain_font(38), fill=EXPLAIN_TEXT_RGB) + draw.text((1050, 620), "initial propagation", font=explain_font(38), fill=EXPLAIN_MUTED_RGB) + draw.text((1450, 620), "trail already empty", font=explain_font(38), fill=EXPLAIN_TEXT_RGB) + _draw_wrapped(draw, (100, 730), "Search starts with trail recording enabled.", width=31, size=44) + _draw_wrapped(draw, (1050, 730), "Search starts with trail recording enabled.", width=31, size=44) + + +def _draw_sat_ownership(draw: ImageDraw.ImageDraw) -> None: + _draw_panel(draw, (48, 154, 920, 910), "Reference: copy after verification") + _draw_panel(draw, (1000, 154, 1872, 910), "Optimized: transfer after verification") + for origin_x in (100, 1050): + draw.rounded_rectangle((origin_x, 260, origin_x + 300, 380), radius=12, fill=(210, 229, 244), outline=(75, 151, 202), width=3) + centered_text(draw, (origin_x, 260, origin_x + 300, 380), "state.domains", font=explain_font(42)) + _draw_arrow(draw, (origin_x + 310, 320), (origin_x + 445, 320)) + draw.rounded_rectangle((origin_x + 455, 260, origin_x + 700, 380), radius=12, fill=(199, 231, 212), outline=(52, 145, 94), width=3) + centered_text(draw, (origin_x + 455, 260, origin_x + 700, 380), "verify SAT", font=explain_font(42)) + draw.text((240, 415), "verified first", font=explain_font(38), fill=EXPLAIN_MUTED_RGB) + draw.text((1190, 415), "verified first", font=explain_font(38), fill=EXPLAIN_MUTED_RGB) + _draw_arrow(draw, (450, 510), (450, 630)) + draw.rounded_rectangle((205, 650, 695, 780), radius=12, fill=(246, 216, 232), outline=(203, 107, 151), width=3) + centered_text(draw, (205, 650, 695, 780), "copy to best_snapshot", font=explain_font(38)) + _draw_arrow(draw, (1400, 510), (1400, 630)) + draw.rounded_rectangle((1155, 650, 1645, 780), radius=12, fill=(246, 216, 232), outline=(203, 107, 151), width=3) + centered_text(draw, (1155, 650, 1645, 780), "transfer state.domains", font=explain_font(38)) + draw.text((1080, 795), "state.domains = NULL before destroy", font=explain_font(38), fill=EXPLAIN_TEXT_RGB) + draw.text((275, 815), "caller owns result", font=explain_font(38), fill=EXPLAIN_TEXT_RGB) + draw.text((1210, 850), "caller owns result", font=explain_font(38), fill=EXPLAIN_TEXT_RGB) + + +def _draw_byte_support(draw: ImageDraw.ImageDraw) -> None: + example = _byte_support_example() + domain = int(example["domain"]) + chunks = example["chunks"] + source_tiles = example["source_tiles"] + source_edges = example["source_east_edges"] + draw.text((48, 145), f"23-bit source domain 0b{domain:023b}", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + colors = ((210, 229, 244), (255, 232, 188), (246, 216, 232)) + for byte, (chunk, tile, edge, color) in enumerate(zip(chunks, source_tiles, source_edges, colors, strict=True)): + x = 48 + byte * 430 + draw.rounded_rectangle((x, 235, x + 360, 500), radius=16, fill=color, outline=(124, 133, 149), width=3) + draw.text((x + 24, 252), f"byte {byte}: 0x{chunk:02X}", font=explain_font(46), fill=EXPLAIN_TEXT_RGB) + draw.text((x + 24, 325), f"set bit -> tile {tile}", font=explain_font(44), fill=EXPLAIN_TEXT_RGB) + draw.text((x + 24, 390), f"east edge = {edge}", font=explain_font(44), fill=EXPLAIN_TEXT_RGB) + draw.text((x + 24, 450), "one table lookup", font=explain_font(42), fill=EXPLAIN_MUTED_RGB) + _draw_arrow(draw, (x + 360, 367), (x + 405, 367)) + draw.rounded_rectangle((1390, 235, 1872, 500), radius=16, fill=(199, 231, 212), outline=(52, 145, 94), width=3) + centered_text(draw, (1390, 250, 1872, 330), "OR three support masks", font=explain_font(44)) + _draw_wrapped( + draw, + (1420, 345), + "east {2,3} supports neighbors whose west edge is 2 or 3", + width=23, + size=40, + ) + supported = " ".join(str(tile) for tile in example["supported_tiles"]) + draw.rounded_rectangle((48, 610, 1872, 820), radius=16, fill=(239, 242, 246), outline=(174, 181, 193), width=3) + draw.text((80, 635), "supported neighbor tile IDs", font=explain_font(42), fill=EXPLAIN_MUTED_RGB) + draw.text((80, 705), supported, font=explain_font(44), fill=EXPLAIN_TEXT_RGB) + draw.text((48, 865), "Zero byte: skip lookup. Unused 24th bit: no tile.", font=explain_font(40), fill=EXPLAIN_MUTED_RGB) + + +def _draw_queue_dedup(draw: ImageDraw.ImageDraw) -> None: + steps = _queue_dedup_steps() + for index, (label, action, queue) in enumerate(steps): + x = 48 + index * 462 + draw.rounded_rectangle((x, 190, x + 414, 835), radius=18, fill=(239, 242, 246), outline=(174, 181, 193), width=3) + draw.text((x + 24, 220), f"{index + 1}. {label}", font=explain_font(36), fill=EXPLAIN_TEXT_RGB) + action_color = (52, 145, 94) if action == "append" else ((214, 91, 91) if action == "suppress" else (55, 126, 168)) + draw.rounded_rectangle((x + 24, 300, x + 390, 390), radius=12, fill=(255, 255, 255), outline=action_color, width=4) + centered_text(draw, (x + 24, 300, x + 390, 390), action, font=explain_font(46), fill=action_color) + draw.text((x + 24, 455), "FIFO", font=explain_font(38), fill=EXPLAIN_MUTED_RGB) + draw.rounded_rectangle((x + 24, 505, x + 390, 615), radius=10, fill=(255, 255, 255), outline=(181, 188, 199), width=3) + if queue: + draw.rounded_rectangle((x + 45, 525, x + 145, 595), radius=8, fill=(210, 229, 244), outline=(75, 151, 202), width=3) + centered_text(draw, (x + 45, 525, x + 145, 595), "c7", font=explain_font(42)) + else: + centered_text(draw, (x + 24, 505, x + 390, 615), "empty", font=explain_font(42), fill=EXPLAIN_MUTED_RGB) + pending = bool(queue) + draw.text((x + 24, 680), "pending bit c7", font=explain_font(36), fill=EXPLAIN_MUTED_RGB) + draw.ellipse((x + 285, 675, x + 345, 735), fill=(52, 145, 94) if pending else (255, 255, 255), outline=(52, 145, 94), width=4) + centered_text(draw, (x + 285, 675, x + 345, 735), "1" if pending else "0", font=explain_font(40), fill=(255, 255, 255) if pending else EXPLAIN_TEXT_RGB) + draw.text((48, 875), "Suppress only while an unconsumed c7 is pending.", font=explain_font(40), fill=EXPLAIN_MUTED_RGB) + + +def _draw_mrv_state( + draw: ImageDraw.ImageDraw, + x: int, + state: tuple[str, tuple[tuple[int, int], ...], tuple[tuple[int, tuple[int, ...]], ...], int], +) -> None: + label, domains, buckets, selected = state + draw.rounded_rectangle((x, 300, x + 570, 820), radius=18, fill=(239, 242, 246), outline=(174, 181, 193), width=3) + draw.text((x + 24, 320), label, font=explain_font(40), fill=EXPLAIN_TEXT_RGB) + draw.text((x + 24, 390), "domains", font=explain_font(38), fill=EXPLAIN_MUTED_RGB) + draw.text((x + 380, 390), f"select c{selected}", font=explain_font(38), fill=(111, 82, 176)) + for index, (cell, size) in enumerate(domains): + left = x + 24 + index * 170 + fill = (231, 222, 249) if cell == selected else (255, 255, 255) + draw.rounded_rectangle((left, 445, left + 145, 520), radius=9, fill=fill, outline=(111, 82, 176) if cell == selected else (181, 188, 199), width=3) + centered_text(draw, (left, 445, left + 145, 520), f"c{cell}: {size}", font=explain_font(52)) + draw.text((x + 24, 555), "buckets: size -> cells", font=explain_font(38), fill=EXPLAIN_MUTED_RGB) + y = 615 + for size, cells in buckets: + draw.text((x + 70, y), str(size), font=explain_font(52), fill=EXPLAIN_TEXT_RGB) + draw.rounded_rectangle((x + 170, y - 7, x + 520, y + 43), radius=7, fill=(255, 255, 255), outline=(181, 188, 199), width=2) + draw.text((x + 190, y), " ".join(f"c{cell}" for cell in cells), font=explain_font(50), fill=EXPLAIN_TEXT_RGB) + y += 58 + + +def _draw_lazy_mrv(draw: ImageDraw.ImageDraw) -> None: + draw.rounded_rectangle((48, 145, 1872, 255), radius=14, fill=(255, 232, 188), outline=(217, 119, 6), width=3) + draw.text((78, 166), "Root: row-major scan. Build the private index only after a surviving nonterminal branch.", font=explain_font(42), fill=EXPLAIN_TEXT_RGB) + for x, state in zip((48, 675, 1302), _mrv_bucket_steps(), strict=True): + _draw_mrv_state(draw, x, state) + draw.text((48, 850), "domains = semantic source of truth", font=explain_font(44), fill=EXPLAIN_TEXT_RGB) + draw.text((1010, 850), "MRV index = private derived state", font=explain_font(44), fill=EXPLAIN_TEXT_RGB) + _draw_wrapped( + draw, + (48, 900), + "Buckets 2-23; exclude 0, 1, inactive.\nPick lowest size, then lowest row-major cell.", + width=72, + size=52, fill=EXPLAIN_MUTED_RGB, + spacing=3, + ) + + +def _optimized_frame(stage: int) -> Image.Image: + if not 0 <= stage < len(_OPTIMIZATIONS): + raise WangSquareRenderError("optimized mechanism stage lies outside panels") + mechanism = _OPTIMIZATIONS[stage] + image, draw = _optimized_canvas(mechanism, stage) + painters = ( + _draw_dynamic_stack, + _draw_initial_trail, + _draw_sat_ownership, + _draw_byte_support, + _draw_queue_dedup, + _draw_lazy_mrv, + ) + painters[stage](draw) + return image + + +def _draw_summary_card( + draw: ImageDraw.ImageDraw, + box: tuple[int, int, int, int], + mechanism: _Optimization, + index: int, +) -> None: + left, top, right, bottom = box + draw.rounded_rectangle( + box, + radius=16, + fill=(239, 242, 246), + outline=(174, 181, 193), + width=3, + ) + draw.text( + (left + 24, top + 17), + mechanism.title, + font=explain_font(50), + fill=EXPLAIN_TEXT_RGB, + ) + center_y = top + 143 + if index == 0: + for slot in range(8): + x = left + 30 + slot * 54 + draw.rounded_rectangle( + (x, center_y - 28, x + 44, center_y + 28), + radius=5, + fill=(199, 231, 212) if slot < 5 else (255, 255, 255), + outline=(52, 145, 94) if slot < 5 else (181, 188, 199), + width=2, + ) + _draw_arrow(draw, (left + 482, center_y), (left + 590, center_y)) + draw.text((left + 610, center_y - 28), "grow -> limit", font=explain_font(42), fill=EXPLAIN_TEXT_RGB) + elif index == 1: + draw.rounded_rectangle((left + 30, center_y - 40, left + 235, center_y + 40), radius=8, fill=(210, 229, 244), outline=(75, 151, 202), width=3) + centered_text(draw, (left + 30, center_y - 40, left + 250, center_y + 40), "domain delta", font=explain_font(38)) + _draw_arrow(draw, (left + 265, center_y), (left + 365, center_y)) + draw.rounded_rectangle((left + 380, center_y - 40, left + 555, center_y + 40), radius=8, fill=(255, 232, 188), outline=(217, 119, 6), width=3) + centered_text(draw, (left + 380, center_y - 40, left + 555, center_y + 40), "trace kept", font=explain_font(36)) + draw.rounded_rectangle((left + 610, center_y - 40, left + 835, center_y + 40), radius=8, fill=(255, 255, 255), outline=(214, 91, 91), width=3) + centered_text(draw, (left + 620, center_y - 40, left + 790, center_y + 40), "initial\nundo entry", font=explain_font(36), fill=EXPLAIN_TEXT_RGB) + draw.line((left + 800, center_y - 20, left + 825, center_y + 20), fill=(214, 91, 91), width=5) + draw.line((left + 825, center_y - 20, left + 800, center_y + 20), fill=(214, 91, 91), width=5) + elif index == 2: + draw.rounded_rectangle((left + 30, center_y - 40, left + 245, center_y + 40), radius=8, fill=(199, 231, 212), outline=(52, 145, 94), width=3) + centered_text(draw, (left + 30, center_y - 40, left + 245, center_y + 40), "verify SAT", font=explain_font(40)) + _draw_arrow(draw, (left + 260, center_y), (left + 390, center_y)) + draw.rounded_rectangle((left + 405, center_y - 40, left + 680, center_y + 40), radius=8, fill=(246, 216, 232), outline=(203, 107, 151), width=3) + centered_text(draw, (left + 405, center_y - 40, left + 680, center_y + 40), "transfer buffer", font=explain_font(38)) + draw.text((left + 700, center_y - 25), "caller owns", font=explain_font(38), fill=EXPLAIN_TEXT_RGB) + elif index == 3: + for byte, label in enumerate(("01", "04", "40")): + x = left + 30 + byte * 120 + draw.rounded_rectangle((x, center_y - 40, x + 90, center_y + 40), radius=8, fill=((210, 229, 244), (255, 232, 188), (246, 216, 232))[byte], outline=(124, 133, 149), width=3) + centered_text(draw, (x, center_y - 40, x + 90, center_y + 40), label, font=explain_font(42)) + _draw_arrow(draw, (left + 390, center_y), (left + 520, center_y)) + draw.rounded_rectangle((left + 535, center_y - 40, left + 835, center_y + 40), radius=8, fill=(199, 231, 212), outline=(52, 145, 94), width=3) + centered_text(draw, (left + 535, center_y - 40, left + 835, center_y + 40), "OR 3 masks", font=explain_font(42)) + elif index == 4: + labels = (("+ c7", "1"), ("dup x", "1"), ("pop", "0"), ("later +", "1")) + for step, (event, pending) in enumerate(labels): + x = left + 30 + step * 205 + draw.text((x, center_y - 35), event, font=explain_font(38), fill=EXPLAIN_TEXT_RGB) + draw.ellipse((x + 118, center_y - 38, x + 190, center_y + 34), fill=(52, 145, 94) if pending == "1" else (255, 255, 255), outline=(52, 145, 94), width=3) + centered_text(draw, (x + 118, center_y - 38, x + 190, center_y + 34), pending, font=explain_font(40), fill=(255, 255, 255) if pending == "1" else EXPLAIN_TEXT_RGB) + else: + labels = (("bucket 4", "c2"), ("bucket 2", "c2 c5"), ("bucket 4", "c2")) + for step, (bucket, cells) in enumerate(labels): + x = left + 30 + step * 275 + draw.rounded_rectangle((x, center_y - 45, x + 225, center_y + 45), radius=8, fill=(231, 222, 249), outline=(111, 82, 176), width=3) + centered_text(draw, (x, center_y - 45, x + 225, center_y - 3), bucket, font=explain_font(36)) + centered_text(draw, (x, center_y + 1, x + 225, center_y + 45), cells, font=explain_font(38), fill=(111, 82, 176)) + if step < 2: + _draw_arrow(draw, (x + 232, center_y), (x + 267, center_y)) + + +def _optimized_summary() -> Image.Image: + image = Image.new("RGB", (1920, 1040), EXPLAIN_PANEL_RGB) + draw = ImageDraw.Draw(image) + draw_explain_heading( + draw, + (48, 34), + title="Optimized serial mechanisms", + subtitle="didactic summary | six private storage/work changes; shared search semantics", + scale=EXPLAIN_RENDER_SCALE, ) + for index, mechanism in enumerate(_OPTIMIZATIONS): + column, row = index % 2, index // 2 + x = 48 + column * 936 + y = 145 + row * 267 + _draw_summary_card(draw, (x, y, x + 888, y + 235), mechanism, index) + draw.text((48, 950), "Six concrete state changes; full frames retain details.", font=explain_font(34), fill=EXPLAIN_MUTED_RGB) return image @@ -236,7 +998,8 @@ def render_optimized_assets( *, duration_ms: int = 750, ) -> AnimationOutputs: - frames = tuple(_optimized_frame(stage) for stage in range(7)) + mechanism_frames = tuple(_optimized_frame(stage) for stage in range(6)) + frames = (*mechanism_frames, _optimized_summary()) return write_animation_assets( frames, tuple(f"frame-{stage:02d}.png" for stage in range(7)), diff --git a/renderer/wang_explain.py b/renderer/wang_explain.py index 0d9d2bf..b6a22c2 100644 --- a/renderer/wang_explain.py +++ b/renderer/wang_explain.py @@ -17,6 +17,17 @@ EXPLAIN_INACTIVE_LIGHT_RGB: Final = (226, 230, 236) EXPLAIN_INACTIVE_DARK_RGB: Final = (190, 197, 207) EXPLAIN_ACTIVE_RGB: Final = (238, 241, 246) +EXPLAIN_RENDER_SCALE: Final = 2 +EXPLAIN_UNRESOLVED_RGB: Final = (128, 164, 201) +EXPLAIN_SINGLETON_RGB: Final = (83, 166, 116) +EXPLAIN_SELECTED_MRV_RGB: Final = (111, 82, 176) +EXPLAIN_PROPAGATION_SOURCE_RGB: Final = (238, 177, 69) +EXPLAIN_PROPAGATION_TARGET_RGB: Final = (75, 151, 202) +EXPLAIN_QUEUED_RGB: Final = (108, 117, 132) +EXPLAIN_DECISION_RGB: Final = (245, 178, 60) +EXPLAIN_CONFLICT_RGB: Final = (218, 82, 82) +EXPLAIN_TRAIL_MUTATION_RGB: Final = (203, 107, 151) +EXPLAIN_RESTORED_RGB: Final = (89, 166, 169) def explain_font(size: int) -> ImageFont.FreeTypeFont | ImageFont.ImageFont: @@ -55,14 +66,20 @@ def draw_explain_heading( *, title: str, subtitle: str, + scale: int = 1, ) -> None: """Draw the common two-line heading used by explainability views.""" x, y = origin - draw.text((x, y), title, font=explain_font(20), fill=EXPLAIN_TEXT_RGB) draw.text( - (x, y + 28), + (x, y), + title, + font=explain_font(20 * scale), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (x, y + 28 * scale), subtitle, - font=explain_font(12), + font=explain_font(12 * scale), fill=EXPLAIN_MUTED_RGB, ) diff --git a/renderer/wang_generalized_render.py b/renderer/wang_generalized_render.py index b384f74..79d032d 100644 --- a/renderer/wang_generalized_render.py +++ b/renderer/wang_generalized_render.py @@ -296,6 +296,7 @@ def compose_atomic_semantic_legend( *, pixels_per_cell: int = DEFAULT_PIXELS_PER_CELL, margin: int = DEFAULT_MARGIN, + scale: int = 1, ) -> np.ndarray: """Compose all 23 atomic IDs with generalized part and symbolic edges.""" try: @@ -303,14 +304,20 @@ def compose_atomic_semantic_legend( except GeneralizedTileError as error: raise _as_render_error(error) from error ppc, checked_margin = _checked_dimensions(pixels_per_cell, margin) - cell_size = max(58, ppc * 2) - columns = 3 + checked_scale = _render_integer(scale, "scale", minimum=1, maximum=2) + checked_margin *= checked_scale + cell_size = max(58, ppc * 2) * checked_scale + columns = 2 if checked_scale == 2 else 3 rows = (len(tile_edges) + columns - 1) // columns - card_width = 420 - card_height = cell_size + 24 - gap = 10 + card_width = 420 * checked_scale + card_height = max( + cell_size + 24 * checked_scale, + 142 * checked_scale if checked_scale == 2 else 0, + ) + gap = 10 * checked_scale width = 2 * checked_margin + columns * card_width + (columns - 1) * gap - height = 2 * checked_margin + _HEADER_HEIGHT + rows * card_height + header_height = _HEADER_HEIGHT * checked_scale + height = 2 * checked_margin + header_height + rows * card_height _check_canvas_limits(width, height) canvas = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB) @@ -323,17 +330,23 @@ def compose_atomic_semantic_legend( "generalized role and symbolic color are primary; numeric IDs in " "brackets preserve the transport vocabulary" ), + scale=checked_scale, ) palette = _build_palette_from_edges(tile_edges) - grid_y = checked_margin + _HEADER_HEIGHT + grid_y = checked_margin + header_height for tile_id, edges in enumerate(tile_edges): column = tile_id % columns row = tile_id // columns x = checked_margin + column * (card_width + gap) y = grid_y + row * card_height draw.rounded_rectangle( - (x, y, x + card_width - 1, y + card_height - 8), - radius=7, + ( + x, + y, + x + card_width - 1, + y + card_height - 8 * checked_scale, + ), + radius=7 * checked_scale, fill=(249, 250, 252), outline=(214, 219, 227), ) @@ -344,24 +357,32 @@ def compose_atomic_semantic_legend( tile_id=tile_id, edge_labels=False, ) - canvas.paste(asset, (x + 8, y + 8)) - text_x = x + cell_size + 20 + canvas.paste( + asset, + (x + 8 * checked_scale, y + 8 * checked_scale), + ) + text_x = x + cell_size + 20 * checked_scale + title_size = 22 if checked_scale == 2 else 14 + edge_size = 24 if checked_scale == 2 else 11 + title_y = 6 if checked_scale == 2 else 9 + north_east_y = 48 if checked_scale == 2 else 33 + south_west_y = 86 if checked_scale == 2 else 53 draw.text( - (text_x, y + 9), + (text_x, y + title_y * checked_scale), f"{atomic_semantic_label(tile_id)} - atomic #{tile_id}", - font=explain_font(14), + font=explain_font(title_size * checked_scale), fill=EXPLAIN_TEXT_RGB, ) draw.text( - (text_x, y + 33), + (text_x, y + north_east_y * checked_scale), f"N {color_label(edges[0])} E {color_label(edges[1])}", - font=explain_font(11), + font=explain_font(edge_size * checked_scale), fill=EXPLAIN_TEXT_RGB, ) draw.text( - (text_x, y + 53), + (text_x, y + south_west_y * checked_scale), f"S {color_label(edges[2])} W {color_label(edges[3])}", - font=explain_font(11), + font=explain_font(edge_size * checked_scale), fill=EXPLAIN_TEXT_RGB, ) return np.asarray(canvas, dtype=np.uint8) diff --git a/renderer/wang_narrative.py b/renderer/wang_narrative.py index ae5d3a2..b4160a1 100644 --- a/renderer/wang_narrative.py +++ b/renderer/wang_narrative.py @@ -7,6 +7,7 @@ import hashlib import json from pathlib import Path +from typing import NamedTuple import numpy as np from PIL import Image, ImageDraw @@ -19,6 +20,8 @@ EXPLAIN_TEXT_RGB, draw_explain_heading, explain_font, + square_inactive_tile, + square_explain_tile, ) from wang_generalized_render import ( compose_atomic_semantic_legend, @@ -27,8 +30,9 @@ ) from wang_generalized import generalized_specification_sha256 from wang_hex_port import WangSquareRenderError, check_square_to_hex, reduce_square_to_hex -from wang_snapshot import load_explainability_bundle +from wang_snapshot import ExplainabilityBundle, load_explainability_bundle from wang_square import ( + _build_palette_from_edges, _compose_wang_hex_explain, _compose_wang_square_explain, _save_png_atomic, @@ -89,6 +93,23 @@ class OverviewOutputs: worked_example: Path | None +class _TilingEvidence(NamedTuple): + active_index: int + inactive_index: int + tile_id: int + right_id: int + tile_edges: tuple[int, int, int, int] + right_edges: tuple[int, int, int, int] + required_n: int + maximum_tile_id: int + + +class _ExtractionEvidence(NamedTuple): + variable: int + tile_ids: tuple[int, int, int] + value: bool + + def _save_image(image: Image.Image, path: Path) -> None: if image.mode != "RGB": raise WangSquareRenderError("narrative output must be RGB") @@ -108,11 +129,211 @@ def _load_image(path: Path) -> Image.Image: def _fit(image: Image.Image, size: tuple[int, int]) -> Image.Image: fitted = image.copy() - fitted.thumbnail(size, resample=Image.Resampling.NEAREST) + fitted.thumbnail(size, resample=Image.Resampling.LANCZOS) return fitted -def _load_verification(path: str | Path) -> tuple[str, tuple[dict[str, object], ...]]: +def _encoded(document: dict[str, object]) -> bytes: + return ( + json.dumps(document, ensure_ascii=False, allow_nan=False, indent=2) + "\n" + ).encode("utf-8") + + +def _manifest_context( + path: str | Path, +) -> tuple[ExplainabilityBundle, dict[str, str | None]]: + source = Path(path) + bundle = load_explainability_bundle(source) + try: + document = json.loads(source.read_text(encoding="utf-8")) + except (OSError, UnicodeError, json.JSONDecodeError) as error: + raise WangSquareRenderError( + f"cannot load explainability identity manifest {source!s}: {error}" + ) from error + artifacts = document.get("artifacts") if type(document) is dict else None + if type(artifacts) is not dict or not { + "formula", "tileset", "region", "reduction", "solution" + } <= set(artifacts): + raise WangSquareRenderError( + "verification requires an explainability manifest with reduction and solution identities" + ) + identities: dict[str, str | None] = { + "source_formula": bundle.source_formula_sha256, + } + for target, artifact_name in ( + ("formula_snapshot", "formula"), + ("tileset", "tileset"), + ("region", "region"), + ("provenance", "reduction"), + ("reference_solution", "solution"), + ): + reference = artifacts[artifact_name] + if reference is None: + identities[target] = None + continue + if type(reference) is not dict or set(reference) != {"path", "sha256", "schema"}: + raise WangSquareRenderError( + f"verification manifest {artifact_name} reference must be closed" + ) + digest = reference["sha256"] + if ( + type(digest) is not str + or len(digest) != 64 + or any(character not in "0123456789abcdef" for character in digest) + ): + raise WangSquareRenderError( + f"verification manifest {artifact_name} identity is invalid" + ) + identities[target] = digest + return bundle, identities + + +def _bind_solution( + bundle: ExplainabilityBundle, + identities: dict[str, str | None], + path: str | Path, +): + source = Path(path) + try: + digest = hashlib.sha256(source.read_bytes()).hexdigest() + except OSError as error: + raise WangSquareRenderError(f"cannot read verification solution: {error}") from error + if digest != identities["reference_solution"]: + raise WangSquareRenderError( + "verification solution identity disagrees with explainability manifest" + ) + presentation = load_wang_presentation(source) + region = bundle.region + if ( + (presentation.min_x, presentation.min_y, presentation.max_x, presentation.max_y) + != (region.min_x, region.min_y, region.max_x, region.max_y) + or presentation.tile_edges != bundle.tileset.tile_edges + or any( + (tile_id is None) == active + for tile_id, active in zip( + presentation.cells, region.active, strict=True + ) + ) + ): + raise WangSquareRenderError( + "verification solution structure disagrees with explainability bundle" + ) + return presentation + + +def _tiling_evidence( + bundle: ExplainabilityBundle, presentation +) -> _TilingEvidence: + region = bundle.region + active_index = next( + index + for index, active in enumerate(region.active) + if active + and index % region.width + 1 < region.width + and region.active[index + 1] + and region.boundary[index] is not None + and region.boundary[index][0] is not None + ) + inactive_index = next( + index for index, active in enumerate(region.active) if not active + ) + right_index = active_index + 1 + tile_id = presentation.cells[active_index] + right_id = presentation.cells[right_index] + if tile_id is None or right_id is None: + raise WangSquareRenderError("verification evidence selected an inactive tile") + tile = presentation.tile_edges[tile_id] + right = presentation.tile_edges[right_id] + required = region.boundary[active_index][0] + if tile[1] != right[3] or tile[0] != required: + raise WangSquareRenderError( + "verification evidence does not match the recorded checker result" + ) + return _TilingEvidence( + active_index=active_index, + inactive_index=inactive_index, + tile_id=tile_id, + right_id=right_id, + tile_edges=tile, + right_edges=right, + required_n=required, + maximum_tile_id=len(presentation.tile_edges) - 1, + ) + + +def _extraction_evidence( + bundle: ExplainabilityBundle, + presentation, + extracted_assignment: tuple[bool, ...], +) -> tuple[_ExtractionEvidence, ...]: + reduction = bundle.reduction + if reduction is None or len(extracted_assignment) != bundle.formula.variable_count: + raise WangSquareRenderError( + "verification extraction inputs do not match the formula" + ) + gadgets = tuple( + sorted( + (gadget for gadget in reduction.gadgets if gadget.kind == "variable"), + key=lambda gadget: gadget.ordinal, + ) + ) + if len(gadgets) != len(extracted_assignment): + raise WangSquareRenderError( + "verification extraction requires one recorded variable gadget per value" + ) + evidence: list[_ExtractionEvidence] = [] + for variable, (gadget, value) in enumerate( + zip(gadgets, extracted_assignment, strict=True) + ): + rows = tuple(range(gadget.y_begin, min(gadget.y_begin + 3, gadget.y_end))) + if len(rows) != 3: + raise WangSquareRenderError( + "verification extraction gadget does not expose three source cells" + ) + tile_ids: list[int] = [] + for y in rows: + index = (y - presentation.min_y) * presentation.width + ( + gadget.x_begin - presentation.min_x + ) + tile_id = presentation.cells[index] + if tile_id is None: + raise WangSquareRenderError( + "verification extraction selected an inactive source cell" + ) + tile_ids.append(tile_id) + evidence.append( + _ExtractionEvidence( + variable=variable, + tile_ids=(tile_ids[0], tile_ids[1], tile_ids[2]), + value=value, + ) + ) + return tuple(evidence) + + +def _assignment_sha256(values: tuple[bool, ...]) -> str: + return hashlib.sha256(_encoded({"witness": list(values)})).hexdigest() + + +def _bounded_variable_indices(variable_count: int) -> tuple[int, ...]: + if variable_count <= 3: + return tuple(range(variable_count)) + return (0, 1, variable_count - 1) + + +def _load_verification( + path: str | Path, + *, + manifest_path: str | Path | None = None, + solution_path: str | Path | None = None, + extracted_assignment: tuple[bool, ...] | None = None, +) -> tuple[ + str, + tuple[dict[str, object], ...], + ExplainabilityBundle | None, + object | None, + tuple[bool, ...] | None, +]: source = Path(path) try: document = json.loads(source.read_text(encoding="utf-8")) @@ -197,44 +418,82 @@ def _load_verification(path: str | Path) -> tuple[str, tuple[dict[str, object], if not valid: raise WangSquareRenderError(f"verification record {name} is inconsistent") records.append(record) - encoded_source = ( - json.dumps( - {"verification": verification, "agreement": agreement}, - ensure_ascii=False, - allow_nan=False, - indent=2, + bundle: ExplainabilityBundle | None = None + presentation = None + source_payload: dict[str, object] = { + "verification": verification, + "agreement": agreement, + } + if manifest_path is not None: + bundle, identities = _manifest_context(manifest_path) + if status == "sat": + if solution_path is None or extracted_assignment is None: + raise WangSquareRenderError( + "SAT verification explanation requires solution and copied assignment" + ) + presentation = _bind_solution(bundle, identities, solution_path) + assignment_record = verification["reference_assignment"] + if _assignment_sha256(extracted_assignment) != assignment_record[ + "witness_sha256" + ]: + raise WangSquareRenderError( + "verification assignment identity disagrees with checker receipt" + ) + elif solution_path is not None or extracted_assignment is not None: + raise WangSquareRenderError( + "UNSAT verification must not receive solution or assignment data" + ) + if (status == "sat") != (identities["reference_solution"] is not None): + raise WangSquareRenderError( + "verification solution applicability disagrees with explainability manifest" + ) + source_payload.update(identities) + source_payload["reference_assignment"] = ( + None + if extracted_assignment is None + else list(extracted_assignment) ) - + "\n" - ).encode("utf-8") + elif status == "sat": + raise WangSquareRenderError( + "SAT verification explanation requires explainability context" + ) + encoded_source = _encoded(source_payload) source_sha256 = document["source_sha256"] if ( type(source_sha256) is not str or hashlib.sha256(encoded_source).hexdigest() != source_sha256 ): raise WangSquareRenderError("verification receipt source hash drifted") - return status, tuple(records) + return status, tuple(records), bundle, presentation, extracted_assignment def _verification_frame( status: str, records: tuple[dict[str, object], ...], stage: int, + bundle: ExplainabilityBundle | None, + presentation, + extracted_assignment: tuple[bool, ...] | None, ) -> Image.Image: - image = Image.new("RGB", (960, 500), EXPLAIN_PANEL_RGB) + image = Image.new("RGB", (1920, 1040), EXPLAIN_PANEL_RGB) draw = ImageDraw.Draw(image) - draw_explain_heading( - draw, - (18, 16), - title="Independent verification sequence", - subtitle=( - f"observed record {stage + 1}/6 | expected {status.upper()} | " - "renders checker receipts; does not rerun a verifier" - ), + draw.text( + (30, 16), + "Independent verification receipts", + font=explain_font(52), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (30, 78), + f"Receipt {stage + 1}/6 | {status.upper()} | display only; no verifier rerun", + font=explain_font(34), + fill=EXPLAIN_MUTED_RGB, ) for index, ((_, label, expected_prefix), record) in enumerate( zip(_CHECKS, records, strict=True) ): - y = 92 + index * 60 + x = 30 + (index % 3) * 630 + y = 118 + (index // 3) * 130 visible = index <= stage performed = record.get("performed") is True passed = record.get("passed") is True @@ -250,36 +509,69 @@ def _verification_frame( f"verification record {_CHECKS[index][0]} is inconsistent" ) draw.rounded_rectangle( - (18, y, 930, y + 46), - radius=6, + (x, y, x + 600, y + 110), + radius=12, fill=fill if visible else (242, 244, 247), outline=(53, 144, 93) if index == stage else (181, 188, 199), - width=2 if index == stage else 1, + width=4 if index == stage else 2, ) draw.text( - (32, y + 7), + (x + 16, y + 16), label, - font=explain_font(12), + font=explain_font(40), fill=EXPLAIN_TEXT_RGB if visible else EXPLAIN_MUTED_RGB, ) draw.text( - (278, y + 8), + (x + 16, y + 66), state, - font=explain_font(11), + font=explain_font(32), fill=EXPLAIN_TEXT_RGB if visible else EXPLAIN_MUTED_RGB, ) - draw.text( - (548, y + 9), - checker, - font=explain_font(9), - fill=EXPLAIN_MUTED_RGB, - ) - draw.text( - (18, 472), - "SAT checks validate named witnesses independently; UNSAT has no fabricated certificate.", - font=explain_font(9), - fill=EXPLAIN_MUTED_RGB, + if status == "unsat": + draw.rounded_rectangle((170, 390, 1750, 850), radius=24, fill=(239, 242, 246), outline=(181, 188, 199), width=3) + draw.text((490, 470), "No SAT witness was returned", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + draw.text((360, 565), "Six witness checks are not applicable; no certificate is fabricated.", font=explain_font(34), fill=EXPLAIN_MUTED_RGB) + draw.text((460, 650), "Observed search traces remain diagnostics only.", font=explain_font(34), fill=EXPLAIN_MUTED_RGB) + return image + + if bundle is None or presentation is None or extracted_assignment is None: + raise WangSquareRenderError("SAT verification frame lacks validated context") + palette = _build_palette_from_edges(presentation.tile_edges) + tiling = _tiling_evidence(bundle, presentation) + draw.rounded_rectangle((30, 390, 930, 982), radius=18, fill=EXPLAIN_ACTIVE_RGB, outline=(181, 188, 199), width=2) + draw.text((62, 416), "Tiling checker coverage", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + + tile_id = tiling.tile_id + right_id = tiling.right_id + tile_size = 180 + image.paste(square_explain_tile(tiling.tile_edges, palette, tile_size, tile_id=tile_id, edge_labels=True), (92, 500)) + image.paste(square_explain_tile(tiling.right_edges, palette, tile_size, tile_id=right_id, edge_labels=True), (318, 500)) + draw.text((92, 696), f"internal: #{tile_id} E{tiling.tile_edges[1]} = #{right_id} W{tiling.right_edges[3]}", font=explain_font(42), fill=EXPLAIN_TEXT_RGB) + draw.text((92, 756), f"boundary: #{tile_id} N{tiling.tile_edges[0]} = required N{tiling.required_n}", font=explain_font(42), fill=EXPLAIN_TEXT_RGB) + image.paste(square_inactive_tile(118), (100, 822)) + draw.text((248, 838), "TILE_NONE", font=explain_font(46), fill=EXPLAIN_TEXT_RGB) + draw.text((248, 894), f"inactive[{tiling.inactive_index}] = null = native 255", font=explain_font(40), fill=EXPLAIN_TEXT_RGB) + draw.text((560, 538), f"active[{tiling.active_index}] = tile #{tile_id}", font=explain_font(42), fill=EXPLAIN_TEXT_RGB) + draw.text((560, 606), f"valid IDs: 0..{tiling.maximum_tile_id}", font=explain_font(42), fill=EXPLAIN_TEXT_RGB) + + draw.rounded_rectangle((960, 390, 1890, 982), radius=18, fill=EXPLAIN_ACTIVE_RGB, outline=(181, 188, 199), width=2) + draw.text((992, 416), "Source cells -> recorded value", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + extraction = _extraction_evidence(bundle, presentation, extracted_assignment) + selected_indices = _bounded_variable_indices(len(extraction)) + selected_extraction = tuple( + extraction[variable] + for variable in selected_indices ) + if len(extraction) > len(selected_indices): + draw.text((1530, 432), f"{len(extraction) - 3} omitted", font=explain_font(32), fill=EXPLAIN_MUTED_RGB) + for row, item in enumerate(selected_extraction): + y = 500 + row * 145 + draw.text((994, y + 34), f"x{item.variable}", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + for offset, source_tile in enumerate(item.tile_ids): + image.paste(square_explain_tile(presentation.tile_edges[source_tile], palette, 112, tile_id=source_tile, edge_labels=False), (1080 + offset * 124, y)) + draw.text((1470, y + 6), f"recorded {'true' if item.value else 'false'}", font=explain_font(46), fill=(30, 112, 70)) + draw.text((1470, y + 68), "checker passed", font=explain_font(36), fill=EXPLAIN_MUTED_RGB) + draw.text((994, 946), "Displayed cells only; decoding happened upstream.", font=explain_font(32), fill=EXPLAIN_MUTED_RGB) return image @@ -287,11 +579,27 @@ def render_verification_assets( run_path: str | Path, output_directory: str | Path, *, + manifest_path: str | Path | None = None, + solution_path: str | Path | None = None, + extracted_assignment: tuple[bool, ...] | None = None, duration_ms: int = 750, ) -> AnimationOutputs: - status, records = _load_verification(run_path) + status, records, bundle, presentation, extracted_assignment = _load_verification( + run_path, + manifest_path=manifest_path, + solution_path=solution_path, + extracted_assignment=extracted_assignment, + ) frames = tuple( - _verification_frame(status, records, stage) for stage in range(len(_CHECKS)) + _verification_frame( + status, + records, + stage, + bundle, + presentation, + extracted_assignment, + ) + for stage in range(len(_CHECKS)) ) return write_animation_assets( frames, @@ -308,7 +616,7 @@ def _presentation_frame( hex_image: Image.Image, stage: int, ) -> Image.Image: - image = Image.new("RGB", (1080, 620), EXPLAIN_PANEL_RGB) + image = Image.new("RGB", (1920, 1040), EXPLAIN_PANEL_RGB) draw = ImageDraw.Draw(image) labels = ( "verified square witness", @@ -316,36 +624,48 @@ def _presentation_frame( "pure Basire/Culik port", "checked hex presentation", ) - draw_explain_heading( - draw, - (18, 16), - title="Verified witness presentation", - subtitle=f"verified-transformation stage {stage + 1}/4 | {labels[stage]}", + draw.text( + (36, 16), + "Verified witness presentation", + font=explain_font(56), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (36, 82), + f"Stage {stage + 1}/4 | {labels[stage]}", + font=explain_font(40), + fill=EXPLAIN_MUTED_RGB, ) sources = (square, generalized, generalized, hex_image) - fitted = _fit(sources[stage], (1020, 475)) + fitted = _fit(sources[stage], (1840, 760)) image.paste( fitted, - ((1080 - fitted.width) // 2, 88 + (475 - fitted.height) // 2), + ((1920 - fitted.width) // 2, 152 + (760 - fitted.height) // 2), ) if stage == 2: draw.rounded_rectangle( - (246, 508, 834, 565), - radius=7, + (300, 844, 1620, 926), + radius=14, fill=(239, 242, 246), outline=(55, 126, 168), - width=2, + width=4, ) draw.text( - (278, 525), + (350, 864), "H(N,E,S,W) = (E,S,kappa,W,N,kappa); inverse and matching checked", - font=explain_font(11), + font=explain_font(34), fill=EXPLAIN_TEXT_RGB, ) draw.text( - (18, 594), - "The independent square witness check precedes presentation; raster output proves nothing by itself.", - font=explain_font(9), + (36, 944), + "Pure 1:1 view of the already verified square witness.", + font=explain_font(40), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (36, 992), + "The checker validates the transform; the pixels are presentation only.", + font=explain_font(34), fill=EXPLAIN_MUTED_RGB, ) return image @@ -394,12 +714,117 @@ def render_generalized_assets( sheet = destination / "sheet.png" legend = destination / "atomic-legend.png" _save_png_atomic(compose_generalized_sheet(bundle.tileset.tile_edges), sheet) - _save_png_atomic( - compose_atomic_semantic_legend(bundle.tileset.tile_edges), legend - ) + _save_image(_compose_atomic_legend(bundle.tileset.tile_edges), legend) return GeneralizedOutputs(sheet, legend) +def _compose_atomic_legend( + tile_edges: tuple[tuple[int, int, int, int], ...], +) -> Image.Image: + """Append local matching examples to the checked atomic vocabulary.""" + scale = 2 + vocabulary = Image.fromarray( + compose_atomic_semantic_legend(tile_edges, scale=scale), mode="RGB" + ) + panel_height = 310 * scale + image = Image.new( + "RGB", + (vocabulary.width, vocabulary.height + panel_height), + EXPLAIN_PANEL_RGB, + ) + image.paste(vocabulary, (0, 0)) + draw = ImageDraw.Draw(image) + panel_y = vocabulary.height + draw.line( + (24 * scale, panel_y, image.width - 24 * scale, panel_y), + fill=(181, 188, 199), + width=2 * scale, + ) + draw.text( + (24 * scale, panel_y + 18 * scale), + "Local Wang compatibility uses the shared edge only", + font=explain_font(32 * scale), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (24 * scale, panel_y + 57 * scale), + "Canonical IDs: equal shared colors = valid; unequal = invalid.", + font=explain_font(28 * scale), + fill=EXPLAIN_MUTED_RGB, + ) + + palette = _build_palette_from_edges(tile_edges) + examples = ( + ("VALID", 0, 4, 24 * scale, (213, 237, 224), (52, 145, 94)), + ("INVALID", 0, 3, 447 * scale, (248, 226, 226), (190, 62, 62)), + ) + tile_size = 72 * scale + tile_y = panel_y + 132 * scale + for label, left_id, right_id, card_x, fill, outline in examples: + draw.rounded_rectangle( + ( + card_x, + panel_y + 88 * scale, + card_x + 399 * scale, + panel_y + 290 * scale, + ), + radius=10 * scale, + fill=fill, + outline=outline, + width=3 * scale, + ) + draw.text( + (card_x + 16 * scale, panel_y + 98 * scale), + label, + font=explain_font(28 * scale), + fill=EXPLAIN_TEXT_RGB, + ) + left_x = card_x + 18 * scale + right_x = card_x + 100 * scale + image.paste( + square_explain_tile( + tile_edges[left_id], + palette, + tile_size, + tile_id=left_id, + edge_labels=True, + ), + (left_x, tile_y), + ) + image.paste( + square_explain_tile( + tile_edges[right_id], + palette, + tile_size, + tile_id=right_id, + edge_labels=True, + ), + (right_x, tile_y), + ) + left_color = tile_edges[left_id][1] + right_color = tile_edges[right_id][3] + relation = "=" if left_color == right_color else "!=" + draw.text( + (card_x + 190 * scale, panel_y + 145 * scale), + f"#{left_id} E = {left_color}", + font=explain_font(20 * scale), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (card_x + 190 * scale, panel_y + 184 * scale), + f"{relation} #{right_id} W = {right_color}", + font=explain_font(20 * scale), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (card_x + 190 * scale, panel_y + 230 * scale), + "shared colors agree" if relation == "=" else "shared colors differ", + font=explain_font(18 * scale), + fill=outline, + ) + return image + + def render_presentation_status(status: str, output_path: str | Path) -> Path: if status != "unsat": raise WangSquareRenderError("presentation status is only valid for UNSAT") @@ -489,27 +914,51 @@ def _pipeline_frame(sources: tuple[Image.Image, ...], stage: int) -> Image.Image def _home_preview(square: Image.Image) -> Image.Image: - image = Image.new("RGB", (760, 430), EXPLAIN_PANEL_RGB) + scale = 2 + image = Image.new("RGB", (760 * scale, 430 * scale), EXPLAIN_PANEL_RGB) draw = ImageDraw.Draw(image) draw_explain_heading( draw, - (18, 16), + (18 * scale, 16 * scale), title="Verified SAT witness", subtitle="observed | captured SAT source | square presentation", + scale=scale, ) - fitted = _fit(square, (720, 320)) - image.paste(fitted, ((760 - fitted.width) // 2, 82)) + fitted = _fit(square, (720 * scale, 320 * scale)) + image.paste(fitted, ((image.width - fitted.width) // 2, 82 * scale)) draw.text( - (18, 407), + (18 * scale, 407 * scale), "Preview only; the worked example retains the full source and trust boundary.", - font=explain_font(9), + font=explain_font(9 * scale), fill=EXPLAIN_MUTED_RGB, ) return image -def _worked_example(sources: tuple[Image.Image, ...]) -> Image.Image: - image = Image.new("RGB", (1080, 940), EXPLAIN_PANEL_RGB) +def _worked_example( + sources: tuple[Image.Image, ...], square: Image.Image +) -> Image.Image: + detail_sources = ( + ("Decision | copied Boolean result", sources[1]), + ("Construction | canonical Yang-Zhang region", sources[2]), + ("Check interpretation | six independent receipts", sources[6]), + ("Verified witness | square source", square), + ("Final presentation | checked hex port", sources[7]), + ) + details = tuple( + (label, _fit(source, (1012, 560))) + for label, source in detail_sources + ) + details_top = 958 + detail_gap = 18 + detail_heights = tuple(detail.height + 70 for _, detail in details) + image_height = ( + details_top + + sum(detail_heights) + + detail_gap * (len(details) - 1) + + 54 + ) + image = Image.new("RGB", (1080, image_height), EXPLAIN_PANEL_RGB) draw = ImageDraw.Draw(image) draw_explain_heading( draw, @@ -538,6 +987,30 @@ def _worked_example(sources: tuple[Image.Image, ...]) -> Image.Image: font=explain_font(9), fill=EXPLAIN_MUTED_RGB, ) + y = details_top + for (label, detail), card_height in zip( + details, detail_heights, strict=True + ): + draw.rounded_rectangle( + (18, y, 1062, y + card_height), + radius=9, + fill=EXPLAIN_ACTIVE_RGB, + outline=(181, 188, 199), + ) + draw.text( + (34, y + 14), + label, + font=explain_font(24), + fill=EXPLAIN_TEXT_RGB, + ) + image.paste(detail, ((1080 - detail.width) // 2, y + 54)) + y += card_height + detail_gap + draw.text( + (18, image.height - 32), + "Selected panels retain source detail; the component pages own the full explanations.", + font=explain_font(9), + fill=EXPLAIN_MUTED_RGB, + ) return image @@ -569,7 +1042,7 @@ def render_overview_assets( home_preview = destination / "home-preview.png" worked_example = destination / "worked-example.png" _save_image(_home_preview(home_image), home_preview) - _save_image(_worked_example(sources), worked_example) + _save_image(_worked_example(sources, home_image), worked_example) return OverviewOutputs(animation, home_preview, worked_example) @@ -581,6 +1054,9 @@ def _parser() -> argparse.ArgumentParser: verification = subparsers.add_parser("verification") verification.add_argument("run", type=Path) verification.add_argument("output_directory", type=Path) + verification.add_argument("--manifest", type=Path) + verification.add_argument("--solution", type=Path) + verification.add_argument("--assignment-json") witness = subparsers.add_parser("witness") witness.add_argument("solution", type=Path) witness.add_argument("output_directory", type=Path) @@ -603,7 +1079,28 @@ def main(arguments: list[str] | None = None) -> int: args = parser.parse_args(arguments) try: if args.mode == "verification": - outputs = render_verification_assets(args.run, args.output_directory) + assignment = None + if args.assignment_json is not None: + try: + raw_assignment = json.loads(args.assignment_json) + except json.JSONDecodeError as error: + raise WangSquareRenderError( + f"verification assignment JSON is invalid: {error.msg}" + ) from error + if type(raw_assignment) is not list or any( + type(value) is not bool for value in raw_assignment + ): + raise WangSquareRenderError( + "verification assignment JSON must be a Boolean array" + ) + assignment = tuple(raw_assignment) + outputs = render_verification_assets( + args.run, + args.output_directory, + manifest_path=args.manifest, + solution_path=args.solution, + extracted_assignment=assignment, + ) print(f"animation={outputs.animation}") print(f"contact_sheet={outputs.contact_sheet}") print(f"fallback={outputs.fallback}") diff --git a/renderer/wang_trace_render.py b/renderer/wang_trace_render.py index b161cd5..049502e 100644 --- a/renderer/wang_trace_render.py +++ b/renderer/wang_trace_render.py @@ -10,11 +10,23 @@ from wang_animation import AnimationOutputs, write_animation_assets from wang_explain import ( + EXPLAIN_ACTIVE_RGB, + EXPLAIN_CONFLICT_RGB, + EXPLAIN_DECISION_RGB, EXPLAIN_INACTIVE_DARK_RGB, EXPLAIN_INACTIVE_LIGHT_RGB, EXPLAIN_MUTED_RGB, EXPLAIN_PANEL_RGB, + EXPLAIN_PROPAGATION_SOURCE_RGB, + EXPLAIN_PROPAGATION_TARGET_RGB, + EXPLAIN_RENDER_SCALE, + EXPLAIN_RESTORED_RGB, + EXPLAIN_SELECTED_MRV_RGB, + EXPLAIN_SINGLETON_RGB, EXPLAIN_TEXT_RGB, + EXPLAIN_TRAIL_MUTATION_RGB, + EXPLAIN_UNRESOLVED_RGB, + centered_text, draw_explain_heading, explain_font, ) @@ -23,14 +35,41 @@ from wang_trace import TraceBundle, TraceEvent, load_trace_bundle, replay_trace -_CELL_SIZE: Final = 18 -_MARGIN: Final = 14 -_HEADER: Final = 76 -_LEGEND_WIDTH: Final = 210 -_GAP: Final = 12 -_UNSAT_RGB: Final = (218, 82, 82) -_SINGLETON_RGB: Final = (83, 166, 116) -_CHANGED_RGB: Final = (245, 178, 60) +_CELL_SIZE: Final = 18 * EXPLAIN_RENDER_SCALE +_MARGIN: Final = 14 * EXPLAIN_RENDER_SCALE +_HEADER: Final = 76 * EXPLAIN_RENDER_SCALE +_LEGEND_WIDTH: Final = 210 * EXPLAIN_RENDER_SCALE +_GAP: Final = 12 * EXPLAIN_RENDER_SCALE +_UNSAT_RGB: Final = EXPLAIN_CONFLICT_RGB +_SINGLETON_RGB: Final = EXPLAIN_SINGLETON_RGB +_CHANGED_RGB: Final = EXPLAIN_DECISION_RGB + + +def _scaled(value: int) -> int: + return value * EXPLAIN_RENDER_SCALE + + +def _frame_height(grid_height: int) -> int: + return 2 * _MARGIN + _HEADER + max( + grid_height + _scaled(112), + _scaled(310), + ) + + +def _first_index_after( + events: tuple[TraceEvent, ...], + start: int, + *, + kind: str, +) -> int | None: + return next( + ( + index + for index in range(start + 1, len(events)) + if events[index].kind == kind + ), + None, + ) def select_semantic_milestones( @@ -49,8 +88,88 @@ def select_semantic_milestones( priority = [0, count - 1] for index in range(1, count): - if events[index].phase != events[index - 1].phase: + if events[index].phase == "search" and events[index - 1].phase != "search": priority.extend((index - 1, index)) + + first_decision = next( + ( + index + for index, event in enumerate(events) + if event.kind == "decision" and event.phase == "search" + ), + None, + ) + if first_decision is not None: + priority.append(first_decision) + decision_reduction = next( + ( + index + for index in range(first_decision + 1, count) + if events[index].kind == "domain_reduction" + and events[index].reason == "decision" + and events[index].cell == events[first_decision].cell + ), + None, + ) + if decision_reduction is not None: + priority.append(decision_reduction) + propagation_reduction = next( + ( + index + for index in range(decision_reduction + 1, count) + if events[index].kind == "domain_reduction" + and events[index].reason == "propagation" + ), + None, + ) + if propagation_reduction is not None: + priority.append(propagation_reduction) + + conflict = _first_index_after(events, first_decision, kind="conflict") + if conflict is not None: + empty_reduction = next( + ( + index + for index in range(conflict - 1, first_decision, -1) + if events[index].kind == "domain_reduction" + and events[index].new_domain == 0 + ), + None, + ) + if empty_reduction is not None: + priority.append(empty_reduction) + priority.append(conflict) + backtrack = _first_index_after(events, conflict, kind="backtrack") + if backtrack is not None: + priority.append(backtrack) + next_decision = _first_index_after( + events, backtrack, kind="decision" + ) + if next_decision is not None: + priority.append(next_decision) + else: + final_propagation = next( + ( + index + for index in range(count - 1, first_decision, -1) + if events[index].kind == "propagation" + ), + None, + ) + final_reduction = next( + ( + index + for index in range(count - 1, first_decision, -1) + if events[index].kind == "domain_reduction" + and events[index].reason == "propagation" + ), + None, + ) + if final_propagation is not None: + priority.append(final_propagation) + if final_reduction is not None: + priority.append(final_reduction) + for kind in ( "propagation", "decision", @@ -87,26 +206,391 @@ def select_semantic_milestones( return tuple(sorted(selected)) +def _domain_tiles(domain: int, tile_count: int) -> tuple[int, ...]: + return tuple(tile for tile in range(tile_count) if domain & (1 << tile)) + + +def _format_domain(domain: int, tile_count: int) -> str: + return "{" + ", ".join(map(str, _domain_tiles(domain, tile_count))) + "}" + + +def _propagation_reason( + bundle: TraceBundle, + event: TraceEvent, + before: tuple[int, ...], +) -> tuple[int, str, str, tuple[int, ...]] | None: + """Derive one unique adjacent support reason from a validated before-state.""" + if ( + event.kind != "domain_reduction" + or event.reason != "propagation" + or event.cell is None + or event.old_domain is None + or event.new_domain is None + ): + return None + region = bundle.explanation.region + target_x = event.cell % region.width + target_y = event.cell // region.width + tiles = bundle.explanation.tileset.tile_edges + relations = ( + (0, -1, "S", 2, "N", 0), + (1, 0, "W", 3, "E", 1), + (0, 1, "N", 0, "S", 2), + (-1, 0, "E", 1, "W", 3), + ) + candidates: list[tuple[int, str, str, tuple[int, ...]]] = [] + for dx, dy, source_side, source_edge, target_side, target_edge in relations: + source_x = target_x + dx + source_y = target_y + dy + if not (0 <= source_x < region.width and 0 <= source_y < region.height): + continue + source_cell = source_y * region.width + source_x + if not region.active[source_cell]: + continue + source_colors = { + tiles[tile][source_edge] + for tile in _domain_tiles(before[source_cell], len(tiles)) + } + supported = sum( + 1 << tile + for tile in _domain_tiles(event.old_domain, len(tiles)) + if tiles[tile][target_edge] in source_colors + ) + if supported != event.new_domain: + continue + shared_colors = tuple( + sorted( + { + tiles[tile][target_edge] + for tile in _domain_tiles(event.new_domain, len(tiles)) + } + & source_colors + ) + ) + candidates.append((source_cell, source_side, target_side, shared_colors)) + return candidates[0] if len(candidates) == 1 else None + + +def _restored_changes( + events: tuple[TraceEvent, ...], backtrack_index: int +) -> tuple[tuple[int, int, int], ...]: + """Return observed deltas restored by one backtrack in reverse trail order.""" + trail: list[tuple[int, int, int]] = [] + for event in events[:backtrack_index]: + if event.kind == "domain_reduction": + assert ( + event.cell is not None + and event.old_domain is not None + and event.new_domain is not None + ) + trail.append((event.cell, event.new_domain, event.old_domain)) + elif event.kind == "backtrack": + del trail[event.change_mark :] + backtrack = events[backtrack_index] + if backtrack.kind != "backtrack": + return () + return tuple(reversed(trail[backtrack.change_mark :])) + + +def _previous_search_event( + events: tuple[TraceEvent, ...], index: int, kind: str +) -> TraceEvent | None: + return next( + (event for event in reversed(events[:index]) if event.kind == kind), + None, + ) + + +def _next_search_event( + events: tuple[TraceEvent, ...], index: int, kind: str +) -> TraceEvent | None: + return next( + (event for event in events[index + 1 :] if event.kind == kind), + None, + ) + + def _domain_rgb(domain: int) -> tuple[int, int, int]: if domain == 0: return _UNSAT_RGB count = domain.bit_count() if count == 1: return _SINGLETON_RGB - shade = 225 - min(12, count - 2) * 6 - return (128, max(145, shade - 24), shade) + return EXPLAIN_UNRESOLVED_RGB + + +def _active_domain_counts( + active: tuple[bool, ...], domains: tuple[int, ...] +) -> tuple[int, int]: + """Return fixed and empty domains, excluding inactive bounding-box cells.""" + return ( + sum( + is_active and domain.bit_count() == 1 + for is_active, domain in zip(active, domains, strict=True) + ), + sum( + is_active and domain == 0 + for is_active, domain in zip(active, domains, strict=True) + ), + ) + + +def _summary_box( + draw: ImageDraw.ImageDraw, + *, + top: int, + width: int, + height: int, +) -> tuple[int, int, int, int] | None: + box = (_MARGIN, top, width - _MARGIN - 1, height - _MARGIN - 1) + if box[3] - box[1] < _scaled(82): + return None + draw.rectangle( + box, + fill=EXPLAIN_ACTIVE_RGB, + outline=(178, 184, 194), + width=_scaled(1), + ) + return box + + +def _draw_propagation_summary( + draw: ImageDraw.ImageDraw, + bundle: TraceBundle, + event: TraceEvent, + reason: tuple[int, str, str, tuple[int, ...]], + *, + top: int, + width: int, + height: int, +) -> None: + box = _summary_box(draw, top=top, width=width, height=height) + if box is None: + return + assert event.cell is not None + assert event.old_domain is not None + assert event.new_domain is not None + tile_count = len(bundle.explanation.tileset.tile_edges) + source_cell, source_side, target_side, colors = reason + removed = event.old_domain & ~event.new_domain + x = _MARGIN + _scaled(12) + draw.text( + (x, top + _scaled(9)), + f"Propagation: cell {source_cell} {source_side} -> " + f"cell {event.cell} {target_side}", + font=explain_font(_scaled(24)), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (x, top + _scaled(39)), + "Shared edge " + + ", ".join(map(str, colors)) + + "; unique in observed before-state", + font=explain_font(_scaled(24)), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (x, top + _scaled(69)), + f"Domain {_format_domain(event.old_domain, tile_count)} -> " + f"{_format_domain(event.new_domain, tile_count)}; " + f"removed {_format_domain(removed, tile_count)}", + font=explain_font(_scaled(24)), + fill=EXPLAIN_TEXT_RGB, + ) + + card_width = _scaled(88) + card_height = _scaled(58) + card_gap = _scaled(28) + target_left = width - _MARGIN - card_width + source_left = target_left - card_gap - card_width + card_top = top + _scaled(16) + for left, color, title, cell in ( + (source_left, EXPLAIN_PROPAGATION_SOURCE_RGB, "source", source_cell), + (target_left, EXPLAIN_PROPAGATION_TARGET_RGB, "restricted", event.cell), + ): + draw.rectangle( + (left, card_top, left + card_width, card_top + card_height), + fill=color, + outline=EXPLAIN_TEXT_RGB, + width=_scaled(1), + ) + centered_text( + draw, + (left, card_top, left + card_width, card_top + card_height), + f"{title}\ncell {cell}", + font=explain_font(_scaled(13)), + ) + arrow_y = card_top + card_height // 2 + draw.line( + (source_left + card_width, arrow_y, target_left, arrow_y), + fill=EXPLAIN_TEXT_RGB, + width=_scaled(2), + ) + draw.polygon( + ( + (target_left, arrow_y), + (target_left - _scaled(7), arrow_y - _scaled(5)), + (target_left - _scaled(7), arrow_y + _scaled(5)), + ), + fill=EXPLAIN_TEXT_RGB, + ) + + +def _draw_search_summary( + draw: ImageDraw.ImageDraw, + bundle: TraceBundle, + event: TraceEvent, + event_index: int, + restored: tuple[tuple[int, int, int], ...], + *, + top: int, + width: int, + height: int, +) -> None: + box = _summary_box(draw, top=top, width=width, height=height) + if box is None: + return + events = bundle.trace.events + decision = _previous_search_event(events, event_index, "decision") + conflict = ( + event + if event.kind == "conflict" + else _previous_search_event(events, event_index, "conflict") + ) + next_decision = _next_search_event(events, event_index, "decision") + tile_count = len(bundle.explanation.tileset.tile_edges) + x = _MARGIN + _scaled(12) + if decision is not None and decision.cell is not None and decision.new_domain: + chosen = _format_domain(decision.new_domain, tile_count) + title = ( + f"DFS conflict d{event.depth}: " + if event.kind == "conflict" + else f"Rollback d{event.depth}: " + ) + title += f"cell {decision.cell} branch {chosen}" + else: + title = ( + f"DFS conflict at depth {event.depth}" + if event.kind == "conflict" + else f"Rollback at depth {event.depth}" + ) + draw.text( + (x, top + _scaled(9)), + title, + font=explain_font(_scaled(24)), + fill=EXPLAIN_TEXT_RGB, + ) + if event.kind == "conflict": + draw.text( + (x, top + _scaled(46)), + f"Cell {event.cell} -> empty domain; trail {event.change_mark}", + font=explain_font(_scaled(24)), + fill=EXPLAIN_TEXT_RGB, + ) + else: + conflict_mark = ( + conflict.change_mark if conflict is not None else event.change_mark + ) + draw.text( + (x, top + _scaled(40)), + f"Restore {len(restored)} changes in reverse; " + f"trail {conflict_mark} -> {event.change_mark}", + font=explain_font(_scaled(24)), + fill=EXPLAIN_TEXT_RGB, + ) + if restored: + sample = "; ".join( + f"cell {cell}: {_format_domain(current, tile_count)} -> " + f"{_format_domain(previous, tile_count)}" + for cell, current, previous in restored[:2] + ) + draw.text( + (x, top + _scaled(70)), + f"First restores: {sample}", + font=explain_font(_scaled(24)), + fill=EXPLAIN_TEXT_RGB, + ) + + card_width = _scaled(82) + card_height = _scaled(58) + card_gap = _scaled(10) + cards_left = width - _MARGIN - 3 * card_width - 2 * card_gap + card_top = top + _scaled(17) + next_label = "next\nbranch" + if ( + next_decision is not None + and next_decision.cell is not None + and next_decision.new_domain is not None + ): + next_label = ( + "next " + + _format_domain(next_decision.new_domain, tile_count) + + f"\ncell {next_decision.cell}" + ) + elif next_decision is None: + next_label = "search\nend" + for offset, color, label in ( + (0, EXPLAIN_DECISION_RGB, "candidate\nbranch"), + (1, EXPLAIN_CONFLICT_RGB, "empty\ndomain"), + (2, EXPLAIN_RESTORED_RGB, next_label), + ): + left = cards_left + offset * (card_width + card_gap) + draw.rectangle( + (left, card_top, left + card_width, card_top + card_height), + fill=color, + outline=EXPLAIN_TEXT_RGB, + width=_scaled(1), + ) + centered_text( + draw, + (left, card_top, left + card_width, card_top + card_height), + label, + font=explain_font(_scaled(12)), + ) + if offset < 2: + arrow_y = card_top + card_height // 2 + draw.line( + (left + card_width, arrow_y, left + card_width + card_gap, arrow_y), + fill=EXPLAIN_TRAIL_MUTATION_RGB, + width=_scaled(2), + ) def _compose_frame( bundle: TraceBundle, event: TraceEvent, domains: tuple[int, ...], + before: tuple[int, ...], + event_index: int, ) -> Image.Image: region = bundle.explanation.region + fixed_count, empty_count = _active_domain_counts(region.active, domains) + propagation = _propagation_reason(bundle, event, before) + restored = ( + _restored_changes(bundle.trace.events, event_index) + if event.kind == "backtrack" + else () + ) + restored_cells = {cell for cell, _, _ in restored} + mrv_candidates: tuple[int, ...] = () + minimum_domain_size: int | None = None + if event.kind == "decision": + unresolved = tuple( + (index, domain.bit_count()) + for index, (active, domain) in enumerate( + zip(region.active, domains, strict=True) + ) + if active and domain.bit_count() > 1 + ) + if unresolved: + minimum_domain_size = min(count for _, count in unresolved) + mrv_candidates = tuple( + index for index, count in unresolved if count == minimum_domain_size + ) grid_width = region.width * _CELL_SIZE grid_height = region.height * _CELL_SIZE width = 2 * _MARGIN + grid_width + _GAP + _LEGEND_WIDTH - height = 2 * _MARGIN + _HEADER + max(grid_height, 310) + height = _frame_height(grid_height) if ( width > MAX_CANVAS_SIDE or height > MAX_CANVAS_SIDE @@ -130,6 +614,7 @@ def _compose_frame( (_MARGIN, _MARGIN), title=f"Observed {bundle.trace.solver} solver trace", subtitle=subtitle, + scale=EXPLAIN_RENDER_SCALE, ) top = _MARGIN + _HEADER for index, (active, domain) in enumerate( @@ -146,64 +631,213 @@ def _compose_frame( ) else: fill = _domain_rgb(domain) - draw.rectangle(box, fill=fill, outline=(178, 184, 194)) - if active and domain != 0 and domain.bit_count() == 1: - tile_id = domain.bit_length() - 1 - draw.text( - (x + 4, y + 2), - str(tile_id), - font=explain_font(9), - fill=EXPLAIN_TEXT_RGB, + if index in mrv_candidates: + fill = EXPLAIN_SELECTED_MRV_RGB + if propagation is not None and index == propagation[0]: + fill = EXPLAIN_PROPAGATION_SOURCE_RGB + if propagation is not None and index == event.cell: + fill = EXPLAIN_PROPAGATION_TARGET_RGB + if index in restored_cells: + fill = EXPLAIN_RESTORED_RGB + draw.rectangle(box, fill=fill, outline=(178, 184, 194), width=_scaled(1)) + if active: + centered_text( + draw, + box, + str(domain.bit_count()), + font=explain_font(_scaled(10)), ) if event.cell == index: - draw.rectangle(box, outline=_CHANGED_RGB, width=3) + draw.rectangle(box, outline=_CHANGED_RGB, width=_scaled(3)) legend_x = _MARGIN + grid_width + _GAP - legend_y = top + 4 + legend_y = top + _scaled(4) draw.text( (legend_x, legend_y), "Domain state", - font=explain_font(14), + font=explain_font(_scaled(14)), fill=EXPLAIN_TEXT_RGB, ) - entries = ( + entries = [ (_SINGLETON_RGB, "singleton / selected tile"), - (_domain_rgb(8), "multiple candidate tiles"), + (EXPLAIN_UNRESOLVED_RGB, "multiple candidate tiles"), (_UNSAT_RGB, "empty domain / conflict"), (_CHANGED_RGB, "current event cell"), - ) + ] + if propagation is not None: + entries.extend( + ( + (EXPLAIN_PROPAGATION_SOURCE_RGB, "derived support source"), + (EXPLAIN_PROPAGATION_TARGET_RGB, "restricted target"), + ) + ) + if restored: + entries.append((EXPLAIN_RESTORED_RGB, "restored by rollback")) for offset, (color, label) in enumerate(entries, start=1): - y = legend_y + offset * 28 - draw.rectangle((legend_x, y, legend_x + 18, y + 18), fill=color) + y = legend_y + offset * _scaled(24) + draw.rectangle( + (legend_x, y, legend_x + _scaled(18), y + _scaled(18)), fill=color + ) draw.text( - (legend_x + 26, y + 2), + (legend_x + _scaled(26), y + _scaled(2)), label, - font=explain_font(10), + font=explain_font(_scaled(10)), fill=EXPLAIN_TEXT_RGB, ) - details = [ - f"phase: {event.phase or '-'}", - f"reason: {event.reason or '-'}", - f"change mark: {event.change_mark}", - f"active: {sum(region.active)}", - f"fixed: {sum(domain.bit_count() == 1 for domain in domains)}", - f"empty: {sum(domain == 0 for domain in domains)}", - ] - y = legend_y + 142 + if mrv_candidates: + y = legend_y + (len(entries) + 1) * _scaled(24) + draw.rectangle( + (legend_x, y, legend_x + _scaled(18), y + _scaled(18)), + fill=EXPLAIN_SELECTED_MRV_RGB, + ) + draw.text( + (legend_x + _scaled(26), y + _scaled(2)), + "minimum-domain candidate", + font=explain_font(_scaled(10)), + fill=EXPLAIN_TEXT_RGB, + ) + if mrv_candidates: + details = [ + "active: " + f"{sum(region.active)} | fixed: " + f"{fixed_count} | empty: {empty_count}", + "minimum domain: " + f"{minimum_domain_size}; tied candidates: {len(mrv_candidates)}", + f"row-major winner: cell {min(mrv_candidates)}", + f"selected cell: {event.cell}", + "tie-break: lowest row-major cell", + ] + elif propagation is not None: + source_cell, source_side, target_side, colors = propagation + details = [ + f"phase: {event.phase or '-'}", + f"source: cell {source_cell} {source_side}", + f"target: cell {event.cell} {target_side}", + "shared edge: " + ", ".join(map(str, colors)), + "source derived from before-state", + ] + elif restored: + details = [ + f"phase: {event.phase or '-'}", + f"rollback depth: {event.depth}", + f"trail mark: {event.change_mark}", + f"restored changes: {len(restored)}", + f"restored cells: {len(restored_cells)}", + ] + else: + details = [ + f"phase: {event.phase or '-'}", + f"reason: {event.reason or '-'}", + f"change mark: {event.change_mark}", + f"active: {sum(region.active)}", + f"fixed: {fixed_count}", + f"empty: {empty_count}", + ] + y = legend_y + _scaled(155 if mrv_candidates else 190 if len(entries) > 4 else 142) for line in details: draw.text( (legend_x, y), line, - font=explain_font(10), + font=explain_font(_scaled(10)), + fill=EXPLAIN_MUTED_RGB, + ) + y += _scaled(15) + summary_top = top + grid_height + _scaled(12) + if mrv_candidates: + summary_box = ( + _MARGIN, + summary_top, + width - _MARGIN - 1, + height - _MARGIN - 1, + ) + draw.rectangle( + summary_box, + fill=EXPLAIN_ACTIVE_RGB, + outline=(178, 184, 194), + width=_scaled(1), + ) + summary_x = _MARGIN + _scaled(12) + draw.text( + (summary_x, summary_top + _scaled(10)), + f"MRV: minimum domain {minimum_domain_size}", + font=explain_font(_scaled(26)), + fill=EXPLAIN_TEXT_RGB, + ) + draw.text( + (summary_x, summary_top + _scaled(42)), + f"{len(mrv_candidates)} ties -> cell {min(mrv_candidates)} wins row-major", + font=explain_font(_scaled(24)), + fill=EXPLAIN_TEXT_RGB, + ) + recorded_domain = _format_domain( + event.new_domain or 0, + len(bundle.explanation.tileset.tile_edges), + ) + draw.text( + (summary_x, summary_top + _scaled(72)), + f"Recorded decision: cell {event.cell} -> {recorded_domain}", + font=explain_font(_scaled(16)), + fill=EXPLAIN_MUTED_RGB, + ) + card_width = _scaled(75) + card_height = _scaled(62) + card_gap = _scaled(12) + card_top = summary_top + _scaled(16) + candidate_left = width - _MARGIN - 2 * card_width - card_gap + winner_left = candidate_left + card_width + card_gap + alternate = next( + (candidate for candidate in mrv_candidates if candidate != event.cell), + event.cell, + ) + for left, color, title, cell in ( + (candidate_left, EXPLAIN_SELECTED_MRV_RGB, "tied", alternate), + (winner_left, _CHANGED_RGB, "winner", event.cell), + ): + draw.rectangle( + (left, card_top, left + card_width, card_top + card_height), + fill=color, + outline=EXPLAIN_TEXT_RGB, + width=_scaled(1), + ) + centered_text( + draw, + ( + left, + card_top + _scaled(6), + left + card_width, + card_top + card_height, + ), + f"{title}\ncell {cell}\ndomain {minimum_domain_size}", + font=explain_font(_scaled(12)), + ) + elif propagation is not None: + _draw_propagation_summary( + draw, + bundle, + event, + propagation, + top=summary_top, + width=width, + height=height, + ) + elif event.kind in {"conflict", "backtrack"}: + _draw_search_summary( + draw, + bundle, + event, + event_index, + restored, + top=summary_top, + width=width, + height=height, + ) + else: + draw.text( + (legend_x, height - _MARGIN - _scaled(15)), + "Rendering is not a correctness proof.", + font=explain_font(_scaled(9)), fill=EXPLAIN_MUTED_RGB, ) - y += 18 - draw.text( - (legend_x, height - _MARGIN - 15), - "Rendering is not a correctness proof.", - font=explain_font(9), - fill=EXPLAIN_MUTED_RGB, - ) return image @@ -219,7 +853,15 @@ def render_trace_assets( states = replay_trace(bundle.trace) selected = select_semantic_milestones(bundle.trace.events, max_frames) frames = tuple( - _compose_frame(bundle, bundle.trace.events[index], states[index]) + _compose_frame( + bundle, + bundle.trace.events[index], + states[index - 1] + if bundle.trace.events[index].kind == "decision" and index > 0 + else states[index], + bundle.trace.initial_domains if index == 0 else states[index - 1], + index, + ) for index in selected ) fallback_index = next( diff --git a/renderer/wang_z3_summary.py b/renderer/wang_z3_summary.py index 5989546..b358265 100644 --- a/renderer/wang_z3_summary.py +++ b/renderer/wang_z3_summary.py @@ -5,6 +5,7 @@ import argparse from dataclasses import dataclass from pathlib import Path +from typing import NamedTuple from PIL import Image, ImageDraw @@ -17,9 +18,11 @@ EXPLAIN_TEXT_RGB, draw_explain_heading, explain_font, + square_explain_tile, ) from wang_hex_port import WangSquareRenderError from wang_snapshot import ( + ExplainabilityBundle, _array, _fields, _integer, @@ -28,7 +31,9 @@ _read_bytes, _sha256, _string, + load_explainability_bundle, ) +from wang_square import _build_palette_from_edges SCHEMA_NAME = "z3-encoding-summary-v1" @@ -72,6 +77,16 @@ class Z3EncodingSummary: statistics: tuple[tuple[str, int], ...] +class _WangExampleEvidence(NamedTuple): + x: int + y: int + tile_id: int + right_id: int + tile_edges: tuple[int, int, int, int] + right_edges: tuple[int, int, int, int] + required_n: int + + def _fail(path: str, message: str) -> None: raise WangSquareRenderError(f"Z3 encoding summary {path}: {message}") @@ -271,212 +286,330 @@ def load_z3_encoding_summary(path: str | Path) -> Z3EncodingSummary: ) -def _compose_wang_frame(summary: Z3EncodingSummary, stage: int) -> Image.Image: - width, height = 940, 430 +def _boolean_clause_lines( + bundle: ExplainabilityBundle, +) -> tuple[tuple[str, str], ...]: + return tuple( + ( + f"c{clause_id} source positions: " + + ", ".join(f"x{variable}" for variable in clause), + " + ".join(f"If(x{variable})" for variable in clause) + " = 1", + ) + for clause_id, clause in enumerate(bundle.formula.clauses) + ) + + +def _bind_oracle_inputs( + summary: Z3EncodingSummary, bundle: ExplainabilityBundle +) -> None: + if summary.source_formula_sha256 != bundle.source_formula_sha256: + raise WangSquareRenderError( + "Z3 summary source formula identity disagrees with explainability bundle" + ) + if summary.variable_count != bundle.formula.variable_count: + raise WangSquareRenderError( + "Z3 summary variable count disagrees with explainability bundle" + ) + if summary.engine != WANG_ENGINE: + return + reduction = bundle.reduction + if reduction is None or summary.region_sha256 != reduction.region_sha256: + raise WangSquareRenderError( + "Z3 summary region identity disagrees with explainability bundle" + ) + if (summary.width, summary.height) != (bundle.region.width, bundle.region.height): + raise WangSquareRenderError( + "Z3 summary region dimensions disagree with explainability bundle" + ) + if summary.active_cell_count != sum(bundle.region.active): + raise WangSquareRenderError( + "Z3 summary active-cell count disagrees with explainability bundle" + ) + if summary.unique_tile_tuple_count != len(bundle.tileset.tile_edges): + raise WangSquareRenderError( + "Z3 summary canonical tile table disagrees with explainability bundle" + ) + if summary.cells is not None and any( + (tile_id is None) == active + for tile_id, active in zip(summary.cells, bundle.region.active, strict=True) + ): + raise WangSquareRenderError( + "Z3 model projection active cells disagree with explainability bundle" + ) + + +def _wang_example_evidence( + summary: Z3EncodingSummary, bundle: ExplainabilityBundle +) -> _WangExampleEvidence: + if summary.cells is None: + raise WangSquareRenderError("Wang SAT example requires a returned model") + region = bundle.region + selected: tuple[int, int] | None = None + for index, active in enumerate(region.active): + if not active: + continue + column = index % region.width + sides = region.boundary[index] + if ( + column + 1 < region.width + and region.active[index + 1] + and sides is not None + and sides[0] is not None + ): + selected = (index, 0) + break + if selected is None: + raise WangSquareRenderError( + "Wang explanation needs an active cell with an east neighbor and exposed north edge" + ) + index, boundary_direction = selected + right_index = index + 1 + tile_id = summary.cells[index] + right_id = summary.cells[right_index] + if tile_id is None or right_id is None: + raise WangSquareRenderError("Wang explanation selected an inactive model cell") + tile = bundle.tileset.tile_edges[tile_id] + right_tile = bundle.tileset.tile_edges[right_id] + if tile[1] != right_tile[3]: + raise WangSquareRenderError("Wang example internal term has unequal model colors") + boundary = region.boundary[index] + assert boundary is not None and boundary[boundary_direction] is not None + required = boundary[boundary_direction] + if tile[boundary_direction] != required: + raise WangSquareRenderError("Wang example does not satisfy its exposed boundary") + x = region.min_x + index % region.width + y = region.min_y + index // region.width + return _WangExampleEvidence( + x=x, + y=y, + tile_id=tile_id, + right_id=right_id, + tile_edges=tile, + right_edges=right_tile, + required_n=required, + ) + + +def _compose_wang_frame( + summary: Z3EncodingSummary, bundle: ExplainabilityBundle, stage: int +) -> Image.Image: + width, height = 1880, 1040 image = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB) draw = ImageDraw.Draw(image) - labels = ( - "configuration", - "edge terms", - "shared internal edges", - "cell relations and boundaries", - "result, model, and encoding statistics", - ) + labels = ("terms", "shared", "tile tuple", "boundary", "model") draw_explain_heading( draw, - (18, 16), + (36, 20), title="Wang Z3 encoding order", subtitle=( - f"encoding-order stage {stage + 1}/5 | {labels[stage]} | " - "not a Z3 internal execution trace" + f"encoding-order {stage + 1}/5 | row-major cells, then N/E/S/W | " + "project construction, not Z3 search" ), + scale=2, ) - draw.text( - (18, 78), - f"Z3 {summary.version} | random_seed={summary.random_seed} | " - f"threads={summary.threads}", - font=explain_font(12), - fill=EXPLAIN_TEXT_RGB, - ) - steps = ( - "1. create edge terms in row-major cell order", - "2. share north/south and east/west internal terms", - "3. add one positional tile-tuple relation per active cell", - "4. add exposed boundary equalities in N,E,S,W order", - "5. check once; copy model and encoding statistics", - ) - for index, label in enumerate(steps): - y = 112 + index * 38 + for index, label in enumerate(labels): + x = 36 + index * 362 active = index <= stage draw.rounded_rectangle( - (18, y, 455, y + 28), - radius=5, + (x, 118, x + 332, 184), + radius=10, fill=(213, 235, 246) if active else (239, 241, 245), outline=(54, 127, 169) if index == stage else (184, 190, 201), - width=2 if index == stage else 1, + width=4 if index == stage else 2, ) draw.text( - (29, y + 7), - label, - font=explain_font(10), + (x + 20, 136), + f"{index + 1} {label}", + font=explain_font(28), fill=EXPLAIN_TEXT_RGB if active else EXPLAIN_MUTED_RGB, ) - - panel = (485, 106, 922, 402) - draw.rounded_rectangle(panel, radius=6, fill=EXPLAIN_ACTIVE_RGB, outline=(180, 187, 198)) - if stage == 0: - lines = ( - f"formula variables: {summary.variable_count}", - f"region: {summary.width} x {summary.height}", - f"active cells: {summary.active_cell_count}", - "project order is public; Z3 search order is not", + if summary.status != "sat": + draw.rounded_rectangle( + (36, 216, 1844, 968), + radius=18, + fill=(239, 242, 246), + outline=(180, 187, 198), + width=2, ) - elif stage == 1: - lines = ( - f"distinct edge terms: {summary.edge_term_count}", - "N and W reuse already-created neighbor terms", - "E and S create the forward row-major frontier", + draw.text( + (104, 294), + f"Wang Z3 result: {summary.status.upper()}", + font=explain_font(64), + fill=EXPLAIN_TEXT_RGB, ) - elif stage == 2: - lines = ( - f"shared internal edges: {summary.shared_internal_edge_count}", - "one arithmetic term represents both sides of an adjacency", - "no support implications or copied native propagation", + draw.text( + (104, 420), + "Cell / tile example: not applicable", + font=explain_font(52), + fill=EXPLAIN_TEXT_RGB, ) - elif stage == 3: - lines = ( - f"unique tile tuples: {summary.unique_tile_tuple_count}", - f"assertions: {summary.assertion_count}", - "cell relation precedes boundary equalities", + draw.text( + (1010, 420), + "Returned model: not applicable", + font=explain_font(52), + fill=EXPLAIN_TEXT_RGB, ) - else: - lines = ( - f"result: {summary.status.upper()}", - f"model cells: {0 if summary.cells is None else len(summary.cells)}", - f"encoding statistics: {len(summary.statistics)}", - "internal Z3 counters and debug order are not claimed", + draw.text( + (104, 548), + "No satisfying model was returned." + if summary.status == "unsat" + else "No model was returned; no result is inferred.", + font=explain_font(44), + fill=EXPLAIN_MUTED_RGB, + ) + draw.text( + (104, 650), + "No cell, tile tuple, boundary, witness, or certificate is claimed.", + font=explain_font(44), + fill=EXPLAIN_MUTED_RGB, ) - y = 124 - for line in lines: - draw.text((502, y), line, font=explain_font(11), fill=EXPLAIN_TEXT_RGB) - y += 27 - - if stage == 4 and summary.cells is not None: - cell = 8 - origin_x, origin_y = 502, 246 + draw.text( + (36, 996), + "Project construction order only; Z3 internal search decisions are not exposed.", + font=explain_font(32), + fill=EXPLAIN_MUTED_RGB, + ) + return image + + evidence = _wang_example_evidence(summary, bundle) + draw.rounded_rectangle((36, 216, 930, 968), radius=18, fill=EXPLAIN_ACTIVE_RGB, outline=(180, 187, 198), width=2) + draw.text((72, 244), "One real cell relation", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + if summary.cells is not None: + tile_id = evidence.tile_id + right_id = evidence.right_id + palette = _build_palette_from_edges(bundle.tileset.tile_edges) + left_edges = evidence.tile_edges + right_edges = evidence.right_edges + image.paste(square_explain_tile(left_edges, palette, 280, tile_id=tile_id, edge_labels=True), (94, 382)) + image.paste(square_explain_tile(right_edges, palette, 280, tile_id=right_id, edge_labels=True), (500, 382)) + draw.line((374, 522, 500, 522), fill=(54, 127, 169), width=12) + draw.text((382, 456), f"E = W", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + draw.text((404, 530), f"{left_edges[1]}", font=explain_font(56), fill=(32, 103, 148)) + draw.text((160, 314), f"active cell ({evidence.x},{evidence.y}) -> returned tile #{tile_id}", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + draw.text((78, 704), f"tile #{tile_id}: N{left_edges[0]} E{left_edges[1]} S{left_edges[2]} W{left_edges[3]}", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + draw.text((78, 782), f"shared term: E{left_edges[1]} = W{right_edges[3]}", font=explain_font(52), fill=EXPLAIN_TEXT_RGB) + draw.text((78, 864), f"boundary: N{left_edges[0]} = required N{evidence.required_n}", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + + draw.rounded_rectangle((960, 216, 1844, 968), radius=18, fill=EXPLAIN_ACTIVE_RGB, outline=(180, 187, 198), width=2) + draw.text((996, 244), "Returned model projection", font=explain_font(48), fill=EXPLAIN_TEXT_RGB) + draw.text((996, 316), f"{summary.width} x {summary.height} | {summary.active_cell_count} active", font=explain_font(42), fill=EXPLAIN_MUTED_RGB) + if summary.cells is not None: + cell = max(2, min(18, 800 // summary.width, 300 // summary.height)) + origin_x, origin_y = 996, 420 for index, tile_id in enumerate(summary.cells): x = origin_x + (index % summary.width) * cell y = origin_y + (index // summary.width) * cell fill = (205, 210, 218) if tile_id is None else (88, 170, 122) draw.rectangle((x, y, x + cell - 1, y + cell - 1), fill=fill) draw.text( - (502, 346), - "model projection (inactive positions in gray)", - font=explain_font(9), + (996, 420 + summary.height * cell + 34), + "green = tile ID gray = inactive", + font=explain_font(42), fill=EXPLAIN_MUTED_RGB, ) + draw.text((996, 754), f"copied {summary.status.upper()} model", font=explain_font(52), fill=EXPLAIN_TEXT_RGB) + draw.text((996, 830), f"{len(summary.cells)} dense entries", font=explain_font(44), fill=EXPLAIN_TEXT_RGB) draw.text( - (18, 408), - "Rendering explains the declared encoding order; it makes no claim about Z3's internal decisions.", - font=explain_font(9), + (36, 996), + "Project construction order and returned projection only; Z3 internal search decisions are not exposed.", + font=explain_font(32), fill=EXPLAIN_MUTED_RGB, ) return image -def _compose_boolean_frame(summary: Z3EncodingSummary, stage: int) -> Image.Image: - width, height = 940, 430 +def _compose_boolean_frame( + summary: Z3EncodingSummary, bundle: ExplainabilityBundle, stage: int +) -> Image.Image: + width, height = 1880, 1040 image = Image.new("RGB", (width, height), EXPLAIN_PANEL_RGB) draw = ImageDraw.Draw(image) - labels = ( - "configuration", - "Boolean variables", - "source-order clauses", - "result, assignment, and encoding statistics", - ) + labels = ("variables", "source order", "ExactlyOne", "model") draw_explain_heading( draw, - (18, 16), + (36, 20), title="Boolean Z3 encoding order", subtitle=( - f"encoding-order stage {stage + 1}/4 | {labels[stage]} | " - "not a Z3 internal execution trace" + f"encoding-order {stage + 1}/4 | repeated positions stay distinct | " + "project construction, not Z3 search" ), + scale=2, ) - draw.text( - (18, 78), - f"Z3 {summary.version} | random_seed={summary.random_seed} | " - f"threads={summary.threads}", - font=explain_font(12), - fill=EXPLAIN_TEXT_RGB, - ) - steps = ( - "1. create one Boolean term per variable in ascending ID order", - "2. visit clauses in source order", - "3. visit each clause left-to-right and assert exactly one true", - "4. check once; copy assignment and project-owned statistics", - ) - for index, label in enumerate(steps): - y = 112 + index * 48 + for index, label in enumerate(labels): + x = 36 + index * 452 active = index <= stage draw.rounded_rectangle( - (18, y, 520, y + 34), - radius=5, + (x, 118, x + 420, 184), + radius=10, fill=(213, 235, 246) if active else (239, 241, 245), outline=(54, 127, 169) if index == stage else (184, 190, 201), - width=2 if index == stage else 1, + width=4 if index == stage else 2, ) draw.text( - (29, y + 9), - label, - font=explain_font(10), + (x + 20, 136), + f"{index + 1} {label}", + font=explain_font(28), fill=EXPLAIN_TEXT_RGB if active else EXPLAIN_MUTED_RGB, ) - draw.rounded_rectangle( - (548, 106, 922, 378), - radius=6, - fill=EXPLAIN_ACTIVE_RGB, - outline=(180, 187, 198), - ) - if stage == 0: - lines = ( - f"formula variables: {summary.variable_count}", - "fixed seed and one solver thread", - "project order is public; Z3 search order is not", - ) - elif stage == 1: - lines = ( - f"Boolean terms: {summary.variable_count}", - "term IDs follow the formula variable IDs", - "no native-solver state is imported", - ) - elif stage == 2: - lines = ( - f"assertions: {summary.assertion_count}", - "clause order follows the parsed source", - "literal positions remain left-to-right", - ) + draw.rounded_rectangle((36, 216, 1844, 968), radius=18, fill=EXPLAIN_ACTIVE_RGB, outline=(180, 187, 198), width=2) + clause_lines = _boolean_clause_lines(bundle) + if len(clause_lines) <= 3: + selected = tuple(enumerate(clause_lines)) + omission = None else: - assignment = summary.assignment or () - assignment_text = ", ".join( - f"x{index + 1}={'1' if value else '0'}" - for index, value in enumerate(assignment) + selected = ((0, clause_lines[0]), (1, clause_lines[1]), (len(clause_lines) - 1, clause_lines[-1])) + omission = f"{len(clause_lines) - 3} source clauses omitted between c1 and c{len(clause_lines) - 1}" + draw.text((72, 244), "Source positions", font=explain_font(40), fill=EXPLAIN_TEXT_RGB) + draw.text((1040, 244), "Actual sum asserted equal to one", font=explain_font(40), fill=EXPLAIN_TEXT_RGB) + if omission is not None: + draw.text((72, 291), omission, font=explain_font(28), fill=EXPLAIN_MUTED_RGB) + for row, (clause_id, (_, equation)) in enumerate(selected): + y = 330 + row * 176 + visible = stage >= 2 + draw.rounded_rectangle( + (72, y, 800, y + 128), + radius=8, + fill=(213, 235, 246) if visible else (242, 244, 247), + outline=(54, 127, 169) if visible else (190, 196, 205), + width=2, ) - lines = ( - f"result: {summary.status.upper()}", - f"assignment: {assignment_text or 'not applicable'}", - f"encoding statistics: {len(summary.statistics)}", - "independent assignment checking is downstream", + variables = bundle.formula.clauses[clause_id] + draw.text((96, y + 38), f"c{clause_id}", font=explain_font(52), fill=EXPLAIN_TEXT_RGB if visible else EXPLAIN_MUTED_RGB) + for position, variable in enumerate(variables): + x = 230 + position * 170 + draw.rounded_rectangle((x, y + 24, x + 132, y + 104), radius=12, fill=EXPLAIN_PANEL_RGB, outline=(54, 127, 169), width=3) + draw.text((x + 36, y + 40), f"x{variable}", font=explain_font(48), fill=EXPLAIN_TEXT_RGB if visible else EXPLAIN_MUTED_RGB) + draw.line((820, y + 64, 994, y + 64), fill=(54, 127, 169), width=8) + draw.polygon(((994, y + 64), (964, y + 46), (964, y + 82)), fill=(54, 127, 169)) + draw.rounded_rectangle((1020, y, 1808, y + 128), radius=8, fill=(213, 235, 246) if visible else (242, 244, 247), outline=(54, 127, 169) if visible else (190, 196, 205), width=2) + draw.text((1050, y + 38), equation.replace(" + ", "+"), font=explain_font(48), fill=EXPLAIN_TEXT_RGB if visible else EXPLAIN_MUTED_RGB) + assignment = summary.assignment or () + assignment_items = tuple( + f"x{index}={'true' if value else 'false'}" + for index, value in enumerate(assignment) + ) + if len(assignment_items) <= 6: + assignment_text = ", ".join(assignment_items) + assignment_font = 48 + else: + assignment_text = ( + ", ".join(assignment_items[:3]) + + f" ... {len(assignment_items) - 5} omitted ... " + + ", ".join(assignment_items[-2:]) ) - y = 128 - for line in lines: - draw.text((566, y), line, font=explain_font(11), fill=EXPLAIN_TEXT_RGB) - y += 31 + assignment_font = 40 + draw.rounded_rectangle((320, 874, 1560, 950), radius=12, fill=(213, 237, 224) if stage == 3 else (242, 244, 247), outline=(53, 144, 93), width=3) + draw.text( + (352, 890), + f"copied {summary.status.upper()} model: {assignment_text or 'not applicable'}", + font=explain_font(assignment_font), + fill=EXPLAIN_TEXT_RGB if stage == 3 else EXPLAIN_MUTED_RGB, + ) draw.text( - (18, 408), - "Rendering explains declared construction order; it does not expose Z3 decisions.", - font=explain_font(9), + (36, 996), + "Each repeated clause position remains a separate If term; Z3 internal search decisions are not exposed.", + font=explain_font(32), fill=EXPLAIN_MUTED_RGB, ) return image @@ -484,6 +617,7 @@ def _compose_boolean_frame(summary: Z3EncodingSummary, stage: int) -> Image.Imag def render_boolean_z3_assets( summary_path: str | Path, + manifest_path: str | Path, output_directory: str | Path, *, duration_ms: int = 800, @@ -491,18 +625,21 @@ def render_boolean_z3_assets( summary = load_z3_encoding_summary(summary_path) if summary.engine != BOOLEAN_ENGINE: raise WangSquareRenderError("encoding animation requires a Boolean Z3 summary") - frames = tuple(_compose_boolean_frame(summary, stage) for stage in range(4)) + bundle = load_explainability_bundle(manifest_path) + _bind_oracle_inputs(summary, bundle) + frames = tuple(_compose_boolean_frame(summary, bundle, stage) for stage in range(4)) return write_animation_assets( frames, tuple(f"frame-{stage:02d}.png" for stage in range(4)), output_directory, - fallback_index=2, + fallback_index=3, duration_ms=duration_ms, ) def render_wang_z3_assets( summary_path: str | Path, + manifest_path: str | Path, output_directory: str | Path, *, duration_ms: int = 800, @@ -510,12 +647,14 @@ def render_wang_z3_assets( summary = load_z3_encoding_summary(summary_path) if summary.engine != WANG_ENGINE: raise WangSquareRenderError("encoding animation requires a Wang Z3 summary") - frames = tuple(_compose_wang_frame(summary, stage) for stage in range(5)) + bundle = load_explainability_bundle(manifest_path) + _bind_oracle_inputs(summary, bundle) + frames = tuple(_compose_wang_frame(summary, bundle, stage) for stage in range(5)) return write_animation_assets( frames, tuple(f"frame-{stage:02d}.png" for stage in range(5)), output_directory, - fallback_index=3, + fallback_index=4, duration_ms=duration_ms, ) @@ -525,6 +664,7 @@ def _parser() -> argparse.ArgumentParser: description="render a declared Boolean or Wang Z3 encoding order without Z3" ) parser.add_argument("summary", type=Path) + parser.add_argument("manifest", type=Path) parser.add_argument("output_directory", type=Path) parser.add_argument("--duration-ms", type=int, default=800) return parser @@ -541,7 +681,10 @@ def main(arguments: list[str] | None = None) -> int: else render_wang_z3_assets ) outputs = renderer( - args.summary, args.output_directory, duration_ms=args.duration_ms + args.summary, + args.manifest, + args.output_directory, + duration_ms=args.duration_ms, ) except (FileNotFoundError, WangSquareRenderError) as error: parser.error(str(error)) diff --git a/templates/run-report-v2.tex b/templates/run-report-v2.tex new file mode 100644 index 0000000..f3ab139 --- /dev/null +++ b/templates/run-report-v2.tex @@ -0,0 +1,32 @@ +\documentclass[10pt]{article} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage[a4paper,margin=18mm]{geometry} +\usepackage{array} +\usepackage{graphicx} +\usepackage{longtable} +\usepackage{url} +\usepackage{verbatim} + +\setlength{\parindent}{0pt} +\setlength{\parskip}{0.55em} +\setlength{\emergencystretch}{2em} + +\ifdefined\pdfinfoomitdate + \pdfinfoomitdate=1 +\fi +\ifdefined\pdftrailerid + \pdftrailerid{} +\fi +\ifdefined\pdfsuppressptexinfo + \pdfsuppressptexinfo=15 +\fi + +\title{@@TITLE@@} +\author{Tiling Foundry full-pipeline run dossier v2} +\date{} + +\begin{document} +\maketitle +@@BODY@@ +\end{document} diff --git a/tests/python/test_multi_engine_dossier.py b/tests/python/test_multi_engine_dossier.py index 286a5de..758a315 100644 --- a/tests/python/test_multi_engine_dossier.py +++ b/tests/python/test_multi_engine_dossier.py @@ -1,6 +1,7 @@ from __future__ import annotations import copy +from datetime import datetime, timezone import json import os from pathlib import Path @@ -14,8 +15,14 @@ from dossier import multi_engine from dossier import narrative_assets as narrative_generator +from dossier.tex_compile import TexCompileError, compile_tex_pdf from formats.pipeline_snapshot import PipelineSnapshotError -from formats.narrative_assets import load_narrative_assets +from formats.narrative_assets import ( + boolean_z3_source_sha256, + load_narrative_assets, + verification_source_sha256, + wang_z3_source_sha256, +) from formats.run_case_v2 import ( CASE_SCHEMA, load_run_case_v2, @@ -25,6 +32,7 @@ validate_run_dossier_v2, ) from formats.run_dossier_v2_bundle import load_run_dossier_v2 +from formats.run_report_v2_tex import _wide_figure, render_run_report_v2_tex from native import multi_engine_pipeline from native.multi_engine_pipeline import ( TraceCaptureOptions, @@ -37,6 +45,66 @@ ROOT = Path(__file__).resolve().parents[2] SAT_CASE = ROOT / "examples/run-cases-v2/pipeline-sat.json" UNSAT_CASE = ROOT / "examples/run-cases-v2/pipeline-unsat-search.json" +V2_TEMPLATE = ROOT / "templates/run-report-v2.tex" + + +class V2FigurePaginationTests(unittest.TestCase): + @unittest.skipUnless( + shutil.which("pdflatex") and shutil.which("pdftotext"), + "pdflatex and pdftotext are optional", + ) + def test_wide_figure_keeps_its_caption_on_the_image_page(self) -> None: + captured_at = datetime(2026, 1, 1, tzinfo=timezone.utc) + with tempfile.TemporaryDirectory() as name: + directory = Path(name) + picture = directory / "picture" + picture.mkdir() + (picture / "report.tex").write_text( + "\n".join( + ( + r"\documentclass{article}", + r"\usepackage[paperwidth=100mm,paperheight=20mm,margin=2mm]{geometry}", + r"\pagestyle{empty}", + r"\begin{document}IMAGE-MARKER\end{document}", + ) + ), + encoding="utf-8", + ) + compile_tex_pdf(picture, "pdflatex", captured_at) + shutil.copyfile(picture / "report.pdf", directory / "image.pdf") + (directory / "report.tex").write_text( + "\n".join( + ( + r"\documentclass{article}", + r"\usepackage[a4paper,margin=18mm]{geometry}", + r"\usepackage{graphicx}", + r"\setlength{\parindent}{0pt}", + r"\setlength{\parskip}{0.55em}", + r"\begin{document}", + r"\newlength{\imageheight}", + r"\settoheight{\imageheight}{\includegraphics[width=\textwidth,height=0.48\textheight,keepaspectratio]{image.pdf}}", + # Leave room for the image, but not its caption: both + # must move together when the page cannot hold them. + r"\vspace*{\dimexpr\textheight-\imageheight-42pt\relax}", + _wide_figure("image.pdf", "CAPTION-MARKER"), + r"\end{document}", + ) + ), + encoding="utf-8", + ) + compile_tex_pdf(directory, "pdflatex", captured_at) + pages = subprocess.run( + ["pdftotext", str(directory / "report.pdf"), "-"], + check=True, + capture_output=True, + text=True, + timeout=30, + ).stdout.split("\f") + image_pages = [i for i, page in enumerate(pages) if "IMAGE-MARKER" in page] + caption_pages = [i for i, page in enumerate(pages) if "CAPTION-MARKER" in page] + self.assertEqual(len(image_pages), 1) + self.assertEqual(len(caption_pages), 1) + self.assertEqual(image_pages, caption_pages) class MultiEngineDossierTests(unittest.TestCase): @@ -156,13 +224,216 @@ def test_sat_capture_binds_named_engines_and_shared_native_inputs(self) -> None: document, ) self.assertEqual(narrative["product"], "run-specific") + for solver in ("reference", "optimized"): + animation = narrative["animations"][f"{solver}_trace"] + self.assertEqual(animation["semantic_label"], "observed") + self.assertEqual(animation["scope"], { + "complete": True, "selected": True, "truncated": False, + }) self.assertEqual( narrative["animations"]["optimized_mechanisms"]["semantic_label"], "didactic", ) + expected_copy = { + "boolean_z3": ( + "Real source clauses become occurrence-preserving exactly-one sums " + "before the copied assignment is shown.", + "Four frames place each source-order clause beside its " + "occurrence-preserving sum and then show the copied Boolean assignment.", + ), + "wang_z3": ( + "A real cell shows its shared term, canonical tile tuple, boundary " + "equality, and returned model projection.", + "Five frames show adjacent canonical Wang tiles sharing an internal " + "edge, one exposed boundary equality, and the copied model projection.", + ), + "verification": ( + "Six named checker receipts with concrete tiling rules and the recorded " + "native extraction beside its source cells.", + "Six frames show all checker receipts, valid tile IDs, TILE_NONE, " + "internal and boundary equality, and copied extracted Boolean values " + "beside variable-gadget cells.", + ), + } + for name, (caption, alt_text) in expected_copy.items(): + self.assertEqual(narrative["animations"][name]["caption"], caption) + self.assertEqual(narrative["animations"][name]["alt_text"], alt_text) self.assertFalse((self.sat_directory / "report.tex").exists()) self.assertFalse((self.sat_directory / "report.pdf").exists()) + def test_v2_sat_report_follows_pipeline_and_uses_static_milestones(self) -> None: + narrative = load_narrative_assets( + self.sat_directory / "assets/narrative/manifest.json", + self.sat_document, + ) + tex = render_run_report_v2_tex( + self.sat_document, + narrative, + V2_TEMPLATE.read_text(encoding="utf-8"), + ) + headings = ( + r"\section{Summary}", + r"\section{Source instance}", + r"\section{Boolean Z3}", + r"\section{Yang--Zhang reduction}", + r"\section{Reference solver}", + r"\section{Optimized solver}", + r"\section{Wang Z3}", + r"\section{Verification and presentation}", + r"\section{Reproducibility appendix}", + ) + offsets = tuple(tex.index(heading) for heading in headings) + self.assertEqual(offsets, tuple(sorted(offsets))) + self.assertIn( + r"\verbatiminput{assets/data/pipeline_sat.cm13}", + tex, + ) + for group in ( + "region_construction", + "reference_trace", + "optimized_trace", + ): + for path in narrative["pdf_milestones"][group]: + self.assertIn(path, tex) + self.assertNotIn("contact-sheet.png", tex) + self.assertNotIn(".gif", tex) + for name in ("square", "generalized", "hex"): + path = narrative["statics"][f"{name}_presentation"]["artifact"]["path"] + self.assertIn( + r"\includegraphics[width=\textwidth,height=0.48\textheight,keepaspectratio]" + rf"{{assets/narrative/{path}}}", + tex, + ) + sheet_path = narrative["statics"]["generalized_sheet"]["artifact"]["path"] + self.assertIn( + r"\includegraphics[width=0.82\textwidth,height=0.64\textheight,keepaspectratio]" + rf"{{assets/narrative/{sheet_path}}}", + tex, + ) + legend_path = narrative["statics"]["atomic_legend"]["artifact"]["path"] + self.assertEqual(tex.count(f"{{assets/narrative/{legend_path}}}"), 2) + self.assertIn("viewport=0 2092 1732 4184,clip,width=0.92", tex) + self.assertIn("viewport=0 0 1732 2092,clip,width=0.92", tex) + + def test_v2_unsat_report_marks_witness_only_content_not_applicable(self) -> None: + narrative = load_narrative_assets( + self.unsat_directory / "assets/narrative/manifest.json", + self.unsat_document, + ) + tex = render_run_report_v2_tex( + self.unsat_document, + narrative, + V2_TEMPLATE.read_text(encoding="utf-8"), + ) + self.assertIn("Assignment: not applicable for this UNSAT result", tex) + self.assertIn("Witness verification: not applicable", tex) + self.assertIn("Witness presentations: not applicable", tex) + self.assertIn("No UNSAT certificate is claimed", tex) + self.assertIn( + narrative["statics"]["presentation_status"]["artifact"]["path"], + tex, + ) + presentation_status = narrative["statics"]["presentation_status"] + status_path = presentation_status["artifact"]["path"] + self.assertIn( + r"\includegraphics[width=0.72\textwidth,height=0.30\textheight,keepaspectratio]" + rf"{{assets/narrative/{status_path}}}", + tex, + ) + self.assertNotIn("contact-sheet.png", tex) + self.assertNotIn(".gif", tex) + for name in ( + "home_preview", + "worked_example", + "square_presentation", + "generalized_presentation", + "hex_presentation", + ): + self.assertIsNone(narrative["statics"][name]) + + def test_v2_formatter_is_pure_after_caller_validation(self) -> None: + narrative = load_narrative_assets( + self.sat_directory / "assets/narrative/manifest.json", + self.sat_document, + ) + with patch("builtins.open", side_effect=AssertionError("formatter I/O")), patch( + "io.open", side_effect=AssertionError("formatter I/O") + ): + tex = render_run_report_v2_tex( + self.sat_document, + narrative, + "@@TITLE@@\n@@BODY@@\n", + ) + self.assertIn(r"\section{Summary}", tex) + + def test_v2_reports_each_oracle_timing_in_its_own_section(self) -> None: + for directory, document in ( + (self.sat_directory, self.sat_document), + (self.unsat_directory, self.unsat_document), + ): + with self.subTest(status=document["case"]["expected_status"]): + narrative = load_narrative_assets( + directory / "assets/narrative/manifest.json", document + ) + tex = render_run_report_v2_tex( + document, narrative, V2_TEMPLATE.read_text(encoding="utf-8") + ) + appendix = tex.split( + r"\section{Reproducibility appendix}", 1 + )[1] + for heading, timing_name in ( + ("Boolean Z3", "boolean_z3_ns"), + ("Wang Z3", "wang_z3_ns"), + ): + elapsed_ns = document["timings"][timing_name] + expected = ( + f"{elapsed_ns / 1_000_000:.3f} ms ({elapsed_ns} ns)" + ) + section = tex.split(rf"\section{{{heading}}}", 1)[1].split( + r"\section{", 1 + )[0] + self.assertIn(expected, section) + self.assertIn("run-specific", section.lower()) + self.assertIn("not a benchmark", section.lower()) + self.assertIn(expected, appendix) + + def test_narrative_source_hashes_cover_every_consumed_identity(self) -> None: + run = self.sat_document + verification_digest = verification_source_sha256(run) + for path, replacement in ( + (("source", "sha256"), "0" * 64), + (("reduction", "formula_sha256"), "1" * 64), + (("reduction", "tileset_sha256"), "2" * 64), + (("reduction", "region_sha256"), "3" * 64), + (("reduction", "provenance_sha256"), "4" * 64), + (("reference", "solution_sha256"), "5" * 64), + (("reference", "extracted_assignment"), [True, False, True]), + ): + mutated = copy.deepcopy(run) + mutated[path[0]][path[1]] = replacement + self.assertNotEqual( + verification_source_sha256(mutated), + verification_digest, + path, + ) + + boolean_digest = boolean_z3_source_sha256("a" * 64, "b" * 64) + self.assertNotEqual( + boolean_z3_source_sha256("c" * 64, "b" * 64), + boolean_digest, + ) + self.assertNotEqual( + boolean_z3_source_sha256("a" * 64, "c" * 64), + boolean_digest, + ) + wang_digest = wang_z3_source_sha256("a" * 64, "b" * 64, "c" * 64) + for values in ( + ("d" * 64, "b" * 64, "c" * 64), + ("a" * 64, "d" * 64, "c" * 64), + ("a" * 64, "b" * 64, "d" * 64), + ): + self.assertNotEqual(wang_z3_source_sha256(*values), wang_digest) + def test_unsat_capture_has_no_witness_or_fabricated_verification(self) -> None: document = self.unsat_document self.assertEqual( @@ -193,6 +464,36 @@ def test_unsat_capture_has_no_witness_or_fabricated_verification(self) -> None: self.assertIsNone(narrative["animations"]["witness_presentation"]) self.assertIsNotNone(narrative["statics"]["presentation_status"]) self.assertIsNone(narrative["statics"]["home_preview"]) + self.assertEqual( + narrative["animations"]["boolean_z3"]["caption"], + "Source clauses retain occurrence-preserving exactly-one sums; " + "the assignment is not applicable for this UNSAT result.", + ) + self.assertEqual( + narrative["animations"]["boolean_z3"]["alt_text"], + "Four frames show source-order clauses and sums, then mark the " + "Boolean assignment not applicable because no SAT model was returned.", + ) + self.assertEqual( + narrative["animations"]["wang_z3"]["caption"], + "The encoding is constructed, but cell, tile, boundary, and returned-model " + "examples are not applicable for this UNSAT result.", + ) + self.assertEqual( + narrative["animations"]["wang_z3"]["alt_text"], + "Five frames end with an UNSAT panel that makes no cell, tile tuple, " + "boundary, model, witness, or certificate claim.", + ) + self.assertEqual( + narrative["animations"]["verification"]["caption"], + "Six named checker receipts mark every witness check not applicable " + "because no SAT witness was returned.", + ) + self.assertEqual( + narrative["animations"]["verification"]["alt_text"], + "Six frames mark every witness check not applicable and state that " + "no SAT witness or certificate is fabricated.", + ) for solver, animation_name in ( ("reference", "reference_trace"), ("optimized", "optimized_trace"), @@ -216,6 +517,34 @@ def test_unsat_capture_has_no_witness_or_fabricated_verification(self) -> None: {"conflict", "backtrack", "result"} <= selected_kinds, (solver, selected_kinds), ) + animation = narrative["animations"][animation_name] + self.assertIn("observed search diagnostic", animation["caption"]) + self.assertIn("not an UNSAT certificate", animation["caption"]) + selected = [ + event for event in trace["events"] + if event["sequence"] in selected_sequences + ] + decision = next(e for e in selected if e["kind"] == "decision") + reduction = next(e for e in selected if ( + e["kind"] == "domain_reduction" and e["reason"] == "propagation" + and e["sequence"] > decision["sequence"] + )) + empty = next(e for e in selected if ( + e["kind"] == "domain_reduction" and e["new_domain"] == 0 + and e["sequence"] >= reduction["sequence"] + )) + conflict = next(e for e in selected if e["kind"] == "conflict") + rollback = next(e for e in selected if e["kind"] == "backtrack") + next_branches = [e for e in selected if ( + e["kind"] == "decision" and e["sequence"] > rollback["sequence"] + )] + self.assertTrue(next_branches, f"{solver} omits the next branch") + next_branch = next_branches[0] + self.assertLess(decision["sequence"], reduction["sequence"]) + self.assertLess(empty["sequence"], conflict["sequence"]) + self.assertLess(conflict["sequence"], rollback["sequence"]) + self.assertLess(rollback["sequence"], next_branch["sequence"]) + self.assertLess(rollback["change_mark"], conflict["change_mark"]) def test_case_contract_forbids_initial_domain_overrides(self) -> None: invalid = json.loads(SAT_CASE.read_text(encoding="utf-8")) @@ -269,7 +598,17 @@ def test_public_generator_dispatch_preserves_the_v1_implementation(self) -> None tex_engine="pdflatex", ) self.assertEqual(v2_actual, v2_expected) - generate_v2.assert_called_once_with(SAT_CASE, v2_expected) + generate_v2.assert_called_once_with(SAT_CASE, v2_expected, include_pdf=False) + with self.assertRaisesRegex( + public_generator.DossierGenerationError, + "v2-only", + ): + public_generator.generate_run_dossier( + v1_case, + expected, + tex_engine="pdflatex", + include_pdf=True, + ) with self.assertRaisesRegex( public_generator.DossierGenerationError, "v1-only", @@ -337,6 +676,24 @@ def test_bundle_loader_imports_no_capture_or_native_producer(self) -> None: ) self.assertEqual(completed.returncode, 0, completed.stderr) + completed = subprocess.run( + [ + sys.executable, + "-c", + ( + "import sys; import dossier.multi_engine; " + "assert 'formats.run_report_v2_tex' not in sys.modules; " + "assert 'dossier.tex_compile' not in sys.modules" + ), + ], + cwd=ROOT, + env={**os.environ, "PYTHONPATH": "python"}, + check=False, + capture_output=True, + text=True, + ) + self.assertEqual(completed.returncode, 0, completed.stderr) + def test_same_compositor_bytes_serve_run_and_canonical_pages(self) -> None: destination = self.root / "canonical-pages-assets" manifest_path = narrative_generator.generate_narrative_assets( @@ -620,6 +977,25 @@ def test_final_replace_failure_leaves_no_partial_destination(self) -> None: self.assertFalse(destination.exists()) self.assertEqual(set(self.root.glob(".replace-failed.*")), before) + def test_v2_pdf_compile_failure_leaves_no_partial_destination(self) -> None: + destination = self.root / "pdf-compile-failed" + before = set(self.root.glob(".pdf-compile-failed.*")) + with patch( + "dossier.tex_compile.compile_tex_pdf", + side_effect=TexCompileError("forced controlled compile failure"), + ): + with self.assertRaisesRegex( + multi_engine.MultiEngineDossierError, + "forced controlled compile failure", + ): + multi_engine.generate_multi_engine_dossier( + SAT_CASE, + destination, + include_pdf=True, + ) + self.assertFalse(destination.exists()) + self.assertEqual(set(self.root.glob(".pdf-compile-failed.*")), before) + def test_v2_schemas_are_closed_draft_2020_12_documents(self) -> None: for name, expected in ( ("wang-run-case-v2.schema.json", CASE_SCHEMA), diff --git a/tests/python/test_pages_checker.py b/tests/python/test_pages_checker.py index 25e1901..9cebc8f 100644 --- a/tests/python/test_pages_checker.py +++ b/tests/python/test_pages_checker.py @@ -167,10 +167,10 @@ def swapped_roles(path: Path, errors: list[str]) -> tuple[dict[str, str], str]: if path == target: body = body.replace( 'animation="/assets/narrative/boolean-z3/trace.gif" ' - 'fallback="/assets/narrative/boolean-z3/frame-02.png" ' + 'fallback="/assets/narrative/boolean-z3/frame-03.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" ' + 'fallback="/assets/narrative/boolean-z3/frame-03.png" ' 'contact_sheet="/assets/narrative/boolean-z3/trace.gif"', ) return metadata, body diff --git a/tests/python/test_run_dossier.py b/tests/python/test_run_dossier.py index b7a536a..1ff0493 100644 --- a/tests/python/test_run_dossier.py +++ b/tests/python/test_run_dossier.py @@ -2,11 +2,15 @@ import copy from dataclasses import replace +from datetime import datetime, timezone import hashlib import json from pathlib import Path +import shutil +import subprocess import tempfile import unittest +from unittest.mock import patch from formats.pipeline_snapshot import PipelineSnapshotError from formats.run_dossier import ( @@ -18,6 +22,8 @@ validate_run_dossier, ) from formats.run_report_tex import render_run_report_tex +from dossier.tex_compile import TexCompileError, compile_tex_pdf +from tools import generate_run_dossier as public_generator from native.trace_pipeline import capture_native_pipeline_trace @@ -49,6 +55,157 @@ def _artifacts() -> dict[str, dict[str, str]]: class RunDossierTests(unittest.TestCase): + def test_shared_tex_compiler_translates_private_home_setup_failure(self) -> None: + with tempfile.TemporaryDirectory() as directory, patch( + "dossier.tex_compile.shutil.which", + return_value="/usr/bin/pdflatex", + ), patch( + "dossier.tex_compile.Path.mkdir", + side_effect=OSError("setup denied"), + ): + with self.assertRaisesRegex(TexCompileError, "setup denied"): + compile_tex_pdf( + Path(directory), + "pdflatex", + datetime(2026, 8, 27, tzinfo=timezone.utc), + ) + + def test_shared_tex_compiler_does_not_remove_preexisting_private_home(self) -> None: + with tempfile.TemporaryDirectory() as directory, patch( + "dossier.tex_compile.shutil.which", + return_value="/usr/bin/pdflatex", + ): + dossier = Path(directory) + tex_home = dossier / ".tex-home" + tex_home.mkdir() + sentinel = tex_home / "caller-owned" + sentinel.write_text("preserve", encoding="utf-8") + + with self.assertRaises(TexCompileError): + compile_tex_pdf( + dossier, + "pdflatex", + datetime(2026, 8, 27, tzinfo=timezone.utc), + ) + + self.assertEqual(sentinel.read_text(encoding="utf-8"), "preserve") + + def test_shared_tex_compiler_translates_cleanup_failure_after_success(self) -> None: + with tempfile.TemporaryDirectory() as directory, patch( + "dossier.tex_compile.shutil.which", + return_value="/usr/bin/pdflatex", + ), patch( + "dossier.tex_compile.subprocess.run", + ), patch( + "dossier.tex_compile.shutil.rmtree", + side_effect=OSError("cleanup denied"), + ): + dossier = Path(directory) + (dossier / "report.pdf").write_bytes(b"%PDF-" + b"0" * 100) + + with self.assertRaisesRegex(TexCompileError, "cleanup denied"): + compile_tex_pdf( + dossier, + "pdflatex", + datetime(2026, 8, 27, tzinfo=timezone.utc), + ) + + def test_shared_tex_compiler_reports_cleanup_failure_inside_caller_except(self) -> None: + with tempfile.TemporaryDirectory() as directory, patch( + "dossier.tex_compile.shutil.which", + return_value="/usr/bin/pdflatex", + ), patch( + "dossier.tex_compile.subprocess.run", + ), patch( + "dossier.tex_compile.shutil.rmtree", + side_effect=OSError("cleanup denied in caller except"), + ): + dossier = Path(directory) + (dossier / "report.pdf").write_bytes(b"%PDF-" + b"0" * 100) + + try: + raise ValueError("unrelated caller error") + except ValueError: + with self.assertRaisesRegex( + TexCompileError, + "cleanup denied in caller except", + ): + compile_tex_pdf( + dossier, + "pdflatex", + datetime(2026, 8, 27, tzinfo=timezone.utc), + ) + + def test_shared_tex_compiler_keeps_primary_error_when_cleanup_also_fails(self) -> None: + primary = TexCompileError("primary compile failure") + with tempfile.TemporaryDirectory() as directory, patch( + "dossier.tex_compile.shutil.which", + return_value="/usr/bin/pdflatex", + ), patch( + "dossier.tex_compile.subprocess.run", + side_effect=primary, + ), patch( + "dossier.tex_compile.shutil.rmtree", + side_effect=OSError("secondary cleanup failure"), + ) as remove_private_home: + with self.assertRaises(TexCompileError) as raised: + compile_tex_pdf( + Path(directory), + "pdflatex", + datetime(2026, 8, 27, tzinfo=timezone.utc), + ) + + self.assertIs(raised.exception, primary) + remove_private_home.assert_called_once() + + @unittest.skipUnless(shutil.which("pdflatex"), "pdflatex is optional") + def test_shared_tex_compiler_is_deterministic_and_rejects_shell_escape(self) -> None: + captured_at = datetime(2026, 8, 27, 20, 0, 0, tzinfo=timezone.utc) + source = (ROOT / "templates/run-report.tex").read_text(encoding="utf-8") + source = source.replace("@@TITLE@@", "Compile boundary test").replace( + "@@BODY@@", "Deterministic body." + ) + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + outputs: list[bytes] = [] + for name in ("one", "two"): + dossier = root / name + dossier.mkdir() + (dossier / "report.tex").write_text(source, encoding="utf-8") + commands: list[list[str]] = [] + actual_run = subprocess.run + + def checked_run(command: list[str], **kwargs: object) -> object: + commands.append(command) + return actual_run(command, **kwargs) + + with patch("dossier.tex_compile.subprocess.run", side_effect=checked_run): + compile_tex_pdf(dossier, "pdflatex", captured_at) + self.assertEqual(len(commands), 2) + self.assertTrue(all("-no-shell-escape" in command for command in commands)) + self.assertFalse((dossier / ".tex-home").exists()) + self.assertEqual( + sorted(path.name for path in dossier.iterdir()), + ["report.pdf", "report.tex"], + ) + outputs.append((dossier / "report.pdf").read_bytes()) + self.assertEqual(outputs[0], outputs[1]) + + def test_v1_caller_translates_the_shared_compile_error(self) -> None: + with patch( + "tools.generate_run_dossier.compile_tex_pdf", + side_effect=TexCompileError("controlled failure"), + ): + with self.assertRaisesRegex( + public_generator.DossierGenerationError, + "controlled failure", + ): + public_generator._compile_pdf( + Path("unused"), + "pdflatex", + datetime(2026, 8, 27, tzinfo=timezone.utc), + ) + def test_versioned_cases_match_distinct_complete_observed_runs(self) -> None: summaries: dict[str, tuple[str, int, int]] = {} for case_path in sorted(CASES.glob("*.json")): diff --git a/tools/generate_run_dossier.py b/tools/generate_run_dossier.py index 9a9dddf..691a895 100644 --- a/tools/generate_run_dossier.py +++ b/tools/generate_run_dossier.py @@ -4,7 +4,6 @@ from __future__ import annotations import argparse -import calendar from datetime import datetime, timezone import hashlib import os @@ -35,6 +34,7 @@ validate_case_outcome, ) from formats.run_report_tex import render_run_report_tex # noqa: E402 +from dossier.tex_compile import TexCompileError, compile_tex_pdf # noqa: E402 from formats.solver_trace_snapshot import ( # noqa: E402 dump_solver_trace_bundle, load_solver_trace_bundle, @@ -62,6 +62,11 @@ def _parser() -> argparse.ArgumentParser: ) parser.add_argument("--max-frames", type=int, default=12, help="v1 only") parser.add_argument("--duration-ms", type=int, default=500, help="v1 only") + parser.add_argument( + "--pdf", + action="store_true", + help="compile the additive static PDF for v2 cases only", + ) return parser @@ -272,66 +277,10 @@ def _git_commit() -> str: def _compile_pdf(dossier_root: Path, tex_engine: str, captured_at: datetime) -> None: - executable = shutil.which(tex_engine) - if executable is None: - raise DossierGenerationError(f"TeX engine not found: {tex_engine}") - tex_home = dossier_root / ".tex-home" - tex_home.mkdir() - tex_var = tex_home / "var" - tex_config = tex_home / "config" - tex_fonts = tex_var / "fonts" - tex_var.mkdir() - tex_config.mkdir() - tex_fonts.mkdir() - environment = { - "PATH": os.environ.get("PATH", "/usr/bin:/bin"), - "HOME": str(tex_home), - "TEXMFHOME": str(tex_home / "texmf"), - "TEXMFVAR": str(tex_var), - "TEXMFCONFIG": str(tex_config), - "VARTEXFONTS": str(tex_fonts), - "SOURCE_DATE_EPOCH": str(calendar.timegm(captured_at.utctimetuple())), - "TZ": "UTC", - "openin_any": "p", - "openout_any": "p", - } - command = [ - executable, - "-interaction=nonstopmode", - "-halt-on-error", - "-file-line-error", - "-no-shell-escape", - "report.tex", - ] - for _ in range(2): - try: - subprocess.run( - command, - cwd=dossier_root, - env=environment, - check=True, - capture_output=True, - text=True, - timeout=120, - ) - except (OSError, subprocess.SubprocessError) as error: - detail = getattr(error, "stdout", "") or getattr(error, "stderr", "") - raise DossierGenerationError( - f"LaTeX compilation failed without shell escape: {detail.strip()}" - ) from error - pdf = dossier_root / "report.pdf" try: - if pdf.stat().st_size < 100 or not pdf.read_bytes().startswith(b"%PDF-"): - raise DossierGenerationError("TeX engine did not produce a valid PDF header") - except OSError as error: - raise DossierGenerationError(f"cannot inspect report.pdf: {error}") from error - for suffix in ("aux", "log", "out", "toc"): - auxiliary = dossier_root / f"report.{suffix}" - try: - auxiliary.unlink() - except FileNotFoundError: - pass - shutil.rmtree(tex_home) + compile_tex_pdf(dossier_root, tex_engine, captured_at) + except TexCompileError as error: + raise DossierGenerationError(str(error)) from error def _generate_run_dossier_v1( @@ -448,10 +397,13 @@ def generate_run_dossier( tex_engine: str, max_frames: int = 12, duration_ms: int = 500, + include_pdf: bool = False, ) -> Path: """Dispatch the sole public CLI without sharing v1/v2 implementations.""" schema = _case_schema(case_path) if schema == "wang-run-case-v1": + if include_pdf: + raise DossierGenerationError("--pdf is a v2-only option") return _generate_run_dossier_v1( case_path, output_directory, @@ -470,7 +422,11 @@ def generate_run_dossier( ) try: - return generate_multi_engine_dossier(case_path, output_directory) + return generate_multi_engine_dossier( + case_path, + output_directory, + include_pdf=include_pdf, + ) except MultiEngineDossierError as error: raise DossierGenerationError(str(error)) from error raise DossierGenerationError(f"unsupported dossier case schema: {schema}") @@ -486,6 +442,7 @@ def main(arguments: list[str] | None = None) -> int: tex_engine=args.tex_engine, max_frames=args.max_frames, duration_ms=args.duration_ms, + include_pdf=args.pdf, ) except (DossierGenerationError, OSError, ValueError) as error: parser.error(str(error))