Persist and replay solver deductions, decisions, and metrics (SLM-64)

docs/design/meta-model-traces.md

@@ -22,6 +22,24 @@ telemetry), and — for decode rows — policy checkpoint SHA, decode-config
 hash (`decode_config_hash`), tokenizer/grammar versions, and seed. Rollouts
 from different checkpoints are never mixed unlabeled.
 
+### Solver-transition events (VSS1-04 / SLM-64)
+
+When the verified solver runs during decode (`verified_solver_decode`, default
+off), each decision emits typed events into the same decode row's `events`
+list — `solver_state`, `support_result`, `certified_deduction`, `decision`,
+`backtrack`, `nogood`, `solver_terminal` — built by
+[`dsl/solver/replay.py`](../../src/slm_training/dsl/solver/replay.py). Exact-closure
+decode emits the `solver_state` / `support_result` / `certified_deduction` /
+`solver_terminal` subset; the reversible search controller additionally emits
+`decision` / `backtrack` / `nogood`. The row also carries a bounded `solver`
+sidecar — `{schema_version, certificate_mode, certificates, counters}` — where
+`certificate_mode` (`none`/`summary`/`full`) gates certificate detail: `none`
+keeps only counters + honest status, `summary` compact descriptors, `full` the
+replay material (each certificate's `to_dict()`, whose recomputed digest must
+equal its id). Events and certificates carry only token/path ids and SHA-256
+digests — never raw region/user text. The schema bumps the decode trace to
+`version = 3`; v1/v2 rows load and replay unchanged.
+
 ## Replayability
 
 `replay_violations(trace)` certifies the decode stream is self-consistent:
@@ -31,6 +49,19 @@ trace with steps must carry a final canvas. Empty list = replayable; the
 fixture test proves both directions (a clean fixture decode passes, a
 corrupted canvas is caught).
 
+For solver-transition events it additionally invokes
+`solver_replay_violations` ([`dsl/solver/replay.py`](../../src/slm_training/dsl/solver/replay.py)),
+which checks the ten VSS1-04 invariants: fingerprint lineage (each transition's
+`before_fingerprint` matches the active replay state), certified deductions
+remove only live values and — in `full` mode — cite a present, digest-consistent
+certificate (tamper detection), `unknown` support never removes, decisions select
+exactly one live value and record the rest, backtracks restore a recorded
+state/level, a `nogood` is never a certified deduction, a `solved` terminal
+carries a verifier report, `certified_unsat` is impossible once any
+`unknown`/budget/truncation appears, event counts match the sidecar counters, and
+a truncated snapshot is reported non-replayable rather than accepted as an
+exhaustive proof. Violations are human-readable strings, never assertions.
+
 ## Retention and bucket layout
 
 Local stores live where run evidence already lives

docs/design/telemetry.md

@@ -41,6 +41,32 @@ the remote endpoint is missing or unavailable.
 **Generate:** `generate_batch` → `generate_once` / `best_of_n_rank`, plus
 `context_encode` inside the model.
 
