Add deterministic solver trace replay

[xtraid]

Summary

• add bounded, opt-in, caller-owned semantic traces to the reference and optimized native solvers, with full initial state, ordered deltas, bounded checkpoints, terminal result, transactional cleanup, and closed hash-bound snapshot contracts
• add one isolated Z3-free offline replay/composition path for deterministic PNG frames, contact sheets, and presentation-only GIFs, plus canonical/didactic algorithm assets embedded in their technical Pages documents with accessible fallbacks
• fix Z3 seed/thread configuration and publish explicit project-owned Boolean/Wang encoding-order summaries without claiming an internal Z3 search trace
• add strict cross-artifact validation and rejection coverage for region activity, event fields, truncation/checkpoints, tile IDs, models, and project-owned statistics

Validation

• make check: 140 Python tests and all 17 C test binaries
• renderer: 253/253 tests
• strict GCC and Clang builds
• ASan/UBSan/LSan, static analyzer, Memcheck, and Cachegrind
• Pages checker: 25 technical documents plus the index; real Jekyll build remains CI-only
• JSON parsing, git diff --check, secret scan, and artifact cleanup
• two review passes with all findings corrected

Trace-disabled profile note

The ordinary solver path preserves solve results, ownership, and public metrics exactly and performs no trace allocation. A controlled Cachegrind smoke comparison measured +0.70% retired instructions for reference and +0.49% for optimized because the shared core still executes disabled trace branches, so this PR deliberately makes no zero-overhead or byte-identical-profile claim.