Integrate exact closure into compiler decode behind a flag (SLM-63)

docs/MODEL_CARD.md

@@ -137,6 +137,7 @@ scratch-matrix clears as production readiness; silent gold-placeholder channels.
 | Output tokenizer | Compositional `OpenUITokenizer` (default) or V5 lexer (`DSLNativeTokenizer`) |
 | Decode | Grammar-constrained LTR / MaskGIT + repair levers (see design docs) |
 | Topology experiment | `grammar_diffusion` v2: typed production-tree expansion/contraction with bounded active nodes; no fixed canvas |
+| Verified-solver decode | `verified_solver_decode` (VSS1-03) **off by default**: opt-in certificate-checked exact-closure pruning of the compiler-tree forest before soft ranking, on the DSL-native path only. **Experimental and unmeasured — no checkpoint uses it and it carries no ship/quality claim** ([config glossary](design/quality-experiment-matrix.md#configuration-glossary--verified-solver-decode-vss1-03)). |
 | Eval gates | Multi-suite `--ship-gates` (parse, structural, `placeholder_fidelity`, reward) |
 
 ---

docs/design/lattice-recursive-search.md

@@ -80,6 +80,25 @@ retained compiler-forest adapter and is unchanged. The full state machine and th
 certified-deduction / reversible-decision / local-nogood / certified-contradiction /
 timeout table live in
 [verified-scope-solver.md](verified-scope-solver.md). Not wired into decode.
+
+### Decode integration behind a flag (VSS1-03)
+
+[`dsl/solver/decode.py`](../../src/slm_training/dsl/solver/decode.py)
+`solver_prune` and [`models/twotower.py`](../../src/slm_training/models/twotower.py)
+`_solver_prune_forest` finally wire this hard/soft split into the compiler-tree
+lattice decode: inside `_compiler_ltr_decode_one`, right after
+`build_completion_forest`, the authoritative forest is projected to a
+`FiniteDomainState`, exact closure runs, and the forest is pruned to the
+certificate-checked live subset **before** `rank_forest` scores anything. So a
+learned ranker only ever reorders candidates that survived certified deduction; it
+can neither reintroduce a certified-removed path (survivors are a subset that keeps
+`CompletionPath` identity and forest order) nor rescue an `UNKNOWN` into removal
+(`keep_and_rank` keeps it live). A certified bottom empties the forest and reuses
+the existing `LatticeSearchState` rollback rather than emitting an unverified
+fallback. The whole seam is gated by `verified_solver_decode` (**default off**);
+off, the lattice decode and its stats/trace output are byte-identical, so the V9
+campaign rows and all measured results below are unaffected. The enabled path is
+**unmeasured** — no new campaign row, checkpoint, or ship claim.
 ## Constraint evidence (VSS0-02)
 
 The hard-lattice projection can now explain itself. `build_completion_forest(...,

docs/design/quality-experiment-matrix.md

@@ -149,6 +149,35 @@ python -m scripts.train_rl \
 python -m scripts.bench_telemetry --train-steps 8 --gen-prompts 8
 ```
 
+## Configuration glossary — verified-solver decode (VSS1-03)
+
+Experimental, **disabled by default**, and **unmeasured**. These flags gate the
+certificate-checked exact-closure pruning of the compiler-tree forest before soft
+ranking (`docs/design/verified-scope-solver.md` → "Implemented decode
+integration"). They are **not** part of any honest gate, champion recipe, or
+matrix row; no row above enables them, and the honest ship policy
+(`STRICT_COMPILER_TREE_POLICY`) does not set them. Enabling changes decode
+behavior only for the semantic choice/compiler path on a DSL-native pack; an
+unsupported tokenizer/pack raises a capability error.
+
+| Flag (`TwoTowerConfig` / `ModelBuildConfig`) | CLI (`evaluate_model.py`) | Default | Meaning |
+| --- | --- | --- | --- |
+| `verified_solver_decode` | `--verified-solver-decode` | `False` | Master switch. Off ⇒ decode is byte-identical to today. |
+| `solver_max_nodes` | `--solver-max-nodes` | `512` | Enumeration node budget per decision (also bounds the token budget). |
+| `solver_max_depth` | — (config/checkpoint) | `64` | Search depth budget. |
+| `solver_max_backtracks` | — (config/checkpoint) | `64` | Backtrack budget. |
+| `solver_max_verifier_calls` | — (config/checkpoint) | `64` | Verifier-call budget. |
+| `solver_max_wall_ms` | — (config/checkpoint) | `0` | `0` = no wall timer; deterministic budgets stay authoritative. |
+| `solver_unknown_policy` | `--solver-unknown-policy` | `keep_and_rank` | Only supported value: `UNKNOWN` candidates stay live for the soft ranker. |
+| `solver_certificate_mode` | `--solver-certificate-mode` | `summary` | `none \| summary \| full` certificate detail. |
+
+```bash
+# Opt-in solver-pruned decode on the honest compiler-tree path (experimental).
+python -m scripts.evaluate_model --checkpoint <ckpt> \
+  --verified-solver-decode --solver-max-nodes 512 \
+  --solver-unknown-policy keep_and_rank --solver-certificate-mode summary
+```
+
 ## Measured results (CPU, 800 steps, scratch, no DESIGN.md in context)
 
 See [quality-matrix-results.json](quality-matrix-results.json). Headline deltas vs ship memorizer:

docs/design/verified-scope-solver.md

@@ -290,6 +290,65 @@ controller validates the returned sequence is a permutation and rejects any
 missing/extra/duplicate); `CERTIFIED_UNSAT` is impossible when any required branch
 was UNKNOWN or budget-truncated; every `SOLVED` carries a final verifier report.
 
+## Implemented decode integration (VSS1-03 / SLM-63)
+
+[`dsl/solver/decode.py`](../../src/slm_training/dsl/solver/decode.py) adds
+`solver_prune(forest, prefix_ids, provider, ...)`, and
+[`models/twotower.py`](../../src/slm_training/models/twotower.py)
+`_solver_prune_forest` wires it into the compiler-tree / choice decode loop
+(`_compiler_ltr_decode_one`, right after `build_completion_forest`). It is gated
+by eight backward-compatible, **disabled-by-default** config fields
+(`verified_solver_decode=False`, `solver_max_nodes`, `solver_max_depth`,
+`solver_max_backtracks`, `solver_max_verifier_calls`, `solver_max_wall_ms`,
+`solver_unknown_policy="keep_and_rank"`, `solver_certificate_mode`) on
+`TwoTowerConfig` / `ModelBuildConfig`; missing fields on existing checkpoints take
+the defaults, so the flag round-trips through config/CLI/checkpoint metadata
+without adding a model parameter.
+
+Per decode decision, when the flag is on and the forest is authoritative:
+
+```text
+forest = build_completion_forest(prefix)      # unchanged; the authoritative set
+if forest.coverage != "complete" or not forest.paths:
+    return forest                             # closure is authoritative only over exhaustive coverage
+state  = completion_forest_state(prefix, forest, pack, cv, bounds)   # one-hole projection
+result = exact_closure(state, provider)       # VSS1-01 certified fixed point
+removed = {v for v in state.domain} - {v for v in result.survivors} # certified-removed only
+forest' = forest keep-order minus paths whose (kind, token_ids) in removed
+```
+
+Honesty invariants this seam preserves (owned here):
+
+- **Subset, identity-preserving.** A surviving path is an original
+  `CompletionPath` object (full path identity and forced suffixes intact); the
+  order is the original forest order. Closure may only *remove*; it never invents
+  a candidate the forest lacked, so a later soft ranker (logits) can never
+  reintroduce a certified-removed candidate — it is simply absent.
+- **Removal needs a replay-valid certificate.** A candidate is dropped only when
+  it was in the closure input domain and got certified `UNSUPPORTED`
+  (`removed = input_domain − survivors`); the closure re-checks each certificate
+  before applying it. `UNKNOWN` (partial coverage / unavailable capability /
+  budget) is always kept — `keep_and_rank` is the only supported policy.
+- **Certified bottom ≠ fallback.** When every candidate is certified
+  `UNSUPPORTED`, the pruned forest is **empty**, and the existing decode
+  dead-end/rollback path handles it — never an unverified fallback emission.
+- **Capability error, not a silent weaker path.** With the flag on, an
+  unsupported tokenizer/pack (`is_dsl_native_tokenizer` false) raises a clear
+  `ValueError` instead of quietly decoding without the solver while reporting
+  solver mode.
+- **Model-independent enumeration.** `decode.py` is Torch-free; support
+  enumeration runs no denoiser forward. The reference oracle order is
+  model-independent; the model scores only the surviving live set afterward.
+
+With `verified_solver_decode=False` the seam is skipped entirely (a single
+`getattr` guard), so default decode is byte-identical — pinned by
+`tests/test_models/test_solver_decode_integration.py` (fixed seed/fixture parity)
+and the unchanged `tests/test_models/test_compiler_decode.py`. Core
+removal/keep/bottom/coverage semantics are pinned Torch-free by
+`tests/test_dsl/test_solver_decode.py`. **No train, eval, benchmark, checkpoint,
+or experiment ran; the enabled path is unmeasured and this makes no correctness,
+readiness, speed, or ship claim.**
+
 ## Reference support semantics
 
 | Verdict | Requirement | Removal permitted? |

scripts/evaluate_model.py

@@ -214,6 +214,20 @@ def main(argv: list[str] | None = None) -> int:
     parser.add_argument("--compiler-search-noise", type=float, default=0.0)
     parser.add_argument("--compiler-search-stagnation-patience", type=int, default=2)
     parser.add_argument("--compiler-search-backtrack-limit", type=int, default=8)
+    parser.add_argument(
+        "--verified-solver-decode",
+        action="store_true",
+        help="VSS1-03: prune the compiler forest via certified exact closure before ranking",
+    )
+    parser.add_argument("--solver-max-nodes", type=int, default=512)
+    parser.add_argument(
+        "--solver-unknown-policy", choices=("keep_and_rank",), default="keep_and_rank"
+    )
+    parser.add_argument(
+        "--solver-certificate-mode",
+        choices=("none", "summary", "full"),
+        default="summary",
+    )
     parser.add_argument(
         "--schema-in-context",
         action="store_true",
@@ -414,6 +428,10 @@ def main(argv: list[str] | None = None) -> int:
         grammar_verify_chosen_only=(True if args.verify_chosen_only else None),
         grammar_top_k=args.grammar_top_k,
         compiler_decode_mode=args.compiler_decode_mode,
+        verified_solver_decode=args.verified_solver_decode,
+        solver_max_nodes=args.solver_max_nodes,
+        solver_unknown_policy=args.solver_unknown_policy,
+        solver_certificate_mode=args.solver_certificate_mode,
         component_inventory_decode_weight=args.component_inventory_decode_weight,
         component_plan_decode_weight=args.component_plan_decode_weight,
         component_edge_decode_weight=args.component_edge_decode_weight,

src/slm_training/dsl/solver/decode.py

@@ -0,0 +1,93 @@
+"""Decode-time forest pruning via certificate-checked exact closure (VSS1-03).
+
+`solver_prune` adapts an authoritative :class:`CompletionForest` to a
+:class:`FiniteDomainState`, runs exact closure, and returns the forest pruned to
+the **certificate-checked live subset** — a subset of the original paths that
+preserves full path identity/forced suffixes and the original forest order.
+
+Honesty invariants (owned by ``docs/design/verified-scope-solver.md``):
+
+* it only prunes when ``forest.coverage == "complete"`` — closure is authoritative
+  only over an exhaustive candidate set; a ``partial``/``none`` forest is returned
+  unchanged;
+* ``UNKNOWN`` candidates are always kept (``keep_and_rank``); only replay-valid
+  ``UNSUPPORTED`` candidates are dropped, so a later soft ranker (logits) can never
+  reintroduce a removed candidate — it is simply absent from the pruned forest;
+* a certified bottom yields an **empty** pruned forest, letting the existing decode
+  dead-end/rollback path handle it rather than returning an unverified fallback.
+
+This module is Torch-free and is **not** invoked by default decode — the caller
+gates it behind a disabled-by-default flag.
+"""
+
+from __future__ import annotations
+
+from slm_training.dsl.grammar.fastpath.compiler_draft import CompletionForest
+from slm_training.dsl.solver.adapters import completion_forest_state
+from slm_training.dsl.solver.closure import ClosureResult, SupportProvider, exact_closure
+from slm_training.dsl.solver.state import SolverBounds
+from slm_training.dsl.solver.support import SupportCertificate
+
+UNKNOWN_POLICIES = ("keep_and_rank",)
+
+
+def _value_key(value) -> tuple[str, tuple[int, ...]]:
+    payload = value.payload
+    return (
+        str(payload.get("kind", "")),
+        tuple(int(token) for token in payload.get("token_ids", ())),
+    )
+
+
+def solver_prune(
+    forest: CompletionForest,
+    prefix_ids,
+    provider: SupportProvider,
+    *,
+    pack_id: str,
+    constraint_version: str,
+    bounds: SolverBounds,
+    unknown_policy: str = "keep_and_rank",
+    state=None,
+    cache: dict | None = None,
+    certificate_store: dict[str, SupportCertificate] | None = None,
+) -> tuple[CompletionForest, ClosureResult | None]:
+    """Return ``(pruned_forest, closure_result)`` for one decode decision.
+
+    A forest path is removed **only** when it was in the closure's input domain and
+    got certified-removed (``removed = original_domain − survivors``); a candidate
+    the oracle never considered is always kept. ``state`` may be a pre-built
+    projection (e.g. the provider's own root state) so fingerprints line up with
+    the oracle; when ``None`` it is projected from ``forest``. ``closure_result`` is
+    ``None`` when no closure ran (non-``complete`` coverage or empty forest).
+    """
+    if unknown_policy not in UNKNOWN_POLICIES:
+        raise ValueError(f"unsupported solver_unknown_policy: {unknown_policy!r}")
+    if forest.coverage != "complete" or not forest.paths:
+        return forest, None
+
+    if state is None:
+        state = completion_forest_state(
+            prefix_ids=tuple(int(token) for token in prefix_ids),
+            forest=forest,
+            pack_id=pack_id,
+            constraint_version=constraint_version,
+            bounds=bounds,
+        )
+    result = exact_closure(
+        state, provider, cache=cache, certificate_store=certificate_store
+    )
+    original = state.holes[0].values if state.holes else ()
+    survivors = result.state.holes[0].values if result.state.holes else ()
+    # Only paths the closure actually certified-removed are dropped.
+    removed_keys = {_value_key(v) for v in original} - {_value_key(v) for v in survivors}
+    if not removed_keys:
+        return forest, result  # nothing certified-removed -> keep identity
+    ordered = tuple(
+        path
+        for path in forest.paths
+        if (path.kind, tuple(path.token_ids)) not in removed_keys
+    )
+    if len(ordered) == len(forest.paths):
+        return forest, result
+    return CompletionForest(ordered, forest.coverage, forest.terminals), result

src/slm_training/harnesses/model_build/config.py

@@ -122,6 +122,15 @@ class ModelBuildConfig:
     compiler_search_stagnation_patience: int = 2
     compiler_search_backtrack_limit: int = 8
     compiler_search_local_nogoods: bool = False
+    # VSS1-03 certified-solver decode (disabled by default; decode-time only).
+    verified_solver_decode: bool = False
+    solver_max_nodes: int = 512
+    solver_max_depth: int = 64
+    solver_max_backtracks: int = 64
+    solver_max_verifier_calls: int = 64
+    solver_max_wall_ms: int = 0
+    solver_unknown_policy: str = "keep_and_rank"
+    solver_certificate_mode: str = "summary"
     decode_min_content: int = 0  # A4: 0 off | >0 floor | -1 auto-from-inventory
     asap_decode: bool = False  # A2: ASAp-style constraint-mass removal in MaskGIT
     fastpath_aux_weight: float = 0.0

src/slm_training/harnesses/model_build/factory.py

@@ -71,6 +71,14 @@ def apply_runtime_overrides(model: Any, config: ModelBuildConfig) -> Any:
         "compiler_search_stagnation_patience",
         "compiler_search_backtrack_limit",
         "compiler_search_local_nogoods",
+        "verified_solver_decode",
+        "solver_max_nodes",
+        "solver_max_depth",
+        "solver_max_backtracks",
+        "solver_max_verifier_calls",
+        "solver_max_wall_ms",
+        "solver_unknown_policy",
+        "solver_certificate_mode",
         "decode_min_content",
         "asap_decode",
         "fastpath_aux_weight",
@@ -295,6 +303,20 @@ def _twotower_config_from_build(config: ModelBuildConfig) -> "TwoTowerConfig":
         ),
         decode_min_content=max(-1, int(getattr(config, "decode_min_content", 0) or 0)),
         asap_decode=bool(getattr(config, "asap_decode", False)),
+        verified_solver_decode=bool(getattr(config, "verified_solver_decode", False)),
+        solver_max_nodes=int(getattr(config, "solver_max_nodes", 512) or 512),
+        solver_max_depth=int(getattr(config, "solver_max_depth", 64) or 64),
+        solver_max_backtracks=int(getattr(config, "solver_max_backtracks", 64) or 64),
+        solver_max_verifier_calls=int(
+            getattr(config, "solver_max_verifier_calls", 64) or 64
+        ),
+        solver_max_wall_ms=int(getattr(config, "solver_max_wall_ms", 0) or 0),
+        solver_unknown_policy=str(
+            getattr(config, "solver_unknown_policy", "keep_and_rank")
+        ),
+        solver_certificate_mode=str(
+            getattr(config, "solver_certificate_mode", "summary")
+        ),
         fastpath_aux_weight=getattr(config, "fastpath_aux_weight", 0.0),
         fastpath_gate_threshold=float(
             getattr(config, "fastpath_gate_threshold", 0.5) or 0.5