+## Decode-stats solver work metrics (VSS1-04 / SLM-64)
+
+The verified solver's per-decode work is measured on the existing
+[`DecodeStats`](../../src/slm_training/models/decode_stats.py) envelope (not a new
+owner). All fields default to zero on every historical/default path (solver
+disabled), and solver wall time is separated from `denoiser_ms` / `projection_ms`.
+Stable names:
+
+| Field | Meaning |
+| --- | --- |
+| `solver_ms` | Solver wall time (`timed_ms`), separate from denoiser/projection. |
+| `solver_enabled` | `1` when the solver ran on a decision, else `0`. |
+| `solver_closure_passes` | Exact-closure fixed-point passes. |
+| `solver_support_queries` / `solver_support_cache_hits` | Support-oracle queries and request-local cache hits. |
+| `solver_supported` / `solver_unsupported` / `solver_unknown` | Tri-state support verdict counts. |
+| `solver_certified_removed` | Candidates removed by replay-valid certificates. |
+| `solver_decisions` / `solver_backtracks` / `solver_nogoods` | Reversible-search work (controller path). |
+| `solver_expanded_nodes` / `solver_verifier_calls` | Enumeration nodes and verifier calls. |
+| `solver_certificate_replay_failures` | Certificate replays that failed (0 at decode — closure never removes on a failed replay; populated by offline trace audits). |
+| `solver_terminal_status` | Honest terminal: `unknown` / `certified_unsat` / `budget_exhausted` (closure never claims `solved`). |
+
+They surface **only** under `metrics["decode_stats"]` in `eval_<suite>.json` (and,
+transitively, `scoreboard.json`) via `aggregate_stats`; no new top-level metric
+keys or files. They do not overload the existing grammar/lattice candidate
+counters.
+
 ## How to use
 
 ```bash

docs/design/verified-scope-solver.md

@@ -349,6 +349,40 @@ removal/keep/bottom/coverage semantics are pinned Torch-free by
 or experiment ran; the enabled path is unmeasured and this makes no correctness,
 readiness, speed, or ship claim.**
 
+## Implemented trace + replay (VSS1-04 / SLM-64)
+
+[`dsl/solver/replay.py`](../../src/slm_training/dsl/solver/replay.py) turns the
+solver artifacts into typed, replayable events recorded inside the existing
+decode trace (`DecodeTraceRecorder.events`, schema bumped to `version = 3`), and
+`solver_replay_violations` validates them. Event kinds: `solver_state`,
+`support_result`, `certified_deduction`, `decision`, `backtrack`, `nogood`,
+`solver_terminal`. Exact-closure decode (`models/twotower.py`
+`_record_solver_metrics`, gated on an attached recorder) emits the closure subset;
+the reversible controller additionally emits decisions/backtracks/nogoods. A
+bounded `solver` sidecar carries `{schema_version, certificate_mode, certificates,
+counters}`; `solver_certificate_mode` gates certificate detail (`none` counters +
+honest status only, `summary` compact descriptors, `full` replay material). Only
+token/path ids and SHA-256 digests are stored — never raw region/user text.
+
+The replay validator (invoked by `harnesses/distill/trace_store.py`
+`replay_violations`) checks ten invariants: fingerprint lineage; certified
+deductions remove only live values and — in `full` mode — cite a present,
+digest-consistent certificate (tamper detection, using the same canonical-JSON
+digest as `SupportCertificate.digest`); `unknown` never removes; decisions select
+one live value and record the rest; backtracks restore a recorded state/level;
+a `nogood` is never a certified deduction; a `solved` terminal carries a verifier
+report; `certified_unsat` is impossible once any `unknown`/budget/truncation
+appears; event counts match the sidecar counters; truncated snapshots are
+reported non-replayable. Solver work metrics (`solver_ms` separated from
+denoiser/projection, plus tri-state and certified-removal counters) ride the
+existing `DecodeStats` → `metrics["decode_stats"]` envelope, zero on the default
+path. Closure never reports `solved` (it prunes; it does not materialize a
+verifier-accepted terminal). Pinned by `tests/test_dsl/test_solver_replay.py`
+(validator + closure round-trip + tamper) and
+`tests/test_harnesses/distill/test_solver_trace.py` (recorder capture, clean
+replay, counters, historical compat). **No train/eval/benchmark/checkpoint ran;
+this makes no solver-quality, correctness, speed, or ship claim.**
+
 ## Reference support semantics
 
 | Verdict | Requirement | Removal permitted? |

docs/design/vss1-04-solver-trace-replay-20260718.md

@@ -0,0 +1,65 @@
+# VSS1-04 solver trace + replay — fixture evidence (2026-07-18)
+
+Fixture-grade wiring evidence for SLM-64 (VSS1-04): making certified-solver
+transitions replayable and measured on the **existing** decode trace + telemetry
+owners. No second trace store, no new output root, no custom binary format.
+
+## What was implemented
+
+- [`dsl/solver/replay.py`](../../src/slm_training/dsl/solver/replay.py) — Torch-free
+  typed event builders (`solver_state`, `support_result`, `certified_deduction`,
+  `decision`, `backtrack`, `nogood`, `solver_terminal`), mode-gated certificate
+  serialization (`none` / `summary` / `full`), and `solver_replay_violations`
+  (ten invariants, human-readable strings).
+- [`harnesses/distill/trace_store.py`](../../src/slm_training/harnesses/distill/trace_store.py)
+  — decode trace **schema `version = 3`** (backward-compatible v1/v2 readers),
+  `DecodeTraceRecorder.record_solver` sidecar, and `replay_violations` extended to
+  run the solver invariants on any solver events present.
+- [`models/decode_stats.py`](../../src/slm_training/models/decode_stats.py) — solver
+  work-metric counters + `solver_ms` (separated from denoiser/projection), zero on
+  the default path, surfaced only under `metrics["decode_stats"]` via
+  `aggregate_stats`.
+- [`models/twotower.py`](../../src/slm_training/models/twotower.py)
+  `_record_solver_metrics` — folds closure counters into `DecodeStats` and, when a
+  `DecodeTraceRecorder` is attached, emits the closure-subset events + a bounded
+  certificate/counter sidecar. No-op when neither stats nor a recorder is active.
+
+## Schema version
+
+- Decode trace: `TRACE_VERSION = 3` (was 2). v1/v2 rows load and replay unchanged.
+- Solver event stream: `SOLVER_TRACE_SCHEMA_VERSION = 1`.
+- Certificate schema: `CERTIFICATE_SCHEMA_VERSION = 1` (unchanged; VSS0-04).
+
+## Privacy / boundedness
+
+Events and certificates carry only token/path ids and SHA-256 digests — never raw
+region/user text (the terminal verifier-report summarizer drops non-allowlisted
+strings). The `solver_state` domain snapshot is bounded; a truncated snapshot sets
+`trace_truncated=true` and the validator reports the trace non-replayable rather
+than accepting bounded evidence as an exhaustive proof.
+
+## Test command
+
+```bash
+python -m pytest \
+  tests/test_dsl/test_solver_replay.py \
+  tests/test_harnesses/distill/test_solver_trace.py \
+  tests/test_models/test_decode_stats.py \
+  tests/test_models/test_trace_store.py \
+  tests/test_harnesses/distill/test_meta_traces.py -q
+python -m scripts.repo_policy
+```
+
+Result: solver-replay + trace + decode-stats + historical-compat suites pass;
+`repo_policy` ok. (The issue's suggested `tests/test_runtime` path does not hold
+trace tests — the runtime-trace tests are `tests/test_runtime_trace.py`; the
+decode-trace/replay tests are the paths above.)
+
+## Honesty
+
+Fixture-grade wiring only: the event schema, the ten replay invariants (including
+`full`-mode certificate tamper detection), the decode-stats counters, and
+historical-trace compatibility are tested on tiny closed fixtures. No model,
+checkpoint, training corpus, or eval run is produced or claimed. Closure never
+reports `solved`. **No solver-quality, correctness, speed, or ship claim is
+made.**