From 8de7bc8d09e84e8e26f3548802ecf819d0e9876a Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 20:50:03 +0000 Subject: [PATCH 1/9] Add bounded verified-scope-solver architecture contract (SLM-57) Specify the guarantee boundary separating prefix legality from support (participation in a bounded, fully verified completion) for the Verified Scope Solving & Hybrid Realization project. Spec-only: no solver code, dependency, experiment, or checkpoint; decode behavior is unchanged until a later VSS issue enables new flags. - docs/design/verified-scope-solver.md: term definitions, SUPPORTED / UNSUPPORTED / UNKNOWN semantics (UNKNOWN never removes a candidate), a deterministic bounded-enumeration reference backend (no SMT/Z3) plus an optional future backend protocol, certificate replay and the deduction-vs-decision transitions with every destructive step citing an exact proof/replay, capsule SCC boundaries, late realization, a relationship-to-existing-code table, and an end-to-end partial-coverage live-UNKNOWN example. - research-lineage.md: VSS0 research anchors (DeepCoder, CEGIS, egg / e-graphs, EDLM, TreeDiff, LDT) with the existing Faithful/Adapted/ Surrogate/Adjacent fidelity vocabulary; none tagged Faithful (spec-only). - README.md: register the new doc in the design-doc navigation index. Verified: python -m scripts.repo_policy ok, check-changed selects no tests (docs-only), git diff --check clean, all relative links resolve. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01MeD6nTTabPQhva7pXtTMNj --- README.md | 2 +- docs/design/research-lineage.md | 24 +++ docs/design/verified-scope-solver.md | 303 +++++++++++++++++++++++++++ 3 files changed, 328 insertions(+), 1 deletion(-) create mode 100644 docs/design/verified-scope-solver.md diff --git a/README.md b/README.md index bd3cb506..4e191c0b 100644 --- a/README.md +++ b/README.md @@ -24,7 +24,7 @@ future campaign evidence. The loop improves by evidence, never by rewriting its code, frozen cases, or gates. RL remains locked until a model passes the frozen production readiness contract. -See [docs/design/model-lineage.md](docs/design/model-lineage.md) (canonical two-track cycle), [docs/design/openui-twotower.md](docs/design/openui-twotower.md), [docs/design/grammar-topology-diffusion.md](docs/design/grammar-topology-diffusion.md) (dynamic production-tree diffusion), [docs/design/research-lineage.md](docs/design/research-lineage.md) (papers → code), [docs/design/research-correction-critics.md](docs/design/research-correction-critics.md) (V4 remask / trust-gate / honest inventory; V6 CoRe/T2M), [docs/design/verifier-stack.md](docs/design/verifier-stack.md) (G0–G12 corpus gates + confidence tiers), [docs/design/abstraction-house-style.md](docs/design/abstraction-house-style.md) (L0–L5 determinacy, grounding, and canonical defaults), [docs/design/verifier-guided-repair.md](docs/design/verifier-guided-repair.md) (PDDL-Instruct / verifier-repair applicability map), [docs/design/quality-experiment-matrix.md](docs/design/quality-experiment-matrix.md) (E0–E75 + X0–X15 matrices; E34 deferred), [docs/design/speculative-denoising.md](docs/design/speculative-denoising.md) (V7 stability / dependency-cluster / survival / successor-cache decode), [docs/design/dsl-native-tokenizer.md](docs/design/dsl-native-tokenizer.md) (V5 lexer alphabet), [docs/design/grammar-fastpath.md](docs/design/grammar-fastpath.md), [docs/design/grammar-backends.md](docs/design/grammar-backends.md), [docs/design/dsl-pack-contract.md](docs/design/dsl-pack-contract.md) (F1 DSL-pack contract; OpenUI first pack), [docs/design/structure-only-eval.md](docs/design/structure-only-eval.md), [docs/design/adversarial-review.md](docs/design/adversarial-review.md), [docs/design/runtime-performance.md](docs/design/runtime-performance.md), [docs/design/hf-jobs-train.md](docs/design/hf-jobs-train.md) (HF Jobs full train — not ZeroGPU), [docs/design/gpu-multi-farm-mcp.md](docs/design/gpu-multi-farm-mcp.md), and [docs/MODEL_CARD.md](docs/MODEL_CARD.md). +See [docs/design/model-lineage.md](docs/design/model-lineage.md) (canonical two-track cycle), [docs/design/openui-twotower.md](docs/design/openui-twotower.md), [docs/design/grammar-topology-diffusion.md](docs/design/grammar-topology-diffusion.md) (dynamic production-tree diffusion), [docs/design/verified-scope-solver.md](docs/design/verified-scope-solver.md) (VSS0 verified scope-solver contract — prefix legality vs verified support), [docs/design/research-lineage.md](docs/design/research-lineage.md) (papers → code), [docs/design/research-correction-critics.md](docs/design/research-correction-critics.md) (V4 remask / trust-gate / honest inventory; V6 CoRe/T2M), [docs/design/verifier-stack.md](docs/design/verifier-stack.md) (G0–G12 corpus gates + confidence tiers), [docs/design/abstraction-house-style.md](docs/design/abstraction-house-style.md) (L0–L5 determinacy, grounding, and canonical defaults), [docs/design/verifier-guided-repair.md](docs/design/verifier-guided-repair.md) (PDDL-Instruct / verifier-repair applicability map), [docs/design/quality-experiment-matrix.md](docs/design/quality-experiment-matrix.md) (E0–E75 + X0–X15 matrices; E34 deferred), [docs/design/speculative-denoising.md](docs/design/speculative-denoising.md) (V7 stability / dependency-cluster / survival / successor-cache decode), [docs/design/dsl-native-tokenizer.md](docs/design/dsl-native-tokenizer.md) (V5 lexer alphabet), [docs/design/grammar-fastpath.md](docs/design/grammar-fastpath.md), [docs/design/grammar-backends.md](docs/design/grammar-backends.md), [docs/design/dsl-pack-contract.md](docs/design/dsl-pack-contract.md) (F1 DSL-pack contract; OpenUI first pack), [docs/design/structure-only-eval.md](docs/design/structure-only-eval.md), [docs/design/adversarial-review.md](docs/design/adversarial-review.md), [docs/design/runtime-performance.md](docs/design/runtime-performance.md), [docs/design/hf-jobs-train.md](docs/design/hf-jobs-train.md) (HF Jobs full train — not ZeroGPU), [docs/design/gpu-multi-farm-mcp.md](docs/design/gpu-multi-farm-mcp.md), and [docs/MODEL_CARD.md](docs/MODEL_CARD.md). ## Model card (summary) diff --git a/docs/design/research-lineage.md b/docs/design/research-lineage.md index 032be3c4..69655f7d 100644 --- a/docs/design/research-lineage.md +++ b/docs/design/research-lineage.md @@ -510,6 +510,30 @@ The code substrate is `data/progspec/scopes.py`, the conditional heads in `models/grammar_diffusion.py`, and planned matrix rows X16-X21. No X16-X21 run, quality gain, or ship status is recorded by this implementation-only change. +## Verified scope solving & hybrid realization (VSS0) + +[verified-scope-solver.md](verified-scope-solver.md) (VSS0-01, SLM-57) is the +spec-only contract that separates **prefix legality** (already enforced by the +compiler completion forest) from **support** — participation in at least one +bounded, fully verified completion. It adds no code, dependency, experiment, or +checkpoint. The anchors below are lineage labels for that contract, not reproduced +results; because SLM-57 ships no code, none is **Faithful**. TreeDiff and the +Lattice Deduction Transformer reuse their existing R13/R7 labels from the V9 +sources ([lattice-recursive-search.md](lattice-recursive-search.md)); grouping the +batch here avoids treating adjacent papers as independent evidence for one lever. + +| Paper | Fidelity | Role in the VSS0 contract (spec-only) | +| --- | --- | --- | +| [DeepCoder](https://arxiv.org/abs/1611.01989) (Balog et al., ICLR 2017) | **Adjacent** | Learned search-guidance / candidate ranking; the contract keeps learned scores soft (`rank_forest`) and does not reimplement its attribute predictor or DSL | +| Counterexample-guided (neural) synthesis / CEGIS — see the *LLM-Modulo / CEGIS planning* anchor above and R19/R23 in [lattice-recursive-search.md](lattice-recursive-search.md) | **Adapted boundary** | Deduction-vs-decision split and local nogoods adopt the counterexample → refinement principle; neural synthesis training is not reimplemented | +| [egg / e-graphs](https://arxiv.org/abs/2004.03082) (Willsey et al., POPL 2021) | **Adjacent** | Post-realization canonicalization is motivated by equality saturation, but the contract is not an e-graph / equality-saturation engine (cf. `iter-e252-canonicalizer-20260716.md`) | +| EDLM — energy-based diffusion language model (2024) | **Adjacent** | Energy/score-based candidate ranking is analogous to the soft-scoring layer; no EDLM training or energy head is implemented or assumed | +| [TreeDiff](https://arxiv.org/abs/2508.01473) (Zeng et al., 2025) | **Adapted boundary** | Tree-edit diffusion informs late realization against AST/choice IR; architecture and training remain future empirical work (as R13) | +| [Lattice Deduction Transformer](https://arxiv.org/abs/2605.08605) (Davis et al., 2026) | **Adapted** | Monotone lattice projection plus rollback are the closure/deduction model; LDT architecture, alpha supervision, and training remain future work (as R7) | + +No solver, experiment, checkpoint, or ship status follows from this spec-only +anchor set; the contract is implemented behind a feature flag by later VSS issues. + ## DSL diffusion research program (Tracks A-G) The 2026-07-16 prior-art sweep for the DSL diffusion SLM research program diff --git a/docs/design/verified-scope-solver.md b/docs/design/verified-scope-solver.md new file mode 100644 index 00000000..f0556472 --- /dev/null +++ b/docs/design/verified-scope-solver.md @@ -0,0 +1,303 @@ +# VSS0-01 (SLM-57): the bounded verified-scope-solver contract + +**Status:** specification only. This document defines the guarantee boundary for +the *Verified Scope Solving & Hybrid Realization* project. It adds no solver +code, no runtime dependency, no experiment, and no checkpoint, and makes no model +or ship claim. Existing checkpoints and decode behavior are unchanged until a +later VSS issue enables new flags behind a feature gate. + +**Code:** none (contract/spec only). + +**Reader contract:** `docs/design/` is the source of truth for coding agents and +experiment reviewers; the Linear project document is planning context only. The +terms and transitions below are meant to be precise enough that subsequent issues +can implement dataclasses and state transitions without inventing semantics. + +## The distinction this contract adds + +The repository already keeps [`CompletionForest`](../../src/slm_training/dsl/grammar/fastpath/compiler_draft.py) +authoritative and lets soft scores only *rank* it — see +[lattice-recursive-search.md](lattice-recursive-search.md), whose subordination +principle is that logits "cannot create a legal branch, discard all legal +branches, or bypass final OpenUI validation." + +What is missing is a contract distinguishing two properties that are currently +conflated in review discussion: + +- **prefix legality** — a candidate is compiler-admissible as the next action at + the current decode position (Lark CFG reachability plus AST/binder/schema + filters, as enumerated by `build_completion_forest`). This already exists. +- **support** — a candidate participates in **at least one bounded, fully + verified completion**. This does **not** exist yet and is what this contract + governs. + +> **Disambiguation (do not drift).** "Support" here is *participation in a +> verified completion*. It is distinct from the existing **support signature** +> telemetry of E283 +> ([iter-e283-signature-support-repair-20260717.md](iter-e283-signature-support-repair-20260717.md)), +> which is the coverage tuple `decision_kind + legal_token_ids + selected_token_id`. +> The E283 signature is decode-coverage instrumentation; it is **not** a +> completion-participation verdict and never authorizes candidate removal. + +## Terms + +Each term is defined so subsequent issues can implement dataclasses and state +transitions without inventing semantics. + +- **`HoleId`** — stable identifier for a single unresolved decision site in the + program IR (a position that must be filled by a choice/subtree). Stable across + reversible search so certificates and nogoods can reference it. New symbol + (absent today). +- **finite domain** — the declared, bounded set of candidate fillings for a + `HoleId` under the current pack/compiler coverage. Finiteness within declared + bounds is a precondition for exact closure; a domain not provably finite within + declared bounds yields `UNKNOWN` results. (Nearest existing phrasing: the + lattice doc's "finite partial-information state"; formalized here.) +- **state fingerprint** — a canonical, order-insensitive hash of the solver state + relevant to a hole (bound holes, active constraints, pack/compiler/verifier + versions) used to key caches, certificates, and nogoods. Two states with the + same fingerprint are interchangeable for replay. (Compare the existing + `RankedForest.signature` and `ChoiceDecodeState.signature`, which hash search + state but do not certify support.) +- **bottom** (`⊥`) — the empty domain: a hole with no legal candidate. A hole + reaching bottom is a certified local contradiction; its incoming decision is + certified UNSAT, distinct from timeout/`UNKNOWN`. (The existing empty + `CompletionForest` / `RankedForest.is_bottom` is the structural precursor.) +- **structurally solved** — every `HoleId` in scope has a chosen candidate and + the resulting IR has no remaining holes, but semantic verification has not yet + been applied. +- **verified terminal** — a structurally solved state whose completion has been + accepted by the applicable verifier(s) (the G0-G12 gate stack of + [verifier-stack.md](verifier-stack.md), at the property tier claimed). The only + state from which `SUPPORTED` may be asserted. +- **`SUPPORTED`** — status of a candidate for which a verifier-accepted witness + completion (a verified terminal using that candidate) exists. +- **`UNSUPPORTED`** — status of a candidate proven to appear in **no** verified + terminal, established only by exhaustive search with complete compiler coverage + over that candidate's finite sub-domain, inside declared bounds. +- **`UNKNOWN`** — status when coverage is partial, a pack capability is + unavailable, a node/verifier/time budget is exhausted, or a version is stale. + `UNKNOWN` never permits candidate removal. +- **exact closure** — the deterministic fixpoint that propagates certified + deductions (domain reductions that hold in *every* completion) until no further + certified reduction applies. Exact closure only ever removes candidates that + are certified `UNSUPPORTED`. +- **proof certificate** — a replayable record justifying a destructive + transition: the state fingerprint, the pack/compiler/verifier versions, the + transition, and the minimal evidence (witness for `SUPPORTED`, + complete-coverage attestation for `UNSUPPORTED`, or a nogood derivation). + Replaying a certificate against its recorded fingerprint must reproduce the same + verdict; a certificate that does not replay is treated as absent. +- **certified deduction** — a domain reduction accepted by exact closure because + a proof certificate shows it holds in every completion. Certified deductions + are **not** reversible. +- **reversible decision** — a search branch that is *not* certified; it is + recorded on the trail and undone on backtracking. Learned proposals enter here. + (Existing precursor: `LatticeSearchState.choose`/`rollback`.) +- **local nogood** — a certified partial assignment that leads to bottom, + recorded (keyed by state fingerprint) so the same dead region is not + re-explored. A nogood is itself a proof certificate. (Existing precursor: the + `Nogood` memory in `lattice_search.py`, which today lacks a replay certificate.) +- **verification capsule** — a dependency-closed unit of holes solved and verified + together. Capsule boundaries are **strongly-connected components (SCCs)** of the + hole-dependency graph, built from the def/use edges of + [`ScopeContract`](../../src/slm_training/data/progspec/scopes.py) + (`definitions`/`uses`/`visible_binders`). New vocabulary: a capsule is **not** a + lexical/AST `ScopeKind` scope and is **not** the `dependency_closed_failure_cone` + helper (which computes an AST least-common-ancestor, not an SCC). Scopes are not + assumed independent. +- **opaque region** — a span the solver does not model semantically (e.g. + user-owned/stripped content); preserved verbatim and spliced back hygienically, + never used to justify a destructive transition. +- **semantic field** — a field whose value is constrained by verified semantics; + it must pass through choice/AST IR and the verifier. +- **surface-only field** — a field with no semantic constraint beyond + well-formedness; the only field class where unrestricted autoregression is + permitted, subject to canonicalization plus the applicable pack oracle + afterward. + +## Reference support semantics + +| Verdict | Requirement | Removal permitted? | +| --- | --- | --- | +| `SUPPORTED` | A verifier-accepted witness completion (verified terminal) exists that uses the candidate. | Candidate stays live. | +| `UNSUPPORTED` | Exhaustive search with **complete** compiler coverage over the candidate's finite sub-domain, inside declared bounds, finds no verified terminal using it. | **Yes — only** with a replayable `UNSUPPORTED` certificate. | +| `UNKNOWN` | Partial coverage, unavailable pack capability, node/verifier/time-budget exhaustion, or stale version. | **Never.** | + +Coverage completeness is evaluated over **each candidate's own finite +sub-domain**, not only globally: a forest whose overall `coverage` is `partial` +may still certify one candidate `UNSUPPORTED` when that candidate's sub-domain has +complete coverage, while another candidate in the same forest is `UNKNOWN`. + +### Required invariants + +- Learned modules may rank or propose; they never create legality and never + produce `SUPPORTED`/`UNSUPPORTED` without a certificate. +- A learned proposal without an accepted certificate is reversible or ignored. +- Singleton domains still require final verification before `SUPPORTED`. +- Certified `UNSUPPORTED`/UNSAT is distinct from timeout/`UNKNOWN`. +- Correctness claims name the verified property tier; `G0-G12` is **not** + represented as a universal semantic proof (see the verification ceiling in + [verifier-stack.md](verifier-stack.md)). +- Existing checkpoints and decode behavior remain unchanged until a later issue + enables new flags. + +## Default reference backend + +The default reference backend is **deterministic bounded enumeration** over the +existing choice/compiler path (`build_completion_forest` plus +`CompletionForest.coverage` plus the length-aware `ChoiceDecodeState.allowed_ids` +/ `exhaustive_allowed_ids`). **No SMT/Z3 is required** to install or run the +default backend. + +An **optional future backend protocol** is defined for later issues only. A +conforming backend must (1) accept a state fingerprint plus a finite domain, +(2) return exactly one of `SUPPORTED`/`UNSUPPORTED`/`UNKNOWN` together with a +replayable certificate, and (3) never assert `UNSUPPORTED` without a +complete-coverage attestation. Backends are pluggable behind this protocol only; +none beyond bounded enumeration is required or assumed installed. + +## Certificate replay and the deduction-vs-decision transition + +Reference closure pseudocode. **Every destructive transition (the only lines that +remove a candidate or retract a decision) cites a required exact proof/replay +step**; non-destructive transitions do not: + +```text +def close(hole): # hole.domain is a finite domain + for cand in hole.domain: + v = classify(cand, hole.state) # SUPPORTED | UNSUPPORTED | UNKNOWN + if v is SUPPORTED: + keep_live(cand) # non-destructive; needs verifier witness + elif v is UNSUPPORTED: + cert = exhaustive_certificate(cand, hole.state) # REQUIRED: complete-coverage attestation + require(replay(cert) is UNSUPPORTED) # REQUIRED: replay reproduces verdict + remove(cand, because=cert) # DESTRUCTIVE — the only candidate-removal path + else: # UNKNOWN + keep_live(cand) # removal forbidden by invariant + if hole.domain is BOTTOM: # ⊥ : certified local contradiction + nogood = derive_nogood(hole.state) # REQUIRED before retracting the parent + record(nogood) # nogood is itself a replayable certificate + retract_parent(hole, because=nogood) # DESTRUCTIVE — cites the nogood +``` + +Deduction vs decision: + +- A **certified deduction** (`remove`, `retract_parent`) is destructive and + irreversible; it exists only with a replayable certificate. +- A **reversible decision** (`choose` a branch) is non-destructive, recorded on + the trail, and undone on backtrack; no certificate required. +- Replay requirement: every certificate stores the state fingerprint and the + pack/compiler/verifier versions, so an independent replay reaches the identical + verdict. Stale versions or a non-replaying certificate ⇒ transition disallowed, + candidate stays live. + +## Capsule boundaries (dependency-closed SCCs) + +Capsules are the strongly-connected components of the hole-dependency graph built +from `ScopeContract` def/use edges. Mutually constraining holes are solved jointly +in one capsule; independent SCCs are solved separately and joined through +interface summaries. This contract fixes that **capsules, not lexical/AST scopes, +are the unit of joint solving and verification**; the SCC decomposition itself is +implemented by a later issue. Lexical/AST `ScopeKind` boundaries +(`COMPONENT_CALL`/`STATEMENT`/`CHILD_LIST`) are inputs to that construction, not +the closure. + +## Late realization + +- Unrestricted autoregression is permitted **only** for fields classified + surface-only. +- Realization occurs against the AST/choice IR — the B1 choice-sequence codec + ([iter-b1-choice-sequence-codec-20260717.md](iter-b1-choice-sequence-codec-20260717.md), + `models/choice_tokenizer.py`) — not the raw token stream. +- Every realized field is followed by canonicalization plus the applicable pack + oracle (`DslPack` `ValidityOracle`, see + [dsl-pack-contract.md](dsl-pack-contract.md)); a field that fails the oracle is + rejected as a reversible decision, never destructively removed without a + certificate. +- Semantic fields never take the autoregressive path. + +## Relationship to existing implementation + +| Symbol (file:line) | Existing role | Disposition under this contract | +| --- | --- | --- | +| `CompletionForest` (`fastpath/compiler_draft.py:29`) | Frozen enumerated next-action set for a prefix, carrying a `coverage: Coverage` guarantee (`complete`/`partial`/`none`) and `candidate_ids`. | **Retained, authoritative.** The support layer sits above it; its `coverage` tag is the substrate mapping to `SUPPORTED`/`UNSUPPORTED`/`UNKNOWN`. Not duplicated. | +| `build_completion_forest` (`fastpath/compiler_draft.py:619`) | Deterministic bounded enumerator over the Lark CFG path (prefix legality via `OpenUIIncrementalEngine`). | **Retained.** Serves as the default reference backend's enumeration primitive. Not duplicated. | +| `LatticeSearchState` + `Nogood` (`fastpath/lattice_search.py:182`, `:16`) | Bounded backtracking search trail with local nogood memory (`choose`/`rollback`). | **Extended (later issue).** Reversible decisions and local nogoods gain replayable certificates; certified deductions become non-reversible. | +| `RankedForest` / `rank_forest` (`fastpath/lattice_search.py:24`/`:44`) | Independent soft ordering over the hard compiler candidate set. | **Retained.** Grounds the invariant that learned modules rank/propose but never create legality. Not duplicated. | +| `ScopeContract` / `ScopeKind` (`data/progspec/scopes.py:33`/`:18`) | AST scopes (`COMPONENT_CALL`/`STATEMENT`/`CHILD_LIST`) plus a def/use binder overlay (`definitions`/`uses`/`visible_binders`). | **Extended.** Scope def/use edges feed capsule SCC construction; scopes are **not** assumed independent. | +| `dependency_closed_failure_cone` (`data/progspec/scopes.py:113`) | Despite the name, computes the least-common-ancestor of failing AST paths — **not** a dependency closure or SCC. | **Not reused for capsules.** Capsule SCCs are a new, distinct construction; this contract does not duplicate or overload this helper. | +| `ChoiceTokenizer` / `ChoiceDecodeState` (`models/choice_tokenizer.py:172`/`:608`) | Grammar-closed choice IR; length-aware legality (`allowed_ids`, `exhaustive_allowed_ids`, `minimal_completion_length`). | **Retained.** The choice IR is the late-realization and verification surface. Not duplicated. | +| `HoleId`, finite `domain`, `verification capsule`, `proof certificate` | Absent today (confirmed greenfield). | **New** dataclasses/semantics introduced by later VSS issues under this contract. | + +## End-to-end example (partial coverage → live `UNKNOWN`) + +Decode a `component_call` scope with hole `h_type` for the component-type slot. +`build_completion_forest` returns three prefix-legal candidates — `Button`, +`Card`, `IconButton` — and stamps `CompletionForest.coverage = "partial"` because +the pack's schema oracle for `IconButton`'s required `icon` enum is not loaded (an +unavailable pack capability: `DslPack.require("schema")` would raise +`PackSlotUnavailable` for that node). + +Closure over `h_type.domain`: + +- **`Button`** → a verifier-accepted witness completion exists (fill `label`, + close the call). Verdict `SUPPORTED`; candidate stays live. +- **`Card`** → its finite child-list sub-domain has **complete** coverage, and + exhaustive bounded enumeration finds no verified terminal (the surrounding scope + structurally forbids the child that `Card` requires). Verdict `UNSUPPORTED`; + removed **with** a replayable `UNSUPPORTED` certificate (destructive transition, + cited). +- **`IconButton`** → its sub-domain coverage is **partial** (the missing schema + capability), so no complete-coverage exhaustive search is possible. Verdict + `UNKNOWN`. It is **not** removed: it remains live and may still be ranked or + realized, but no `SUPPORTED`/`UNSUPPORTED` verdict is asserted and no + certificate is issued. + +The forest's overall `coverage` is `partial`, yet `Card` is still certified +`UNSUPPORTED` (its own sub-domain is fully covered) while `IconButton` stays a +live `UNKNOWN`. Removing `IconButton` would violate the invariant that `UNKNOWN` +never permits candidate removal. + +## Research anchors + +Fidelity labels follow the controlled vocabulary owned by +[research-lineage.md](research-lineage.md) (**Faithful / Adapted / Surrogate / +Adjacent**); the authoritative rows for this contract are added there under +*Verified scope solving & hybrid realization (VSS0)*. Because SLM-57 ships no +code, none of these is **Faithful** — the labels are lineage-only, consistent with +the X16-X21 convention ("lineage labels, not reproduced results"). + +- **DeepCoder** (Balog et al., ICLR 2017, [arXiv:1611.01989](https://arxiv.org/abs/1611.01989)) + — **Adjacent**. Learned search-guidance / candidate ranking; the contract keeps + learned scores *soft* (ranking only, `rank_forest`) and does not reimplement it. +- **Counterexample-guided (neural) synthesis / CEGIS** — **Adapted boundary**. The + deduction-vs-decision split and local nogoods adopt the counterexample → + refinement principle; neural synthesis training is not reimplemented. See the + existing *LLM-Modulo / CEGIS planning* anchor in research-lineage.md and R19/R23 + in [lattice-recursive-search.md](lattice-recursive-search.md). +- **egg / e-graphs** (Willsey et al., POPL 2021, [arXiv:2004.03082](https://arxiv.org/abs/2004.03082)) + — **Adjacent**. Post-realization canonicalization is motivated by equality + saturation, but the contract is **not** an e-graph engine + (cf. `iter-e252-canonicalizer-20260716.md`). +- **EDLM** (energy-based diffusion language model, 2024) — **Adjacent**. Energy / + score-based candidate ranking is analogous to the soft-scoring layer; no EDLM + training or energy head is implemented or assumed. +- **TreeDiff** (Zeng et al., 2025, [arXiv:2508.01473](https://arxiv.org/abs/2508.01473)) + — **Adapted boundary** (same as R13 in the V9 sources). Tree-edit diffusion + informs late realization against AST/choice IR; architecture and training remain + future empirical work. +- **Lattice Deduction Transformer** (Davis et al., 2026, [arXiv:2605.08605](https://arxiv.org/abs/2605.08605)) + — **Adapted** (same as R7 in the V9 sources). Monotone lattice projection plus + rollback are the closure/deduction model; LDT architecture, alpha supervision, + and training remain future work. + +## Measured status + +2026-07-17 — specification-only change (VSS0-01 / SLM-57). No solver code, no +runtime dependency, no experiment, no checkpoint, and no eval run; therefore no +measured results and **no model or ship claim**. This document defines the +guarantee boundary only. `python -m scripts.repo_policy` passes; documentation +changes select no test suites (`scripts/check_changed` skips `docs/`). Later VSS +issues implement the dataclasses and state transitions specified here behind a +feature flag before any decode-behavior change. From 6f2cf2c979cf339a3a662106e414144f51aaf883 Mon Sep 17 00:00:00 2001 From: Tyler Kendrick <145080887+Tyler-R-Kendrick@users.noreply.github.com> Date: Fri, 17 Jul 2026 16:03:18 -0500 Subject: [PATCH 2/9] Define calculated arity precision contract --- README.md | 3 + .../calculated-arity-adaptive-precision.md | 268 ++++++++++++++++++ docs/design/research-lineage.md | 28 ++ 3 files changed, 299 insertions(+) create mode 100644 docs/design/calculated-arity-adaptive-precision.md diff --git a/README.md b/README.md index 4e191c0b..d8712f65 100644 --- a/README.md +++ b/README.md @@ -26,6 +26,9 @@ production readiness contract. See [docs/design/model-lineage.md](docs/design/model-lineage.md) (canonical two-track cycle), [docs/design/openui-twotower.md](docs/design/openui-twotower.md), [docs/design/grammar-topology-diffusion.md](docs/design/grammar-topology-diffusion.md) (dynamic production-tree diffusion), [docs/design/verified-scope-solver.md](docs/design/verified-scope-solver.md) (VSS0 verified scope-solver contract — prefix legality vs verified support), [docs/design/research-lineage.md](docs/design/research-lineage.md) (papers → code), [docs/design/research-correction-critics.md](docs/design/research-correction-critics.md) (V4 remask / trust-gate / honest inventory; V6 CoRe/T2M), [docs/design/verifier-stack.md](docs/design/verifier-stack.md) (G0–G12 corpus gates + confidence tiers), [docs/design/abstraction-house-style.md](docs/design/abstraction-house-style.md) (L0–L5 determinacy, grounding, and canonical defaults), [docs/design/verifier-guided-repair.md](docs/design/verifier-guided-repair.md) (PDDL-Instruct / verifier-repair applicability map), [docs/design/quality-experiment-matrix.md](docs/design/quality-experiment-matrix.md) (E0–E75 + X0–X15 matrices; E34 deferred), [docs/design/speculative-denoising.md](docs/design/speculative-denoising.md) (V7 stability / dependency-cluster / survival / successor-cache decode), [docs/design/dsl-native-tokenizer.md](docs/design/dsl-native-tokenizer.md) (V5 lexer alphabet), [docs/design/grammar-fastpath.md](docs/design/grammar-fastpath.md), [docs/design/grammar-backends.md](docs/design/grammar-backends.md), [docs/design/dsl-pack-contract.md](docs/design/dsl-pack-contract.md) (F1 DSL-pack contract; OpenUI first pack), [docs/design/structure-only-eval.md](docs/design/structure-only-eval.md), [docs/design/adversarial-review.md](docs/design/adversarial-review.md), [docs/design/runtime-performance.md](docs/design/runtime-performance.md), [docs/design/hf-jobs-train.md](docs/design/hf-jobs-train.md) (HF Jobs full train — not ZeroGPU), [docs/design/gpu-multi-farm-mcp.md](docs/design/gpu-multi-farm-mcp.md), and [docs/MODEL_CARD.md](docs/MODEL_CARD.md). +Calculated arity, task rate, neural precision, and physical cost are kept distinct +by the [CAP0 contract](docs/design/calculated-arity-adaptive-precision.md). + ## Model card (summary) Full card: **[docs/MODEL_CARD.md](docs/MODEL_CARD.md)**. Agents update both this diff --git a/docs/design/calculated-arity-adaptive-precision.md b/docs/design/calculated-arity-adaptive-precision.md new file mode 100644 index 00000000..03bdc409 --- /dev/null +++ b/docs/design/calculated-arity-adaptive-precision.md @@ -0,0 +1,268 @@ +# CAP0-01 (SLM-77): calculated arity and adaptive precision + +**Status:** specification only. This contract adds no model, solver, quantizer, +experiment, checkpoint, or ship claim. It preregisters terms, proofs, comparator +rules, and falsifiers for later CAP issues; existing decode and deployment behavior +is unchanged. + +**Owners and boundaries:** the bounded tree carrier remains in +[grammar-topology-diffusion.md](grammar-topology-diffusion.md), hard next-action +membership remains in [lattice-recursive-search.md](lattice-recursive-search.md), +and verified-completion support and destructive pruning remain in +[verified-scope-solver.md](verified-scope-solver.md). The frozen language bundle and +its declared property tiers remain in [dsl-pack-contract.md](dsl-pack-contract.md). +This document owns only capacity, task-rate, precision, physical-cost, and matched +experiment claims. Sources and fidelity labels live in +[research-lineage.md](research-lineage.md). + +## Central non-equivalence + +The program must never collapse these four quantities into one claim: + +> **exact symbolic-state capacity != task-relevant information rate != neural +> weight/activation precision != deployed system optimum** + +An exact count of legal states does not determine how many states a task must +distinguish. A task quotient does not determine the arity of weights or +activations. A nominal arity does not determine packed bytes, latency, energy, or +quality on a real kernel. Any optimum claim must therefore declare, in the same +row or sentence, the state set or task quotient, every `K` and `d` role, structural +bounds, noise model, exact/estimated status, and packing assumption when cost is +involved. + +## Declared frame and notation + +A report first freezes a frame + +`F = (pack, grammar, parser, codec, state_signature, AST/depth/scope/cutoff bounds, +traffic distribution, distortion, noise model)`. + +Changing any member creates a different claim. + +| Symbol | Meaning | Required declaration | +| --- | --- | --- | +| `Q` | Exact continuation quotient: equivalence classes of bounded compiler states that admit the same verifier-relevant continuation behavior under `F` | State representation, equivalence test, enumeration/completeness method, versions, bounds, and work count | +| `M = \|Q\|` | Number of exact quotient classes | Exact only when `Q` is replayably enumerated; otherwise use an estimate with provenance | +| `M_epsilon` | Task-confusability quotient size after merging states whose distinction changes distortion by at most declared `epsilon` under the declared traffic distribution | Distortion, `epsilon`, estimator, sample design, coverage, confidence interval, and tail metric | +| `R_task(D)` | Task rate-distortion target, `min I(X; Z \| Q)`, where `Q` is exact compiler state, `Z` carries only input-conditioned uncertainty, and the minimum ranges over a declared encoder/representation class subject to expected distortion at most `D` | Distribution of `X`, definition of `Z`, fixed `Q`, encoder class, distortion, estimator, and uncertainty | +| `K_z` | Arity of one latent or decision-code coordinate | Coordinate semantics and length `d_z` | +| `K_w` | Number of representable weight levels after any grouping/scaling | Group size, scale/zero representation, exceptions, and packing | +| `K_a` | Number of representable activation levels | Tensor sites, calibration, clipping, accumulation precision, and kernel | +| `K_E` | Number of representable energy/output-score levels | Scored sites, calibration, numeric format, and decision rule | +| `K_code` | Alphabet size of an explicit error-control code | Code length `d_code`, minimum distance, channel/noise model, encoder, and decoder | +| physical cost | Packed weights/codes plus scales, zero points, masks, norms, indexes, alignment, activations, unpack/routing work, latency, memory traffic, and energy | Hardware, kernel, batch/shape, packing format, accounting scope, and measurement protocol | + +The current [`semantic_bits.py`](../../src/slm_training/evals/semantic_bits.py) +computes an empirical corpus-unigram description length for production, choice, +and surface streams. It is useful telemetry but is neither `M_epsilon` nor +`R_task(D)`: it does not condition on `Q`, impose a distortion constraint, declare +an encoder class, or supply coverage, confidence, and tail guarantees. + +## Guarantee boundary + +The compiler and verified-scope solver own guarantees. Learned modules remain +subordinate: + +| Layer | Allowed authority | Forbidden inference | +| --- | --- | --- | +| Compiler / pack | Define hard legality and current next-action membership under declared pack capabilities | A `well_formed_not_behavioral` oracle cannot prove behavior | +| Verified Scope | Prove bounded completion support, carry replayable proof evidence, and authorize destructive removal | `UNKNOWN`, timeout, partial coverage, or a stale version cannot remove a candidate | +| Learned ranker / uncertainty model | Rank live members, estimate uncertainty, propose reversible decisions, or request more compute | A score, margin, low entropy, or latent code never creates legality or proves support | +| Realizer | Fill fields classified surface-only against fixed AST/choice IR, then canonicalize and run the applicable pack oracle | It may not autoregress semantic structure or bypass final verification | + +[`CompletionForest`](../../src/slm_training/dsl/grammar/fastpath/compiler_draft.py) +is currently a bounded next-decision projection, not an enumerated and minimized +global `Q`. Likewise, +[`RankedForest.signature`](../../src/slm_training/dsl/grammar/fastpath/lattice_search.py) +hashes coverage and token paths for search telemetry; it omits the full frame and +is not a CAP state signature or proof. CAP does not duplicate the support solver: +feasibility, the support oracle, proof-carrying refinement, and the irreversible +guarantee boundary are owned by the Verified Scope contract. + +## Exact finite-state capacity + +For a declared exact quotient `Q` with `M = |Q|`, a fixed-length noiseless code of +length `d` over an alphabet of size `K` can injectively name all states iff +`K^d >= M`. This is a cardinality fact only. It says nothing about task distortion, +learnability, geometry, error robustness, packed cost, or a neural optimum. + +The preregistered noiseless capacity comparator is `(K_z=2, d_z=6)` versus +`(K_z=3, d_z=4)` for the same exact `M=41` quotient, fixed bounded frame, zero +symbol errors, exact enumeration, and ideal dense symbol packing reported +separately from physical bytes. Both have enough names (`64` versus `81`). Neither +is called optimal until matched semantic-quality and physical-cost studies run. + +## Corrected one-substitution baseline + +Here `M=41` messages, code length `d`, alphabet `K_code`, and one arbitrary symbol +substitution require minimum Hamming distance at least three. These rows are exact +coding statements under that channel, not model or deployment results. + +| State set / task quotient and bounds | `K_code`, `d_code`, noise, exact status | Result and construction / proof | +| --- | --- | --- | +| Fixed exact 41-message set; no AST semantics beyond its declared enumeration | `K_code=6`, `d_code=4`; one substitution; exact; packing not claimed | **Impossible.** Singleton gives `M <= K_code^(d_code-3+1) = 6^2 = 36 < 41`. The former robust arm `(6,4)` is deleted. | +| Same fixed exact 41-message set | `K_code=7`, `d_code=4`; one substitution; exact; packing not claimed | **Sufficient.** The `[4,2,3]_7` MDS code generated by rows `(1,1,1,1)` and `(0,1,2,3)` has 49 words; any 41-word subset retains distance at least three. | +| Same fixed exact 41-message set | `K_code=3`, `d_code=6`; one substitution; exact computer-assisted coding bound; packing not claimed | **Impossible.** The published exhaustive classification establishes `A_3(6,3) <= 39`; its provenance is required because Singleton alone is insufficient. The former robust arm `(3,6)` is deleted. | +| Same fixed exact 41-message set | `K_code=3`, `d_code=7`; one substitution; exact; packing not claimed | **Sufficient.** A shortened ternary Hamming `[7,4,3]_3` code has 81 words. One parity-check matrix has columns `(1,0,0),(0,1,0),(0,0,1),(1,1,0),(1,0,1),(0,1,1),(1,1,1)` over `F_3`; pairwise non-proportional columns exclude weights 1 and 2, and `(1,0,0)+(0,1,0)-(1,1,0)=0` supplies weight 3. Select any 41 words. This code is not MDS. | + +The `d=6` impossibility relies on a computer-assisted small-alphabet-code result, +not an elementary analytic bound. Replay must retain the cited theorem and its +provenance; the repository does not currently carry an independent exhaustive +enumerator. + +## Boundary predicates and ternary-specific claims + +### Strict margin plane + +For a declared fixed geometric ternary residual with `R` digits, bounded aggregate +error `E_max`, and decision margin `gamma` expressed in the same exact integer +units, the admissible sufficient condition is strictly + +`E_max / (3^R - 1) < gamma / 2`. + +Implementations must compare the division-free integer predicate +`2 * E_max < gamma * (pow(3, R) - 1)`. Equality fails. Do not derive the boundary +through floating logarithms or rounded powers; the earlier exact-power boundary bug +came from doing so. Learned scales or non-integer units require an empirical margin +distribution with numeric-error provenance, not this exact predicate. + +### Ternary ECOC + +For `b` labels, an injective base-3 label needs `ceil(log_3 b)` trits but has no +error-detection guarantee. Append one mod-3 parity trit, giving +`m = ceil(log_3 b) + 1`; then every one-trit substitution violates parity and the +code has minimum distance at least two. This detects one substitution; it does not +correct one. Correction requires minimum distance at least three and the robust +coding table above. + +### Balanced ternary + +`R` balanced ternary digits with the exact geometric place values +`1, 3, ..., 3^(R-1)` represent exactly `3^R` consecutive integer states. That +cardinality guarantee does not transfer to learned, repeated, zero, unordered, or +otherwise non-geometric scales. Learned scales must report empirical collision, +coverage, reconstruction, margin, and tail-error results; they do not inherit a +`3^R` state guarantee. + +## Evidence and certificate ledger + +The word **certificate** is reserved for replayable exact evidence or an explicitly +statistical certificate whose estimator, uncertainty, and provenance are recorded. +A teacher margin, low-rank diagnostic, or point estimate is not an exact +certificate. + +| Claim class | Exact replay record | Estimated / statistical record | +| --- | --- | --- | +| State count / quotient | Pack, grammar, parser, codec, and state-signature versions; AST/depth/scope/cutoff bounds; canonical states; equivalence procedure; completeness proof; work count; digest | Trace/data IDs; sample design and `n`; coverage; estimator; confidence interval; collision/tail metric; code/checkpoint digest | +| Code capacity / robustness | Message set digest; `K_code`, `d_code`, encoder/decoder; minimum-distance proof or replay; channel model; construction/theorem provenance | Sampled corruption design; seeds and `n`; decoder; error-rate estimate and interval; worst observed tail, explicitly not exhaustive | +| Task quotient / rate | Exact distribution and distortion table, fixed `Q`, declared encoder class, exhaustive optimizer and replay | Traffic distribution/version; distortion and `epsilon`/`D`; estimator; held-out design; interval; coverage and tail error | +| Margin boundary | Exact integer units; geometric scales; `R`; exhaustive `E_max`; strict integer predicate replay | Checkpoint/data IDs; margin/error estimator; calibration split; interval and quantiles; numeric precision | +| Physical cost | Exact format layout and byte accounting for a fixed shape, including metadata/alignment | Hardware/software/kernel versions; warmup/repeats; batch/shape; latency/memory/energy distribution and interval | + +Every exact record must name the property tier it establishes. Every statistical +record must remain statistical. Pack-oracle labels are limited to the capability +declared by the pack; syntax success is not meaningful-parse or ship evidence. + +## Fair comparator contract + +Later experiments must keep each question separate: + +1. **Noiseless requirement-matched capacity:** compare `(K_z=2,d_z=6)` with + `(K_z=3,d_z=4)` on the same exact 41-state quotient and bounded frame. +2. **Robust requirement-matched capacity:** compare valid arms such as + `(K_code=7,d_code=4)` and `(K_code=3,d_code=7)` under the same one-substitution channel; + never resurrect `(6,4)` or `(3,6)`. +3. **Equal nominal rate:** match `d * log2(K)` before metadata, and label this an + analytic ideal-rate study. +4. **Equal physical bytes:** match the full stored and live-memory ledger. This is + a distinct study; padding, scales, masks, and kernel layout count. +5. **Representation controls:** include optimized four-level-with-zero, symmetric + four-level, binary-plus-mask, and continuous/soft latent controls beside ternary. + +Across trained arms, match activation precision, group size, calibration/adaptation +data, data order, optimizer steps/tokens, seeds, model shape, compiler frame, and +kernel implementation. If a factor cannot be matched, isolate it as a named +ablation. Report syntax only as diagnostic; meaningful parse and the unchanged +multi-suite ship gates remain primary, with latency, memory, and energy reported by +the performance matrix. Nominal rate and equal physical bytes must never be pooled +into one winner. + +## Hypothesis ledger + +IDs are permanent and must not be reused. A later result appends a verdict rather +than rewriting the prediction or falsifier. + +| ID | Operational prediction | Falsifier | Comparator contract and required metrics | +| --- | --- | --- | --- | +| `CAP-H1` | A compiler-owned exact state plus a local legal-action scorer reaches matched semantic quality with fewer learned parameters and lower precision than implicit grammar-state inference. | Implicit state tracking is equal or better after matched state information and deployed cost. | Explicit-`Q` vs implicit-history models; match data/order/steps/shape/kernel; meaningful parse, regret among legal ASTs, parameters, `K_z/K_w/K_a/K_E`, bytes, latency, seeds. | +| `CAP-H2` | `R_task(D)` or `M_epsilon` predicts the latent-capacity phase boundary better than raw `log2(M)`. | Raw exact-state count remains the strongest held-out predictor after action entropy, semantic regret, and margin are controlled. | Same exact `Q`, traffic and model ladder; raw count vs task-rate estimators; meaningful parse, distortion, regret, coverage, confidence and tail errors. | +| `CAP-H3` | An unrestricted optimized four-level-with-zero representation matches or beats ternary at equal physical storage; any ternary win is due to optimization, regularization, entropy, zero support, or execution rather than reconstruction capacity. | Repeated matched runs show ternary strictly superior outside the preregistered equivalence interval. | Ternary, optimized four-level-with-zero, symmetric four-level, binary+mask, continuous/soft; match bytes/calibration/steps/activations/groups/kernel; meaningful parse, gates, latency, energy, seeds. | +| `CAP-H4` | Grammar-stratified calibration by state/action/scope/margin/timestep outperforms random calibration at the same sample count. | Random calibration is indistinguishable after repeated seeds and coverage controls. | Same checkpoint, `n`, quantizer, groups, activations and kernel; meaningful parse/gates, regret, calibration error, state/action coverage, worst-case/tail error. | +| `CAP-H5` | At equal packed bytes, a slightly wider ternary/two-bit model recovers more semantic quality than a narrower high-precision model. | Quality stays precision-dominated and does not recover with width under equal packed bytes and latency. | Width-by-precision frontier with matched data/order/steps and physical ledger; meaningful parse/gates, parameters, bytes, peak memory, latency, energy, seeds. | +| `CAP-H6` | Hybrid precision—low-bit bulk blocks with INT4/INT8 task-sensitive plan projections, state updates, or local heads—improves the quality-cost frontier over uniform ternary. | Sensitivity is broadly distributed and no hybrid schedule improves the replicated frontier. | Uniform vs sensitivity-guided schedules; same checkpoint/data/groups/kernel/budget; per-layer `K_w/K_a/K_E`, meaningful parse/gates, loss, bytes, latency, energy. | +| `CAP-H7` | Runtime posterior entropy, top-two margin, or conditioned sensitivity routes refinement better than raw branching, reducing average compute over structural-state-only routing. | Structural state alone predicts required planes and learned/runtime routing adds only overhead or changes verified outcomes beyond tolerance. | Same compiler/support oracle/ranker; reversible routing only; meaningful parse/gates, verified terminals, `UNKNOWN` rate, planes/nodes/verifier calls, mean/tail latency, seeds. | +| `CAP-H8` | Compiler-aligned deterministic block activation or state-routed micro-experts gives larger measured speedups than incidental unstructured ternary zero-skipping. | Dispatch, batching, or memory overhead removes the speed/energy benefit at matched quality. | Structured routing vs unstructured zero-skip and dense controls; same bytes/quality target/kernel family; meaningful parse/gates, utilization, traffic, latency distribution, energy. | +| `CAP-H9` | Typed-hole or exact-quotient-state corruption reduces invalid-state work only when the quotient graph retains adequate connectivity, conductance, and posterior support. | Graph bottlenecks or information loss require more steps or a larger denoiser than matched AST-subtree corruption. | Quotient-state vs AST-subtree diffusion; same data/model/steps/compute; graph connectivity/conductance/support, invalid work, denoise steps, meaningful parse/gates, bytes, latency. | + +`CAP-H3` tests whether an optimized four-level control explains an apparent ternary +effect. Repeated ternary superiority is its falsifier, not its confirmation. No +ledger row asserts general ternary optimality. + +## Physical-cost ledger + +Every cost table has two non-interchangeable columns: + +- **analytic ideal packing:** `N * log2(K)` or the specified dense-code formula, + with state/task quotient, all `K,d` roles, bounds, and noise model in the row; +- **measured physical system:** packed payload plus scale/bias/zero-point/norm/mask, + indexes and alignment, activation and accumulator storage, unpack/dequant work, + memory traffic, routing/verifier work, latency, and energy on a named kernel and + device. + +An ideal packing win is not a deployed-system win. A deployed optimum is local to +the stated hardware, shapes, traffic, quality constraints, compiler frame, and +packing implementation. + +## Source review and corrections (2026-07-17) + +The project review covered the Linear documents derived from the user-supplied +artifacts named `Kimi_Agent_Kimi CLI Context Issue.zip` and `Pasted text(6).txt` +(Grok follow-up). This repository paraphrases their conclusions; it does not copy +private source text. + +The condensed Kimi document source-reports an independent reproduction over 27 +quantitative claim classes and 19 demo outputs: 130 bounded ASTs, 351 trie states, +41 minimized states, decision histograms of 162/190/345, exact Hankel rank 40, and +99%-energy rank 32. The typing-rule variant, executable, signature frame, and +checksum needed to replay those numbers are absent from Linear. They are therefore +**source-reported estimates/evidence, not repository certificates**. The raw +86-state claim was not reproduced; this does not by itself invalidate the reported +downstream 41-state calculation, but blocks reuse as an exact local baseline. + +Corrections adopted here: + +- separate exact state capacity, task rate, neural precision, and deployment cost; +- replace infeasible robust `(6,4)` and `(3,6)` arms with proven sufficient + `(7,4)` and `(3,7)` arms; +- attribute ternary length-six impossibility to the computer-assisted + small-alphabet classification, not Singleton; +- use a strict division-free integer margin predicate and distinguish geometric + balanced-ternary guarantees from learned-scale estimates; +- require distance two plus parity only for one-error detection, and distance + three for one-error correction; +- correct `CAP-H3` polarity and keep nominal-rate and equal-physical-byte studies + separate. + +Primary sources and transfer boundaries are catalogued in +[research-lineage.md](research-lineage.md). In particular, quantization results on +large pretrained models, latent-image codecs, and automata over restricted algebras +do not establish a local OpenUI optimum. + +## Implementation note (2026-07-17) + +SLM-77 commits this architecture, claim, and hypothesis contract only. No train, +eval, benchmark, matrix, profile, telemetry, or reproduction run occurred; no +result JSON, AgentV bundle, model-card update, or checkpoint is warranted. Future +runs must use the existing quality/performance matrices, preserve meaningful parse +as the primary metric, retain unchanged ship gates, and document even negative or +partial results under `docs/design/`. diff --git a/docs/design/research-lineage.md b/docs/design/research-lineage.md index 69655f7d..5c726fb6 100644 --- a/docs/design/research-lineage.md +++ b/docs/design/research-lineage.md @@ -568,6 +568,34 @@ markers + deterministic identifier/macro expansion + canonicalizing denoiser, measured by bits-per-semantic-decision. No novelty is claimed until matched local runs exist. +## Calculated arity and adaptive precision (CAP0) + +[calculated-arity-adaptive-precision.md](calculated-arity-adaptive-precision.md) +is the specification-only contract separating exact symbolic capacity, +task-relevant rate, neural precision, and measured deployment cost. SLM-77 runs no +experiment and implements none of the mechanisms below, so all new anchors are +**Adjacent**. Grammar-Aligned Decoding and Diffusion on Syntax Trees retain their +existing A2/X22 fidelity records above; their inclusion here is a cross-reference, +not a second or stronger implementation claim. + +| Paper / result | Fidelity | CAP use and transfer boundary | +| --- | --- | --- | +| Ma et al., [*The Era of 1-bit LLMs: All Large Language Models are in 1.58 Bits*](https://arxiv.org/abs/2402.17764) (BitNet b1.58) | **Adjacent** | Native ternary weight training motivates a `K_w=3` control. It does not show that post-hoc choice codes or latent quantizers preserve this tiny OpenUI model. | +| Liu et al., [*ParetoQ: Scaling Laws in Extremely Low-bit LLM Quantization*](https://arxiv.org/abs/2502.02631) | **Adjacent** | Its unified low-bit QAT comparison motivates matched bit-width controls. Its empirical transition between at-most-two and at-least-three bits is model/recipe specific and does not transfer locally. | +| Wang et al., [*CAT-Q: Cost-efficient and Accurate Ternary Quantization for LLMs*](https://arxiv.org/abs/2606.26650) | **Adjacent** | Learnable modulation and softened ternarization motivate a ternary PTQ control distinct from native training. Large-model/calibration results do not establish local arity or system optima. | +| Mentzer et al., [*Finite Scalar Quantization: VQ-VAE Made Simple*](https://arxiv.org/abs/2309.15505) | **Adjacent** | Product scalar grids motivate explicit `K_z,d_z` accounting. FSQ is a latent quantizer, not an error-correcting code or weight-PTQ result. | +| Zhu et al., [*Robust Residual Finite Scalar Quantization for Neural Compression*](https://arxiv.org/abs/2508.15860) | **Adjacent** | Learned scaling and invertible normalization motivate a residual-scale control. Audio/image neural-compression evidence does not establish an OpenUI rate-distortion gain. | +| Dong et al., [*HAWQ-V2*](https://arxiv.org/abs/1911.03852) | **Adjacent** | Hessian-trace sensitivity and Pareto allocation motivate `CAP-H8`. They do not prove an optimal local `K_w`, `K_a`, or semantic-quality frontier. | +| Maletti, [*Minimizing deterministic weighted tree automata*](https://doi.org/10.1016/j.ic.2009.01.004); Rabusseau et al., [*Low-Rank Approximation of Weighted Tree Automata*](https://arxiv.org/abs/1511.01442) | **Adjacent** | Exact minimization over deterministic WTA and approximate Hankel/SVD reduction motivate keeping exact `Q` separate from estimated task compression. Their algebraic assumptions do not automatically cover this compiler, CFG, or learned score algebra. | +| Shin et al., [*Grammar-Aligned Decoding*](https://arxiv.org/abs/2405.21047) | Existing **Adapted** A2 boundary | The existing ASAp transplant concerns positionwise constraint-mass removal. It supplies no convergence, exact quotient, or precision optimum here. | +| Kapur et al., [*Diffusion on Syntax Trees*](https://arxiv.org/abs/2405.20519) | Existing **Faithful (mechanism)** X22 boundary | The tree-edit mechanism and its missing rendered-observation half remain recorded above. Tree arity does not imply weight, activation, or deployment arity. | +| Bogdanova and Kapralov, [*Bounds for Codes over Small Alphabets*](https://www.math.bas.bg/smb/2000_PK/tom_2000/pdf/149-154.pdf) | **Adjacent theorem provenance** | The computer-assisted `A_3(6,3) <= 39` bound proves the 41-message ternary length-six robust arm infeasible. It is a coding bound, not model evidence or a general ternary-optimality result. | + +No paper in this table supplies a model, checkpoint, local benchmark result, or +ship evidence. Future CAP rows must use meaningful parse as primary quality, +retain frozen multi-suite gates, and measure physical packing/kernel costs rather +than infer them from nominal arity. + ## Autoresearch systems and adjacent research directions ### Swappable deep-research systems From 70ba8b7ba38c0990bc375915ea08d4b7552c26b4 Mon Sep 17 00:00:00 2001 From: Tyler Kendrick <145080887+Tyler-R-Kendrick@users.noreply.github.com> Date: Fri, 17 Jul 2026 16:20:38 -0500 Subject: [PATCH 3/9] Add finite-domain support lattice --- docs/design/verified-scope-solver.md | 60 ++- src/slm_training/dsl/solver/__init__.py | 27 ++ src/slm_training/dsl/solver/adapters.py | 90 +++++ src/slm_training/dsl/solver/state.py | 467 ++++++++++++++++++++++++ tests/test_dsl/test_solver_state.py | 362 ++++++++++++++++++ 5 files changed, 1000 insertions(+), 6 deletions(-) create mode 100644 src/slm_training/dsl/solver/__init__.py create mode 100644 src/slm_training/dsl/solver/adapters.py create mode 100644 src/slm_training/dsl/solver/state.py create mode 100644 tests/test_dsl/test_solver_state.py diff --git a/docs/design/verified-scope-solver.md b/docs/design/verified-scope-solver.md index f0556472..dcc2e585 100644 --- a/docs/design/verified-scope-solver.md +++ b/docs/design/verified-scope-solver.md @@ -46,8 +46,8 @@ transitions without inventing semantics. - **`HoleId`** — stable identifier for a single unresolved decision site in the program IR (a position that must be filled by a choice/subtree). Stable across - reversible search so certificates and nogoods can reference it. New symbol - (absent today). + reversible search so certificates and nogoods can reference it. Implemented by + VSS0-03 in `dsl/solver/state.py`. - **finite domain** — the declared, bounded set of candidate fillings for a `HoleId` under the current pack/compiler coverage. Finiteness within declared bounds is a precondition for exact closure; a domain not provably finite within @@ -116,6 +116,44 @@ transitions without inventing semantics. permitted, subject to canonicalization plus the applicable pack oracle afterward. +## Implemented finite-domain state (VSS0-03 / SLM-59) + +[`dsl/solver/`](../../src/slm_training/dsl/solver/) now implements the Torch-free, +model-independent hard-state carrier. It is not invoked by decode by default. + +| Type / operation | Implemented contract | +| --- | --- | +| `HoleId` | Immutable namespace, mixed string/integer path, and kind; ordered by tagged canonical JSON rather than unsafe raw mixed-type tuple comparison. | +| `SolverBounds` | Non-negative token, node, depth, backtrack, and verifier-call bounds; every field participates in hard-state identity. | +| `DomainValue` | A tag plus immutable canonical JSON text. `to_dict` exposes ordinary tagged JSON while construction rejects objects, non-string object keys, and non-finite floats. | +| `HoleDomain` | Unique values and scalar metadata, both canonically ordered. An empty domain is bottom. | +| `FiniteDomainState` | Unique canonically ordered holes; monotone `refine`, domain-wise `meet`, reversible `with_decision`, stable JSON round-trip, and compact numeric summary. | +| `completion_forest_state` | Projects exactly one current compiler decision. Values preserve each full `CompletionPath.token_ids` plus `kind`; metadata preserves `coverage` and global support remains `UNKNOWN`. | + +The full SHA-256 fingerprint includes `problem_id`, `pack_id`, constraint version, +bounds, hole IDs, domain values, and hard scalar metadata. It excludes model +logits/scores, timestamps, process IDs, mutable caches, certificate references, and +reversible search lineage (`decision_level` / `parent_fingerprint`). Thus two +search trails reaching the same hard domains share an identity. A decision records +the prior fingerprint as its parent but never changes `UNKNOWN` into +`UNSUPPORTED`. + +`refine` accepts a forward-compatible `certificate_ref` argument but does not +persist it yet: certificate schema, checking, and replay belong to VSS0-04. Meet +requires identical problem/pack/constraint/bounds identity, the same hole IDs, and +type-preserving matching metadata rather than inventing a merge rule. Because meet +can combine unrelated reversible trails, it explicitly resets decision lineage to +level zero with no parent. All mutation-like operations return new validated +states; none embeds soft scores. + +The compiler adapter deliberately ignores any optional explanation evidence added +by VSS0-02. Considered-candidate evidence is provenance, not an exhaustive support +proof. Empty forest paths produce bottom. A singleton forest is structurally solved +**only for that next-decision projection**; it is not a globally solved program, +verified terminal, `SUPPORTED` claim, correctness gain, or ship claim. The +`TopologyDomainAdapter` protocol is only a future model-independent seam and imports +no model or Torch code. + ## Reference support semantics | Verdict | Requirement | Removal permitted? | @@ -228,7 +266,9 @@ the closure. | `ScopeContract` / `ScopeKind` (`data/progspec/scopes.py:33`/`:18`) | AST scopes (`COMPONENT_CALL`/`STATEMENT`/`CHILD_LIST`) plus a def/use binder overlay (`definitions`/`uses`/`visible_binders`). | **Extended.** Scope def/use edges feed capsule SCC construction; scopes are **not** assumed independent. | | `dependency_closed_failure_cone` (`data/progspec/scopes.py:113`) | Despite the name, computes the least-common-ancestor of failing AST paths — **not** a dependency closure or SCC. | **Not reused for capsules.** Capsule SCCs are a new, distinct construction; this contract does not duplicate or overload this helper. | | `ChoiceTokenizer` / `ChoiceDecodeState` (`models/choice_tokenizer.py:172`/`:608`) | Grammar-closed choice IR; length-aware legality (`allowed_ids`, `exhaustive_allowed_ids`, `minimal_completion_length`). | **Retained.** The choice IR is the late-realization and verification surface. Not duplicated. | -| `HoleId`, finite `domain`, `verification capsule`, `proof certificate` | Absent today (confirmed greenfield). | **New** dataclasses/semantics introduced by later VSS issues under this contract. | +| `HoleId`, `SolverBounds`, `DomainValue`, `HoleDomain`, `FiniteDomainState` (`dsl/solver/state.py`) | Immutable JSON-safe finite-domain carrier with canonical hard-state identity and monotone operations. | **Implemented by VSS0-03.** Torch-free and not invoked by default; soft scores and proof artifacts remain outside the state. | +| `completion_forest_state` (`dsl/solver/adapters.py`) | One-hole projection of full compiler completion paths plus coverage and `UNKNOWN` provenance. | **Implemented by VSS0-03.** Retains the compiler as owner; a singleton solves only the projection. | +| `verification capsule`, `proof certificate` | Not implemented yet. | **Future VSS issues.** Capsule solving and replayable proof ownership are not duplicated here. | ## End-to-end example (partial coverage → live `UNKNOWN`) @@ -298,6 +338,14 @@ the X16-X21 convention ("lineage labels, not reproduced results"). runtime dependency, no experiment, no checkpoint, and no eval run; therefore no measured results and **no model or ship claim**. This document defines the guarantee boundary only. `python -m scripts.repo_policy` passes; documentation -changes select no test suites (`scripts/check_changed` skips `docs/`). Later VSS -issues implement the dataclasses and state transitions specified here behind a -feature flag before any decode-behavior change. +changes select no test suites (`scripts/check_changed` skips `docs/`). VSS0-03 now +implements the carrier without decode integration; later VSS issues add proof and +search behavior behind a feature flag before any decode-behavior change. + +2026-07-17 — VSS0-03 / SLM-59 implements the Torch-free finite-domain state, +canonical SHA-256 identity, monotone refinement/meet, reversible decision lineage, +compiler projection adapter, JSON round-trip, and focused regression coverage. It +does not implement recursive support search, a proof checker, capsule solving, +decode integration, or model scoring. No train, eval, benchmark, checkpoint, or +experiment ran; this is infrastructure only and makes **no correctness, readiness, +or ship claim**. diff --git a/src/slm_training/dsl/solver/__init__.py b/src/slm_training/dsl/solver/__init__.py new file mode 100644 index 00000000..c4b50aed --- /dev/null +++ b/src/slm_training/dsl/solver/__init__.py @@ -0,0 +1,27 @@ +"""Torch-free finite-domain support-lattice primitives.""" + +from slm_training.dsl.solver.adapters import ( + TopologyDomainAdapter, + completion_forest_state, +) +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleDomain, + HoleId, + JsonScalar, + SolverBounds, + SupportVerdict, +) + +__all__ = [ + "DomainValue", + "FiniteDomainState", + "HoleDomain", + "HoleId", + "JsonScalar", + "SolverBounds", + "SupportVerdict", + "TopologyDomainAdapter", + "completion_forest_state", +] diff --git a/src/slm_training/dsl/solver/adapters.py b/src/slm_training/dsl/solver/adapters.py new file mode 100644 index 00000000..bd1c9f0f --- /dev/null +++ b/src/slm_training/dsl/solver/adapters.py @@ -0,0 +1,90 @@ +"""Narrow Torch-free projections into the finite-domain solver state.""" + +from __future__ import annotations + +import hashlib +import json +from typing import Protocol, TypeVar + +from slm_training.dsl.grammar.fastpath.compiler_draft import CompletionForest +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleDomain, + HoleId, + SolverBounds, + SupportVerdict, +) + + +TopologyNodeT = TypeVar("TopologyNodeT") + + +class TopologyDomainAdapter(Protocol[TopologyNodeT]): + """Future model-independent seam for bounded topology-domain projections.""" + + def domain_for( + self, node: TopologyNodeT, *, bounds: SolverBounds + ) -> HoleDomain: + """Project one bounded topology node without model scores.""" + ... + + +def completion_forest_state( + *, + prefix_ids: tuple[int, ...] | list[int], + forest: CompletionForest, + pack_id: str, + constraint_version: str, + bounds: SolverBounds, +) -> FiniteDomainState: + """Project the current next compiler decision, not a globally solved program.""" + if any( + isinstance(token_id, bool) or not isinstance(token_id, int) or token_id < 0 + for token_id in prefix_ids + ): + raise ValueError("completion-forest prefix_ids must be non-negative integers") + if forest.coverage not in {"complete", "partial", "none"}: + raise ValueError("completion-forest coverage must be complete, partial, or none") + for path in forest.paths: + if not isinstance(path.kind, str) or not path.kind: + raise ValueError("completion-forest path kind must be non-empty text") + if any( + isinstance(token_id, bool) + or not isinstance(token_id, int) + or token_id < 0 + for token_id in path.token_ids + ): + raise ValueError( + "completion-forest path token_ids must be non-negative integers" + ) + prefix = tuple(prefix_ids) + payload = json.dumps(prefix, separators=(",", ":")) + prefix_sha = hashlib.sha256(payload.encode()).hexdigest() + hole_id = HoleId( + namespace="completion_forest", + path=(len(prefix), prefix_sha), + kind="next_semantic_decision", + ) + values = tuple( + DomainValue.create( + "completion_path", + {"kind": path.kind, "token_ids": list(path.token_ids)}, + ) + for path in forest.paths + ) + domain = HoleDomain( + hole_id=hole_id, + values=values, + metadata=( + ("coverage", forest.coverage), + ("support_verdict", SupportVerdict.UNKNOWN.value), + ), + ) + return FiniteDomainState( + problem_id=f"completion-forest:{prefix_sha}", + pack_id=pack_id, + constraint_version=constraint_version, + bounds=bounds, + holes=(domain,), + ) diff --git a/src/slm_training/dsl/solver/state.py b/src/slm_training/dsl/solver/state.py new file mode 100644 index 00000000..0f312d2c --- /dev/null +++ b/src/slm_training/dsl/solver/state.py @@ -0,0 +1,467 @@ +"""Torch-free finite-domain state for bounded verified synthesis. + +The semantics and fingerprint exclusions are owned by +``docs/design/verified-scope-solver.md``. +""" + +from __future__ import annotations + +import hashlib +import json +import math +from dataclasses import dataclass, replace +from enum import Enum +from functools import total_ordering +from typing import Any, Iterable, TypeAlias + +JsonScalar: TypeAlias = str | int | float | bool | None + + +def _canonical_json(value: Any) -> str: + return json.dumps( + value, + allow_nan=False, + ensure_ascii=False, + separators=(",", ":"), + sort_keys=True, + ) + + +def _validate_json(value: Any, *, context: str) -> None: + if value is None or isinstance(value, (str, bool, int)): + return + if isinstance(value, float): + if not math.isfinite(value): + raise ValueError(f"{context} contains a non-finite float") + return + if isinstance(value, (list, tuple)): + for item in value: + _validate_json(item, context=context) + return + if isinstance(value, dict): + for key, item in value.items(): + if not isinstance(key, str): + raise ValueError(f"{context} object keys must be strings") + _validate_json(item, context=context) + return + raise ValueError(f"{context} is not JSON-safe: {type(value).__name__}") + + +def _require_text(value: Any, *, field: str, context: str) -> str: + if not isinstance(value, str) or not value: + raise ValueError(f"{context} requires a non-empty {field}") + return value + + +def _strict_fields(data: dict[str, Any], expected: set[str], *, context: str) -> None: + unknown = set(data) - expected + missing = expected - set(data) + if unknown or missing: + raise ValueError( + f"{context} fields mismatch: missing={sorted(missing)}, " + f"unknown={sorted(unknown)}" + ) + + +class SupportVerdict(str, Enum): + """Bounded support result; ``UNKNOWN`` never licenses candidate removal.""" + + SUPPORTED = "supported" + UNSUPPORTED = "unsupported" + UNKNOWN = "unknown" + + +@total_ordering +@dataclass(frozen=True) +class HoleId: + """Stable identity for one unresolved semantic decision site.""" + + namespace: str + path: tuple[str | int, ...] + kind: str + + def __post_init__(self) -> None: + context = f"hole {self.namespace!r}/{self.kind!r}" + _require_text(self.namespace, field="namespace", context=context) + _require_text(self.kind, field="kind", context=context) + normalized: list[str | int] = [] + for part in self.path: + if isinstance(part, bool) or not isinstance(part, (str, int)): + raise ValueError( + f"{context} path entries must be strings or integers" + ) + normalized.append(part) + object.__setattr__(self, "path", tuple(normalized)) + + @property + def sort_key(self) -> str: + return _canonical_json(self.to_dict()) + + def __lt__(self, other: object) -> bool: + if not isinstance(other, HoleId): + return NotImplemented + return self.sort_key < other.sort_key + + def to_dict(self) -> dict[str, Any]: + return { + "namespace": self.namespace, + "path": list(self.path), + "kind": self.kind, + } + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> HoleId: + _strict_fields(data, {"namespace", "path", "kind"}, context="HoleId") + path = data["path"] + if not isinstance(path, list): + raise ValueError("HoleId path must be a JSON array") + return cls( + namespace=data["namespace"], + path=tuple(path), + kind=data["kind"], + ) + + +@dataclass(frozen=True) +class SolverBounds: + """Finite resource bounds that participate in solver-state identity.""" + + max_tokens: int + max_nodes: int + max_depth: int + max_backtracks: int + max_verifier_calls: int + + def __post_init__(self) -> None: + for field, value in self.to_dict().items(): + if isinstance(value, bool) or not isinstance(value, int) or value < 0: + raise ValueError(f"solver bounds require non-negative {field}") + + def to_dict(self) -> dict[str, int]: + return { + "max_tokens": self.max_tokens, + "max_nodes": self.max_nodes, + "max_depth": self.max_depth, + "max_backtracks": self.max_backtracks, + "max_verifier_calls": self.max_verifier_calls, + } + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> SolverBounds: + expected = { + "max_tokens", + "max_nodes", + "max_depth", + "max_backtracks", + "max_verifier_calls", + } + _strict_fields(data, expected, context="SolverBounds") + return cls(**{field: data[field] for field in expected}) + + +@dataclass(frozen=True, order=True) +class DomainValue: + """A tagged JSON value stored as immutable canonical JSON text.""" + + tag: str + payload_json: str + + def __post_init__(self) -> None: + _require_text(self.tag, field="tag", context="domain value") + if not isinstance(self.payload_json, str): + raise ValueError(f"domain value {self.tag!r} payload_json must be text") + try: + payload = json.loads(self.payload_json) + except (TypeError, ValueError) as exc: + raise ValueError(f"domain value {self.tag!r} has invalid JSON") from exc + _validate_json(payload, context=f"domain value {self.tag!r}") + object.__setattr__(self, "payload_json", _canonical_json(payload)) + + @classmethod + def create(cls, tag: str, payload: Any) -> DomainValue: + _validate_json(payload, context=f"domain value {tag!r}") + return cls(tag=tag, payload_json=_canonical_json(payload)) + + @property + def payload(self) -> Any: + return json.loads(self.payload_json) + + def to_dict(self) -> dict[str, Any]: + return {"tag": self.tag, "value": self.payload} + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> DomainValue: + _strict_fields(data, {"tag", "value"}, context="DomainValue") + return cls.create(data["tag"], data["value"]) + + +def _normalize_metadata( + metadata: Iterable[tuple[str, JsonScalar]], *, context: str +) -> tuple[tuple[str, JsonScalar], ...]: + rows = tuple(metadata) + keys: set[str] = set() + normalized: list[tuple[str, JsonScalar]] = [] + for row in rows: + if not isinstance(row, tuple) or len(row) != 2: + raise ValueError(f"{context} metadata entries must be key/value tuples") + key, value = row + _require_text(key, field="metadata key", context=context) + if key in keys: + raise ValueError(f"{context} has duplicate metadata key {key!r}") + _validate_json(value, context=f"{context} metadata {key!r}") + if isinstance(value, (list, tuple, dict)): + raise ValueError(f"{context} metadata {key!r} must be a JSON scalar") + keys.add(key) + normalized.append((key, value)) + return tuple(sorted(normalized, key=lambda row: row[0])) + + +@dataclass(frozen=True, eq=False) +class HoleDomain: + """Canonical finite values and epistemic metadata for one hole.""" + + hole_id: HoleId + values: tuple[DomainValue, ...] + metadata: tuple[tuple[str, JsonScalar], ...] = () + + def __post_init__(self) -> None: + if not isinstance(self.hole_id, HoleId): + raise ValueError("hole domain requires a HoleId") + values = tuple(self.values) + if any(not isinstance(value, DomainValue) for value in values): + raise ValueError(f"hole {self.hole_id!r} contains a non-DomainValue") + if len(set(values)) != len(values): + raise ValueError(f"hole {self.hole_id!r} contains duplicate values") + object.__setattr__(self, "values", tuple(sorted(values))) + object.__setattr__( + self, + "metadata", + _normalize_metadata(self.metadata, context=f"hole {self.hole_id!r}"), + ) + + def to_dict(self) -> dict[str, Any]: + return { + "hole_id": self.hole_id.to_dict(), + "values": [value.to_dict() for value in self.values], + "metadata": [[key, value] for key, value in self.metadata], + } + + def __eq__(self, other: object) -> bool: + if not isinstance(other, HoleDomain): + return NotImplemented + return _canonical_json(self.to_dict()) == _canonical_json(other.to_dict()) + + def __hash__(self) -> int: + return hash(_canonical_json(self.to_dict())) + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> HoleDomain: + _strict_fields(data, {"hole_id", "values", "metadata"}, context="HoleDomain") + values = data["values"] + metadata = data["metadata"] + if not isinstance(values, list) or not isinstance(metadata, list): + raise ValueError("HoleDomain values and metadata must be JSON arrays") + return cls( + hole_id=HoleId.from_dict(data["hole_id"]), + values=tuple(DomainValue.from_dict(value) for value in values), + metadata=tuple(tuple(row) for row in metadata), + ) + + +@dataclass(frozen=True) +class FiniteDomainState: + """Canonical hard state; soft scores and proof artifacts live elsewhere.""" + + problem_id: str + pack_id: str + constraint_version: str + bounds: SolverBounds + holes: tuple[HoleDomain, ...] + decision_level: int = 0 + parent_fingerprint: str | None = None + + def __post_init__(self) -> None: + context = f"problem {self.problem_id!r}" + _require_text(self.problem_id, field="problem_id", context=context) + _require_text(self.pack_id, field="pack_id", context=context) + _require_text( + self.constraint_version, field="constraint_version", context=context + ) + if not isinstance(self.bounds, SolverBounds): + raise ValueError(f"{context} requires SolverBounds") + if ( + isinstance(self.decision_level, bool) + or not isinstance(self.decision_level, int) + or self.decision_level < 0 + ): + raise ValueError(f"{context} requires a non-negative decision_level") + if self.parent_fingerprint is not None and ( + not isinstance(self.parent_fingerprint, str) + or len(self.parent_fingerprint) != 64 + or any(char not in "0123456789abcdef" for char in self.parent_fingerprint) + ): + raise ValueError(f"{context} parent_fingerprint must be a SHA-256 hex digest") + holes = tuple(self.holes) + if any(not isinstance(hole, HoleDomain) for hole in holes): + raise ValueError(f"{context} contains a non-HoleDomain") + ids = [hole.hole_id for hole in holes] + if len(set(ids)) != len(ids): + raise ValueError(f"{context} contains duplicate hole IDs") + object.__setattr__(self, "holes", tuple(sorted(holes, key=lambda h: h.hole_id))) + + def _hard_dict(self) -> dict[str, Any]: + return { + "problem_id": self.problem_id, + "pack_id": self.pack_id, + "constraint_version": self.constraint_version, + "bounds": self.bounds.to_dict(), + "holes": [hole.to_dict() for hole in self.holes], + } + + @property + def fingerprint(self) -> str: + """Full SHA-256 over hard state/config, excluding search lineage.""" + return hashlib.sha256(_canonical_json(self._hard_dict()).encode()).hexdigest() + + @property + def is_bottom(self) -> bool: + return any(not hole.values for hole in self.holes) + + @property + def is_structurally_solved(self) -> bool: + return not self.is_bottom and all(len(hole.values) == 1 for hole in self.holes) + + def domain(self, hole_id: HoleId) -> HoleDomain: + for hole in self.holes: + if hole.hole_id == hole_id: + return hole + raise LookupError(f"problem {self.problem_id!r} has no hole {hole_id!r}") + + def refine( + self, + hole_id: HoleId, + retained_values: Iterable[DomainValue], + *, + certificate_ref: str | None = None, + ) -> FiniteDomainState: + """Return a monotone subset; certificate persistence starts in VSS0-04.""" + if certificate_ref is not None and ( + not isinstance(certificate_ref, str) or not certificate_ref + ): + raise ValueError( + f"problem {self.problem_id!r} certificate_ref must be non-empty" + ) + current = self.domain(hole_id) + retained = tuple(retained_values) + if any(not isinstance(value, DomainValue) for value in retained): + raise ValueError( + f"problem {self.problem_id!r} hole {hole_id!r} refinement " + "requires DomainValue candidates" + ) + current_values = set(current.values) + added = [value for value in retained if value not in current_values] + if added: + raise ValueError( + f"problem {self.problem_id!r} hole {hole_id!r} refinement " + "cannot add candidates" + ) + replacement = HoleDomain(hole_id, retained, current.metadata) + holes = tuple(replacement if hole.hole_id == hole_id else hole for hole in self.holes) + return replace(self, holes=holes) + + def meet(self, other: FiniteDomainState) -> FiniteDomainState: + """Intersect corresponding domains without inventing missing-hole semantics.""" + if not isinstance(other, FiniteDomainState): + raise ValueError(f"problem {self.problem_id!r} can meet only another state") + identity = (self.problem_id, self.pack_id, self.constraint_version, self.bounds) + other_identity = ( + other.problem_id, + other.pack_id, + other.constraint_version, + other.bounds, + ) + if identity != other_identity: + raise ValueError(f"problem {self.problem_id!r} cannot meet mismatched identity") + if {hole.hole_id for hole in self.holes} != { + hole.hole_id for hole in other.holes + }: + raise ValueError(f"problem {self.problem_id!r} cannot meet mismatched holes") + domains: list[HoleDomain] = [] + for left in self.holes: + right = other.domain(left.hole_id) + if _canonical_json(left.to_dict()["metadata"]) != _canonical_json( + right.to_dict()["metadata"] + ): + raise ValueError( + f"problem {self.problem_id!r} hole {left.hole_id!r} " + "cannot meet mismatched metadata" + ) + live = set(right.values) + domains.append( + HoleDomain( + left.hole_id, + tuple(value for value in left.values if value in live), + left.metadata, + ) + ) + return FiniteDomainState( + problem_id=self.problem_id, + pack_id=self.pack_id, + constraint_version=self.constraint_version, + bounds=self.bounds, + holes=tuple(domains), + ) + + def with_decision(self, hole_id: HoleId, value: DomainValue) -> FiniteDomainState: + """Choose one live value reversibly without claiming proof.""" + refined = self.refine(hole_id, (value,)) + return replace( + refined, + decision_level=self.decision_level + 1, + parent_fingerprint=self.fingerprint, + ) + + def summary(self) -> dict[str, int | float | bool]: + sizes = [len(hole.values) for hole in self.holes] + total = sum(sizes) + return { + "hole_count": len(sizes), + "unresolved_count": sum(size != 1 for size in sizes), + "total_candidate_count": total, + "max_domain_size": max(sizes, default=0), + "mean_domain_size": total / len(sizes) if sizes else 0.0, + "is_bottom": self.is_bottom, + "is_structurally_solved": self.is_structurally_solved, + } + + def to_dict(self) -> dict[str, Any]: + return { + **self._hard_dict(), + "decision_level": self.decision_level, + "parent_fingerprint": self.parent_fingerprint, + } + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> FiniteDomainState: + expected = { + "problem_id", + "pack_id", + "constraint_version", + "bounds", + "holes", + "decision_level", + "parent_fingerprint", + } + _strict_fields(data, expected, context="FiniteDomainState") + holes = data["holes"] + if not isinstance(holes, list): + raise ValueError("FiniteDomainState holes must be a JSON array") + return cls( + problem_id=data["problem_id"], + pack_id=data["pack_id"], + constraint_version=data["constraint_version"], + bounds=SolverBounds.from_dict(data["bounds"]), + holes=tuple(HoleDomain.from_dict(hole) for hole in holes), + decision_level=data["decision_level"], + parent_fingerprint=data["parent_fingerprint"], + ) diff --git a/tests/test_dsl/test_solver_state.py b/tests/test_dsl/test_solver_state.py new file mode 100644 index 00000000..bd5371df --- /dev/null +++ b/tests/test_dsl/test_solver_state.py @@ -0,0 +1,362 @@ +from __future__ import annotations + +import json +import os +import subprocess +import sys +from dataclasses import dataclass, replace +from pathlib import Path + +import pytest + +from slm_training.dsl.grammar.fastpath.compiler_draft import ( + CompletionForest, + CompletionPath, +) +from slm_training.dsl.solver import ( + DomainValue, + FiniteDomainState, + HoleDomain, + HoleId, + SolverBounds, + SupportVerdict, + completion_forest_state, +) + +BOUNDS = SolverBounds(64, 32, 8, 16, 20) + + +def value(number: int, *, tag: str = "token") -> DomainValue: + return DomainValue.create(tag, {"id": number}) + + +def hole(name: str, values: tuple[DomainValue, ...]) -> HoleDomain: + return HoleDomain( + HoleId("test", (name, 0), "choice"), + values, + (("support_verdict", SupportVerdict.UNKNOWN.value), ("coverage", "complete")), + ) + + +def state(*holes: HoleDomain) -> FiniteDomainState: + return FiniteDomainState("problem", "openui", "v1", BOUNDS, tuple(holes)) + + +def test_canonical_order_and_json_round_trip_stabilize_fingerprint() -> None: + a = hole("a", (value(2), value(1))) + b = HoleDomain( + HoleId("test", (1, "mixed"), "choice"), + (value(4), value(3)), + (("z", 1), ("a", True)), + ) + first = state(a, b) + second = state( + HoleDomain(b.hole_id, tuple(reversed(b.values)), tuple(reversed(b.metadata))), + HoleDomain(a.hole_id, tuple(reversed(a.values)), tuple(reversed(a.metadata))), + ) + + assert first == second + assert first.fingerprint == second.fingerprint + payload = json.loads(json.dumps(first.to_dict())) + restored = FiniteDomainState.from_dict(payload) + assert restored == first + assert restored.fingerprint == first.fingerprint + assert len(first.fingerprint) == 64 + + +@pytest.mark.parametrize( + "changed", + [ + lambda base: replace(base, problem_id="other"), + lambda base: replace(base, pack_id="other"), + lambda base: replace(base, constraint_version="v2"), + lambda base: replace(base, bounds=replace(BOUNDS, max_nodes=33)), + lambda base: replace( + base, + holes=(hole("other", (value(1), value(2))),), + ), + lambda base: replace(base, holes=(hole("a", (value(1),)),)), + lambda base: replace( + base, + holes=( + HoleDomain( + base.holes[0].hole_id, + base.holes[0].values, + (("coverage", "partial"),), + ), + ), + ), + ], +) +def test_fingerprint_changes_for_each_hard_field(changed) -> None: + base = state(hole("a", (value(1), value(2)))) + assert changed(base).fingerprint != base.fingerprint + + +@pytest.mark.parametrize( + "field", + [ + "max_tokens", + "max_nodes", + "max_depth", + "max_backtracks", + "max_verifier_calls", + ], +) +def test_fingerprint_changes_for_each_bound(field: str) -> None: + base = state(hole("a", (value(1), value(2)))) + changed_bounds = replace(BOUNDS, **{field: getattr(BOUNDS, field) + 1}) + assert replace(base, bounds=changed_bounds).fingerprint != base.fingerprint + + +def test_fingerprint_excludes_reversible_search_lineage() -> None: + base = state(hole("a", (value(1),))) + lineage = replace(base, decision_level=3, parent_fingerprint="a" * 64) + assert lineage.fingerprint == base.fingerprint + + +def test_bottom_structurally_solved_and_summary_semantics() -> None: + bottom = state(hole("empty", ())) + solved = state(hole("one", (value(1),))) + open_state = state(hole("many", (value(1), value(2)))) + + assert bottom.is_bottom and not bottom.is_structurally_solved + assert solved.is_structurally_solved and not solved.is_bottom + assert not open_state.is_bottom and not open_state.is_structurally_solved + assert open_state.summary() == { + "hole_count": 1, + "unresolved_count": 1, + "total_candidate_count": 2, + "max_domain_size": 2, + "mean_domain_size": 2.0, + "is_bottom": False, + "is_structurally_solved": False, + } + + +def test_refine_is_monotone_and_unknown_holes_fail_with_identity() -> None: + one, two, three = value(1), value(2), value(3) + base = state(hole("a", (one, two))) + hole_id = base.holes[0].hole_id + + refined = base.refine(hole_id, (two,), certificate_ref="future-proof-ref") + assert refined.domain(hole_id).values == (two,) + assert base.domain(hole_id).values == (one, two) + assert base.refine(hole_id, ()).is_bottom + with pytest.raises(ValueError, match="problem.*cannot add candidates"): + base.refine(hole_id, (one, three)) + with pytest.raises(LookupError, match="problem.*no hole"): + base.refine(HoleId("test", ("missing",), "choice"), ()) + + +def test_meet_intersects_domains_and_rejects_mismatched_identity() -> None: + one, two, three = value(1), value(2), value(3) + left = state(hole("a", (one, two))) + right = state(hole("a", (two, three))) + met = left.meet(right) + + assert met.holes[0].values == (two,) + assert met.is_structurally_solved + with pytest.raises(ValueError, match="mismatched identity"): + left.meet(replace(right, pack_id="other")) + with pytest.raises(ValueError, match="mismatched holes"): + left.meet(state(hole("b", (two,)))) + + +@pytest.mark.parametrize( + "changed", + [ + lambda base: replace(base, problem_id="other"), + lambda base: replace(base, pack_id="other"), + lambda base: replace(base, constraint_version="v2"), + lambda base: replace(base, bounds=replace(BOUNDS, max_tokens=65)), + lambda base: replace(base, bounds=replace(BOUNDS, max_nodes=33)), + lambda base: replace(base, bounds=replace(BOUNDS, max_depth=9)), + lambda base: replace(base, bounds=replace(BOUNDS, max_backtracks=17)), + lambda base: replace(base, bounds=replace(BOUNDS, max_verifier_calls=21)), + ], +) +def test_meet_rejects_every_identity_mismatch(changed) -> None: + base = state(hole("a", (value(1), value(2)))) + with pytest.raises(ValueError, match="mismatched identity"): + base.meet(changed(base)) + + +def test_meet_resets_unrelated_reversible_lineage() -> None: + base = state(hole("a", (value(1), value(2)))) + left = replace(base, decision_level=2, parent_fingerprint="a" * 64) + right = replace(base, decision_level=3, parent_fingerprint="b" * 64) + met = left.meet(right) + assert met.decision_level == 0 + assert met.parent_fingerprint is None + + +def test_decision_records_parent_without_claiming_support() -> None: + one, two = value(1), value(2) + base = state(hole("a", (one, two))) + chosen = base.with_decision(base.holes[0].hole_id, two) + + assert chosen.decision_level == 1 + assert chosen.parent_fingerprint == base.fingerprint + assert chosen.holes[0].values == (two,) + assert dict(chosen.holes[0].metadata)["support_verdict"] == "unknown" + + +def test_validation_rejects_duplicates_invalid_bounds_and_non_json() -> None: + one = value(1) + with pytest.raises(ValueError, match="duplicate values"): + hole("a", (one, one)) + with pytest.raises(ValueError, match="non-negative max_tokens"): + replace(BOUNDS, max_tokens=-1) + with pytest.raises(ValueError, match="not JSON-safe"): + DomainValue.create("bad", object()) + with pytest.raises(ValueError, match="duplicate hole IDs"): + state(hole("a", (one,)), hole("a", (value(2),))) + with pytest.raises(ValueError, match="requires DomainValue candidates"): + state(hole("a", (one,))).refine(hole("a", (one,)).hole_id, ({},)) + + +@pytest.mark.parametrize("left,right", [(True, 1), (1, 1.0), (-0.0, 0.0)]) +def test_metadata_json_types_remain_distinct(left, right) -> None: + hole_id = HoleId("test", ("typed",), "choice") + first = state(HoleDomain(hole_id, (value(1),), (("typed", left),))) + second = state(HoleDomain(hole_id, (value(1),), (("typed", right),))) + assert first != second + assert first.fingerprint != second.fingerprint + with pytest.raises(ValueError, match="mismatched metadata"): + first.meet(second) + + +def test_completion_forest_adapter_preserves_full_paths_kind_and_coverage() -> None: + forest = CompletionForest( + ( + CompletionPath((11, 21), "component"), + CompletionPath((11, 20), "component"), + CompletionPath((11, 20), "binder"), + ), + "partial", + ) + projected = completion_forest_state( + prefix_ids=[1, 2], + forest=forest, + pack_id="openui", + constraint_version="v1", + bounds=BOUNDS, + ) + payloads = [value.payload for value in projected.holes[0].values] + + assert payloads == [ + {"kind": "binder", "token_ids": [11, 20]}, + {"kind": "component", "token_ids": [11, 20]}, + {"kind": "component", "token_ids": [11, 21]}, + ] + assert dict(projected.holes[0].metadata) == { + "coverage": "partial", + "support_verdict": "unknown", + } + assert projected.holes[0].hole_id.path[0] == 2 + assert not projected.is_structurally_solved + + +def test_completion_forest_adapter_empty_singleton_and_ordering() -> None: + kwargs = { + "prefix_ids": (1,), + "pack_id": "openui", + "constraint_version": "v1", + "bounds": BOUNDS, + } + empty = completion_forest_state(forest=CompletionForest((), "none"), **kwargs) + path_a = CompletionPath((10, 12), "component") + path_b = CompletionPath((11,), "binder") + singleton = completion_forest_state( + forest=CompletionForest((path_a,), "complete"), **kwargs + ) + ordered = completion_forest_state( + forest=CompletionForest((path_a, path_b), "complete"), **kwargs + ) + reversed_state = completion_forest_state( + forest=CompletionForest((path_b, path_a), "complete"), **kwargs + ) + + assert empty.is_bottom + assert singleton.is_structurally_solved + assert dict(singleton.holes[0].metadata)["support_verdict"] == "unknown" + assert ordered == reversed_state + assert ordered.fingerprint == reversed_state.fingerprint + with pytest.raises(ValueError, match="duplicate values"): + completion_forest_state( + forest=CompletionForest((path_a, path_a), "complete"), **kwargs + ) + with pytest.raises(ValueError, match="prefix_ids must be non-negative integers"): + completion_forest_state( + forest=CompletionForest((path_a,), "complete"), + **{**kwargs, "prefix_ids": (True,)}, + ) + + +@pytest.mark.parametrize( + ("forest", "message"), + [ + (CompletionForest((), "bogus"), "coverage"), + (CompletionForest((CompletionPath((1,), ""),), "complete"), "kind"), + ( + CompletionForest((CompletionPath((True,), "component"),), "complete"), + "token_ids", + ), + ( + CompletionForest((CompletionPath((-1,), "component"),), "complete"), + "token_ids", + ), + ], +) +def test_completion_forest_adapter_rejects_malformed_input( + forest: CompletionForest, message: str +) -> None: + with pytest.raises(ValueError, match=message): + completion_forest_state( + prefix_ids=(), + forest=forest, + pack_id="openui", + constraint_version="v1", + bounds=BOUNDS, + ) + + +def test_completion_forest_adapter_ignores_explanation_only_fields() -> None: + @dataclass(frozen=True) + class ExtendedForest(CompletionForest): + evidence: tuple[str, ...] = () + + path = CompletionPath((10, 12), "component") + kwargs = { + "prefix_ids": (1,), + "pack_id": "openui", + "constraint_version": "v1", + "bounds": BOUNDS, + } + first = completion_forest_state( + forest=ExtendedForest((path,), "complete", evidence=("first",)), **kwargs + ) + second = completion_forest_state( + forest=ExtendedForest((path,), "complete", evidence=("second",)), **kwargs + ) + assert first == second + assert first.fingerprint == second.fingerprint + + +def test_solver_package_import_does_not_require_torch() -> None: + root = Path(__file__).parents[2] + code = """ +import importlib.abc +import sys +class BlockTorch(importlib.abc.MetaPathFinder): + def find_spec(self, fullname, path=None, target=None): + if fullname == 'torch' or fullname.startswith('torch.'): + raise AssertionError(f'unexpected torch import: {fullname}') + return None +sys.meta_path.insert(0, BlockTorch()) +import slm_training.dsl.solver +assert 'torch' not in sys.modules +""" + env = {**os.environ, "PYTHONPATH": str(root / "src")} + subprocess.run([sys.executable, "-c", code], check=True, cwd=root, env=env) From d0fba97053435716e24a5551ce2f99331112990f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 23:33:57 +0000 Subject: [PATCH 4/9] Add exhaustive tri-state support oracle and replayable certificates (SLM-60) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit VSS0-04: implement the deterministic reference oracle that decides whether a candidate participates in at least one bounded, verifier-accepted completion — the first component allowed to produce UNSUPPORTED — plus a pure replay checker. Torch-free, not wired into decode, no ship or speed claim. - dsl/solver/support.py: SupportQuery / SupportCertificate / SupportResult / SearchCounters, the SupportOracle + ProblemExpander + Verifier protocols, and EnumerativeSupportOracle — iterative (no Python recursion) deterministic search in canonical domain-value order, fingerprint dedup, per-SolverBounds budgets, tri-state verdicts (SUPPORTED witness / exhausted-complete UNSUPPORTED / partial|budget|unavailable UNKNOWN), and replay_support_certificate returning structured violations rather than a bare bool. - dsl/solver/openui_support.py: OpenUIForestExpander (advances a token prefix via build_completion_forest + completion_forest_state; eos->terminal, none->dead, partial->incomplete) and OpenUIWellFormedVerifier (lang-core validate; ParseError ->REJECT, missing-bridge/timeout->UNAVAILABLE, never UNSUPPORTED). - tests/test_dsl/test_solver_support.py: tiny closed fixtures pinning all three verdicts, witness-before-partial, duplicate-state suppression, determinism, stale-query/candidate rejection, JSON round-trip, torch-free, and replay rejection of tampered digests / non-exhausted UNSUPPORTED / incomplete coverage / stale versions, plus an OpenUI wiring smoke. - solver/__init__ exports the new public API; docs add the implemented-oracle section + tri-state table + replay rules to verified-scope-solver.md and a prefix-extendability-vs-support subsection to lattice-recursive-search.md. Verified: pytest test_solver_support.py test_solver_state.py test_compiler_decode.py (92 passed), ruff, repo_policy, git diff --check. Stacked on SLM-59. The 13 failures check-changed surfaces are pre-existing environmental DSL/pack/tokenizer failures on the base branch (vocab 500!=480, bridge-unavailable QUARANTINE), unrelated to this change. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt --- docs/design/lattice-recursive-search.md | 15 + docs/design/verified-scope-solver.md | 58 ++ src/slm_training/dsl/solver/__init__.py | 30 + src/slm_training/dsl/solver/openui_support.py | 169 +++++ src/slm_training/dsl/solver/support.py | 588 ++++++++++++++++++ tests/test_dsl/test_solver_support.py | 423 +++++++++++++ 6 files changed, 1283 insertions(+) create mode 100644 src/slm_training/dsl/solver/openui_support.py create mode 100644 src/slm_training/dsl/solver/support.py create mode 100644 tests/test_dsl/test_solver_support.py diff --git a/docs/design/lattice-recursive-search.md b/docs/design/lattice-recursive-search.md index d13eb23f..950a9137 100644 --- a/docs/design/lattice-recursive-search.md +++ b/docs/design/lattice-recursive-search.md @@ -51,6 +51,21 @@ This preserves the compiler as verifier. A learned conflict or quality score may prioritize exploration, but cannot create a legal branch, discard all legal branches, or bypass final OpenUI validation. +### Prefix-global extendability vs. verifier-backed support (VSS0-04) + +`CompletionForest` answers **prefix-global extendability**: at this decode +position, a candidate is grammar/schema/binder-admissible and has at least one +maximal forced continuation. That is *not* the same as **support** — whether the +candidate participates in at least one bounded, verifier-accepted completion. The +[`EnumerativeSupportOracle`](../../src/slm_training/dsl/solver/support.py) (VSS0-04) +supplies the latter: it exhausts the candidate's finite completion space and only +returns `UNSUPPORTED` when every branch had `complete` coverage and no completion +verified — a `partial`/`none` forest, a missing verifier capability, or any budget +stop stays `UNKNOWN`, never `UNSUPPORTED`. A forest that admits a candidate as +extendable therefore never authorizes removal; only a replayed support certificate +does. The oracle is not wired into decode, so this section changes no runtime +behavior. + ## Campaign design (V9) The registered runnable rows are hypotheses, not results. The matched controls separate the diff --git a/docs/design/verified-scope-solver.md b/docs/design/verified-scope-solver.md index dcc2e585..edf0f36f 100644 --- a/docs/design/verified-scope-solver.md +++ b/docs/design/verified-scope-solver.md @@ -154,6 +154,48 @@ verified terminal, `SUPPORTED` claim, correctness gain, or ship claim. The `TopologyDomainAdapter` protocol is only a future model-independent seam and imports no model or Torch code. +## Implemented support oracle (VSS0-04 / SLM-60) + +[`dsl/solver/support.py`](../../src/slm_training/dsl/solver/support.py) implements +the deterministic reference oracle — the **first** component allowed to produce +`UNSUPPORTED` — plus a pure replay checker. It is Torch-free, is not wired into +decode, and makes no speed or ship claim. The problem-specific parts (how a chosen +value expands, how a terminal is verified) are injected through the `ProblemExpander` +and `Verifier` protocols; [`openui_support.py`](../../src/slm_training/dsl/solver/openui_support.py) +supplies the OpenUI wiring while tiny closed fixtures drive the exhaustive tests. + +`EnumerativeSupportOracle.check(state, query)` iteratively explores the queried +candidate's completions (no Python recursion), deduplicates by the VSS0-03 +`FiniteDomainState.fingerprint`, enforces every `SolverBounds` budget, and returns +one verdict with a replayable `SupportCertificate`: + +| Verdict | Reference behavior | Removal? | +| --- | --- | --- | +| `SUPPORTED` | A `Verifier` `ACCEPT` on a decoded terminal was found. Valid even if other branches stay partial; the certificate stores only the witness **digest** plus a source label (never raw text/logits/timestamps). | Candidate stays live. | +| `UNSUPPORTED` | The candidate's whole finite completion space was exhausted with **only** `complete` coverage and no accepted terminal (`exhausted=True`, `stop_reason=None`). | **Yes — only** under a replayed `UNSUPPORTED` certificate. | +| `UNKNOWN` | Any `partial`/`none` coverage at a required expansion, a `Verifier` `UNAVAILABLE` (missing bridge/pack capability/timeout), or any budget stop. `exhausted=False`. | **Never.** | + +- **Search order** — `canonical-domain-value-v1`: values are explored in the + canonical order `HoleDomain` guarantees, so the search is deterministic and + logit-independent (`build_completion_forest` takes no scores). +- **Certificate** — schema version `1`; records the query, verdict, problem/pack/ + constraint identity, bounds, search order, explored-state fingerprints, coverage + observations, verifier profile, witness digest/source, per-reason failure counts, + `exhausted`, and `stop_reason`. +- **Verifier profile (fixture wiring)** — `openui/lang-core-validate/well-formed@0.2.x`: + a genuine `ParseError` is a hard `REJECT`; a missing lang-core bridge, timeout, or + other `RuntimeError` is `UNAVAILABLE` → `UNKNOWN`. A timeout/UNAVAILABLE is **never** + `UNSUPPORTED` (the timeout-vs-UNSAT distinction the contract requires). +- **Replay** — `replay_support_certificate(...)` re-derives identity, reruns the + deterministic search, and returns structured violations (never a bare bool). It + rejects an `UNSUPPORTED` certificate whose `exhausted` is false, whose coverage is + incomplete, or that carries a budget stop; and a `SUPPORTED` certificate whose + witness digest does not match a re-verified witness. `UNKNOWN` is accepted as an + honest result but never as pruning authority. + +Non-goals honored: no multi-candidate closure loop, no model ranking, no SMT +dependency, no decode/runtime flag, and no production-scale performance claim. + ## Reference support semantics | Verdict | Requirement | Removal permitted? | @@ -349,3 +391,19 @@ does not implement recursive support search, a proof checker, capsule solving, decode integration, or model scoring. No train, eval, benchmark, checkpoint, or experiment ran; this is infrastructure only and makes **no correctness, readiness, or ship claim**. + +2026-07-17 — VSS0-04 / SLM-60 implements the deterministic enumerative support +oracle and pure certificate replay (`dsl/solver/support.py`) plus the OpenUI +expander/verifier wiring (`dsl/solver/openui_support.py`). Correctness is pinned by +tiny closed fixtures (`tests/test_dsl/test_solver_support.py`): SUPPORTED with a +witness digest, UNSUPPORTED only after exhausted complete-coverage search, +UNKNOWN for every partial-coverage/budget/unavailable condition, duplicate-state +suppression, deterministic ordering, and replay rejection of tampered digests, +non-exhausted `UNSUPPORTED`, incomplete coverage, and stale versions. The oracle is +**not** wired into generation; default decode behavior is unchanged. Verifier +`UNAVAILABLE`/timeouts never become `UNSUPPORTED`. This is a reference correctness +implementation — no train/eval/benchmark/checkpoint ran and **no ship or +speed claim** is made. Verified: `python -m pytest +tests/test_dsl/test_solver_support.py tests/test_dsl/test_solver_state.py +tests/test_models/test_compiler_decode.py -q` (92 passed) and +`python -m scripts.repo_policy`. diff --git a/src/slm_training/dsl/solver/__init__.py b/src/slm_training/dsl/solver/__init__.py index c4b50aed..b3db1d9b 100644 --- a/src/slm_training/dsl/solver/__init__.py +++ b/src/slm_training/dsl/solver/__init__.py @@ -13,15 +13,45 @@ SolverBounds, SupportVerdict, ) +from slm_training.dsl.solver.support import ( + EnumerativeSupportOracle, + ExpandStatus, + ExpandStep, + ProblemExpander, + ReplayResult, + SearchCounters, + SupportCertificate, + SupportOracle, + SupportQuery, + SupportResult, + VerifyOutcome, + VerifyStatus, + Verifier, + replay_support_certificate, +) __all__ = [ "DomainValue", + "EnumerativeSupportOracle", + "ExpandStatus", + "ExpandStep", "FiniteDomainState", "HoleDomain", "HoleId", "JsonScalar", + "ProblemExpander", + "ReplayResult", + "SearchCounters", "SolverBounds", + "SupportCertificate", + "SupportOracle", + "SupportQuery", + "SupportResult", "SupportVerdict", "TopologyDomainAdapter", + "Verifier", + "VerifyOutcome", + "VerifyStatus", "completion_forest_state", + "replay_support_certificate", ] diff --git a/src/slm_training/dsl/solver/openui_support.py b/src/slm_training/dsl/solver/openui_support.py new file mode 100644 index 00000000..efe7f932 --- /dev/null +++ b/src/slm_training/dsl/solver/openui_support.py @@ -0,0 +1,169 @@ +"""OpenUI wiring for the enumerative support oracle (VSS0-04). + +Adapts the deterministic compiler forest and the lang-core validity check to the +problem-independent :class:`~slm_training.dsl.solver.support.EnumerativeSupportOracle`. + +* :class:`OpenUIForestExpander` advances a token prefix through + :func:`build_completion_forest`, projecting each next decision with the VSS0-03 + :func:`completion_forest_state` adapter. A chosen ``eos`` path terminates the + program; a ``coverage == "none"`` forest is bottom; a ``partial``/``none`` + child is reported ``INCOMPLETE`` so the oracle keeps it ``UNKNOWN`` (it can + never be exhaustively covered). +* :class:`OpenUIWellFormedVerifier` runs the deterministic lang-core parse/schema + check. A genuine ``ParseError`` is a hard ``REJECT``; a missing bridge, timeout, + or other runtime fault is ``UNAVAILABLE`` (→ ``UNKNOWN``), **never** + ``UNSUPPORTED`` — the timeout-vs-UNSAT distinction the contract requires. + +This module is Torch-free and is not invoked by decode by default. +""" + +from __future__ import annotations + +from typing import Any + +from slm_training.dsl.grammar.fastpath.compiler_draft import build_completion_forest +from slm_training.dsl.grammar.fastpath.token_map import decode_prefix +from slm_training.dsl.solver.adapters import completion_forest_state +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleId, + SolverBounds, +) +from slm_training.dsl.solver.support import ( + ExpandStatus, + ExpandStep, + VerifyOutcome, + VerifyStatus, +) + +WELL_FORMED_PROFILE = "openui/lang-core-validate/well-formed@0.2.x" + + +class OpenUIWellFormedVerifier: + """Deterministic lang-core well-formedness verifier (G0-G2 surface). + + ``profile`` is the recorded verifier identity. This checks structural + validity only (``reward_label`` is ``well_formed_not_behavioral``); it is not + a behavioral or ship verdict. + """ + + def __init__(self, *, profile: str = WELL_FORMED_PROFILE) -> None: + self._profile = profile + + @property + def profile(self) -> str: + return self._profile + + def verify(self, program: str) -> VerifyOutcome: + from slm_training.dsl import lang_core + + if not lang_core.bridge_available(): + return VerifyOutcome(VerifyStatus.UNAVAILABLE, detail="bridge_unavailable") + try: + lang_core.validate(program) + except lang_core.ParseError: + return VerifyOutcome(VerifyStatus.REJECT, detail="parse_error") + except RuntimeError as exc: # bridge/timeout — capability, not a rejection + return VerifyOutcome(VerifyStatus.UNAVAILABLE, detail=type(exc).__name__) + return VerifyOutcome(VerifyStatus.ACCEPT) + + +class OpenUIForestExpander: + """Bounded deterministic expander over the OpenUI choice/compiler forest.""" + + def __init__( + self, + tokenizer: Any, + prefix_ids: tuple[int, ...] | list[int], + *, + pack_id: str, + constraint_version: str, + bounds: SolverBounds, + max_path_tokens: int = 8, + ) -> None: + self._tok = tokenizer + self._pack_id = pack_id + self._cv = constraint_version + self._bounds = bounds + self._mpt = max(1, int(max_path_tokens)) + self._eos = int(tokenizer.eos_id) + self._prefix_by_fp: dict[str, tuple[int, ...]] = {} + self._root = self._project(tuple(int(t) for t in prefix_ids)) + + def _project(self, prefix: tuple[int, ...]) -> FiniteDomainState: + forest = build_completion_forest(self._tok, list(prefix), max_path_tokens=self._mpt) + state = completion_forest_state( + prefix_ids=prefix, + forest=forest, + pack_id=self._pack_id, + constraint_version=self._cv, + bounds=self._bounds, + ) + self._prefix_by_fp[state.fingerprint] = prefix + return state + + # --- ProblemExpander protocol ---------------------------------------- # + @property + def problem_id(self) -> str: + return self._root.problem_id + + @property + def pack_id(self) -> str: + return self._pack_id + + @property + def constraint_version(self) -> str: + return self._cv + + @property + def bounds(self) -> SolverBounds: + return self._bounds + + def root_state(self) -> FiniteDomainState: + return self._root + + def successor( + self, state: FiniteDomainState, hole_id: HoleId, value: DomainValue + ) -> ExpandStep: + prefix = self._prefix_by_fp.get(state.fingerprint) + if prefix is None: + # The oracle only expands states this expander created; a miss means + # an out-of-band state we cannot faithfully advance -> UNKNOWN. + return ExpandStep( + ExpandStatus.INCOMPLETE, coverage="none", detail="unknown_state" + ) + payload = value.payload + token_ids = tuple(int(tok) for tok in payload.get("token_ids", ())) + kind = str(payload.get("kind", "")) + if kind == "eos" or (len(token_ids) == 1 and token_ids[0] == self._eos): + program = decode_prefix(self._tok, list(prefix)) + return ExpandStep( + ExpandStatus.TERMINAL, + program=program, + coverage="complete", + detail=f"prefix_len={len(prefix)}", + ) + new_prefix = prefix + token_ids + forest = build_completion_forest( + self._tok, list(new_prefix), max_path_tokens=self._mpt + ) + if forest.coverage == "none": + return ExpandStep(ExpandStatus.DEAD, coverage="none", detail="illegal_prefix") + if not forest.paths: + return ExpandStep( + ExpandStatus.INCOMPLETE, + coverage=forest.coverage, + detail="no_enumerated_actions", + ) + child = completion_forest_state( + prefix_ids=new_prefix, + forest=forest, + pack_id=self._pack_id, + constraint_version=self._cv, + bounds=self._bounds, + ) + self._prefix_by_fp[child.fingerprint] = new_prefix + return ExpandStep( + ExpandStatus.CONTINUE, next_state=child, coverage=forest.coverage + ) diff --git a/src/slm_training/dsl/solver/support.py b/src/slm_training/dsl/solver/support.py new file mode 100644 index 00000000..2d58d284 --- /dev/null +++ b/src/slm_training/dsl/solver/support.py @@ -0,0 +1,588 @@ +"""Exhaustive tri-state support oracle and replayable certificates (VSS0-04). + +This is the first component allowed to produce ``UNSUPPORTED``. It answers, for a +single candidate at one hole of a :class:`FiniteDomainState`, whether that +candidate participates in at least one bounded, verifier-accepted completion: + +* ``SUPPORTED`` — a verifier-accepted witness completion using the candidate was + found (a witness is valid even if other branches are only partially covered); +* ``UNSUPPORTED`` — **every** reachable completion inside the declared finite + bounds was exhausted with **complete** coverage and none verified; +* ``UNKNOWN`` — coverage was partial/none at a required expansion, a capability + was unavailable, or a finite budget was exhausted before a witness. ``UNKNOWN`` + never licenses candidate removal, and a budget/timeout is never ``UNSUPPORTED``. + +The search is deterministic and independent of model logits (values are explored +in the canonical order guaranteed by :class:`~slm_training.dsl.solver.state.HoleDomain`). +The problem-specific parts — how a chosen value expands to the next decision or a +terminal program, and how a terminal is verified — are injected through the +:class:`ProblemExpander` and :class:`Verifier` protocols, so the core is testable +against tiny closed fixtures and reused by the OpenUI adapter in +``openui_support.py``. Semantics are owned by +``docs/design/verified-scope-solver.md``. +""" + +from __future__ import annotations + +import hashlib +import json +from dataclasses import dataclass +from enum import Enum +from typing import Any, Protocol + +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleId, + SolverBounds, + SupportVerdict, +) + +CERTIFICATE_SCHEMA_VERSION = 1 +SEARCH_ORDER = "canonical-domain-value-v1" + + +def _canonical_json(value: Any) -> str: + return json.dumps( + value, + allow_nan=False, + ensure_ascii=False, + separators=(",", ":"), + sort_keys=True, + ) + + +def _sha256(text: str) -> str: + return hashlib.sha256(text.encode()).hexdigest() + + +def _require_digest(value: Any, *, field: str) -> str: + if ( + not isinstance(value, str) + or len(value) != 64 + or any(char not in "0123456789abcdef" for char in value) + ): + raise ValueError(f"{field} must be a SHA-256 hex digest") + return value + + +# --------------------------------------------------------------------------- # +# Verifier + expander seams (problem-specific, injected) +# --------------------------------------------------------------------------- # + + +class VerifyStatus(str, Enum): + """Outcome of validating one structurally-solved terminal program.""" + + ACCEPT = "accept" # verifier-accepted witness + REJECT = "reject" # hard rejection: this terminal is not a witness + UNAVAILABLE = "unavailable" # capability missing -> UNKNOWN, never UNSUPPORTED + + +@dataclass(frozen=True) +class VerifyOutcome: + status: VerifyStatus + detail: str = "" + + +class ExpandStatus(str, Enum): + """How one chosen value advances the bounded search.""" + + TERMINAL = "terminal" # the choice completes a program to verify + CONTINUE = "continue" # the choice leads to the next decision state + DEAD = "dead" # the choice leads to bottom (no legal continuation) + INCOMPLETE = "incomplete" # coverage partial/none or capability unavailable + + +@dataclass(frozen=True) +class ExpandStep: + """Result of applying one value to one hole of the current state.""" + + status: ExpandStatus + program: str | None = None + next_state: FiniteDomainState | None = None + coverage: str = "complete" + detail: str = "" + + +class Verifier(Protocol): + """Validates a structurally-solved terminal program.""" + + @property + def profile(self) -> str: + """Stable identifier of the verifier stack/profile used.""" + ... + + def verify(self, program: str) -> VerifyOutcome: ... + + +class ProblemExpander(Protocol): + """Deterministic bounded expansion of the choice/compiler search space.""" + + @property + def problem_id(self) -> str: ... + + @property + def pack_id(self) -> str: ... + + @property + def constraint_version(self) -> str: ... + + @property + def bounds(self) -> SolverBounds: ... + + def successor( + self, state: FiniteDomainState, hole_id: HoleId, value: DomainValue + ) -> ExpandStep: + """Apply ``value`` at ``hole_id`` and report the successor step. + + Must be deterministic and independent of model logits. + """ + ... + + +# --------------------------------------------------------------------------- # +# Query / certificate / result contracts +# --------------------------------------------------------------------------- # + + +@dataclass(frozen=True) +class SupportQuery: + """Identifies the candidate whose support is being decided.""" + + state_fingerprint: str + hole_id: HoleId + candidate: DomainValue + + def __post_init__(self) -> None: + _require_digest(self.state_fingerprint, field="query state_fingerprint") + if not isinstance(self.hole_id, HoleId): + raise ValueError("support query requires a HoleId") + if not isinstance(self.candidate, DomainValue): + raise ValueError("support query requires a DomainValue candidate") + + def to_dict(self) -> dict[str, Any]: + return { + "state_fingerprint": self.state_fingerprint, + "hole_id": self.hole_id.to_dict(), + "candidate": self.candidate.to_dict(), + } + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> SupportQuery: + return cls( + state_fingerprint=str(data["state_fingerprint"]), + hole_id=HoleId.from_dict(data["hole_id"]), + candidate=DomainValue.from_dict(data["candidate"]), + ) + + +@dataclass(frozen=True) +class SearchCounters: + """Bounded work counters; a frozen snapshot travels in the result.""" + + nodes: int = 0 + tokens: int = 0 + depth: int = 0 + backtracks: int = 0 + verifier_calls: int = 0 + + def to_dict(self) -> dict[str, int]: + return { + "nodes": self.nodes, + "tokens": self.tokens, + "depth": self.depth, + "backtracks": self.backtracks, + "verifier_calls": self.verifier_calls, + } + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> SearchCounters: + return cls(**{key: int(data[key]) for key in cls().to_dict()}) + + +class _MutableCounters: + """Internal running counters checked against bounds during search.""" + + __slots__ = ("nodes", "tokens", "depth", "backtracks", "verifier_calls") + + def __init__(self) -> None: + self.nodes = 0 + self.tokens = 0 + self.depth = 0 + self.backtracks = 0 + self.verifier_calls = 0 + + def snapshot(self) -> SearchCounters: + return SearchCounters( + nodes=self.nodes, + tokens=self.tokens, + depth=self.depth, + backtracks=self.backtracks, + verifier_calls=self.verifier_calls, + ) + + def over_budget(self, bounds: SolverBounds) -> str | None: + if self.nodes > bounds.max_nodes: + return "budget:max_nodes" + if self.tokens > bounds.max_tokens: + return "budget:max_tokens" + if self.depth > bounds.max_depth: + return "budget:max_depth" + if self.backtracks > bounds.max_backtracks: + return "budget:max_backtracks" + if self.verifier_calls > bounds.max_verifier_calls: + return "budget:max_verifier_calls" + return None + + +@dataclass(frozen=True) +class SupportCertificate: + """Replayable justification for a support verdict. + + Contains no model logits, timestamps, secrets, or raw user-region contents; + a witness travels only as ``witness_digest`` plus a source label. + """ + + schema_version: int + query: SupportQuery + verdict: SupportVerdict + problem_id: str + pack_id: str + constraint_version: str + bounds: SolverBounds + search_order: str + explored_state_fingerprints: tuple[str, ...] + coverage_observations: tuple[str, ...] + verifier_profile: str + witness_source: str | None = None + witness_digest: str | None = None + failure_counts: tuple[tuple[str, int], ...] = () + exhausted: bool = False + stop_reason: str | None = None + + def to_dict(self) -> dict[str, Any]: + return { + "schema_version": self.schema_version, + "query": self.query.to_dict(), + "verdict": self.verdict.value, + "problem_id": self.problem_id, + "pack_id": self.pack_id, + "constraint_version": self.constraint_version, + "bounds": self.bounds.to_dict(), + "search_order": self.search_order, + "explored_state_fingerprints": list(self.explored_state_fingerprints), + "coverage_observations": list(self.coverage_observations), + "verifier_profile": self.verifier_profile, + "witness_source": self.witness_source, + "witness_digest": self.witness_digest, + "failure_counts": [list(row) for row in self.failure_counts], + "exhausted": self.exhausted, + "stop_reason": self.stop_reason, + } + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> SupportCertificate: + return cls( + schema_version=int(data["schema_version"]), + query=SupportQuery.from_dict(data["query"]), + verdict=SupportVerdict(data["verdict"]), + problem_id=str(data["problem_id"]), + pack_id=str(data["pack_id"]), + constraint_version=str(data["constraint_version"]), + bounds=SolverBounds.from_dict(data["bounds"]), + search_order=str(data["search_order"]), + explored_state_fingerprints=tuple( + str(item) for item in data["explored_state_fingerprints"] + ), + coverage_observations=tuple( + str(item) for item in data["coverage_observations"] + ), + verifier_profile=str(data["verifier_profile"]), + witness_source=( + None if data.get("witness_source") is None else str(data["witness_source"]) + ), + witness_digest=( + None if data.get("witness_digest") is None else str(data["witness_digest"]) + ), + failure_counts=tuple( + (str(row[0]), int(row[1])) for row in data.get("failure_counts", ()) + ), + exhausted=bool(data.get("exhausted", False)), + stop_reason=( + None if data.get("stop_reason") is None else str(data["stop_reason"]) + ), + ) + + @property + def digest(self) -> str: + return _sha256(_canonical_json(self.to_dict())) + + +@dataclass(frozen=True) +class SupportResult: + verdict: SupportVerdict + certificate: SupportCertificate + witness: str | None = None + counters: SearchCounters = SearchCounters() + + +# --------------------------------------------------------------------------- # +# Enumerative reference oracle +# --------------------------------------------------------------------------- # + + +class SupportOracle(Protocol): + def check(self, state: FiniteDomainState, query: SupportQuery) -> SupportResult: ... + + +class EnumerativeSupportOracle: + """Deterministic bounded reference oracle over the choice/compiler path. + + Explores the candidate's completions iteratively (no Python recursion), + deduplicating by the hard-state fingerprint, and returns exactly one of + ``SUPPORTED``/``UNSUPPORTED``/``UNKNOWN`` with a replayable certificate. + """ + + def __init__(self, expander: ProblemExpander, verifier: Verifier) -> None: + self._expander = expander + self._verifier = verifier + + def check(self, state: FiniteDomainState, query: SupportQuery) -> SupportResult: + if not isinstance(state, FiniteDomainState): + raise ValueError("support oracle requires a FiniteDomainState") + if query.state_fingerprint != state.fingerprint: + raise ValueError( + "stale support query: fingerprint does not match the state" + ) + if ( + state.problem_id != self._expander.problem_id + or state.pack_id != self._expander.pack_id + or state.constraint_version != self._expander.constraint_version + or state.bounds != self._expander.bounds + ): + raise ValueError("support query identity does not match the expander") + domain = state.domain(query.hole_id) # raises LookupError on unknown hole + if query.candidate not in set(domain.values): + raise ValueError("support query candidate is not in the hole domain") + + counters = _MutableCounters() + explored: list[str] = [] + seen: set[str] = set() + coverage_obs: set[str] = set() + failures: dict[str, int] = {} + witness: str | None = None + witness_source: str | None = None + incomplete = False + stop_reason: str | None = None + + # Fix the queried candidate first, then explore its completions. + stack: list[tuple[FiniteDomainState, HoleId, DomainValue, int]] = [ + (state, query.hole_id, query.candidate, 0) + ] + + while stack: + current, hole_id, value, depth = stack.pop() + counters.nodes += 1 + counters.depth = max(counters.depth, depth) + budget = counters.over_budget(self._expander.bounds) + if budget is not None: + stop_reason = budget + incomplete = True + break + + step = self._expander.successor(current, hole_id, value) + counters.tokens += len(value.payload_json) + coverage_obs.add(step.coverage) + + if step.status is ExpandStatus.INCOMPLETE or step.coverage in {"partial", "none"}: + incomplete = True + failures[f"incomplete:{step.detail or step.coverage}"] = ( + failures.get(f"incomplete:{step.detail or step.coverage}", 0) + 1 + ) + continue + + if step.status is ExpandStatus.DEAD: + counters.backtracks += 1 + failures[f"dead:{step.detail or 'bottom'}"] = ( + failures.get(f"dead:{step.detail or 'bottom'}", 0) + 1 + ) + continue + + if step.status is ExpandStatus.TERMINAL: + program = step.program or "" + counters.verifier_calls += 1 + if counters.over_budget(self._expander.bounds) is not None: + stop_reason = "budget:max_verifier_calls" + incomplete = True + break + outcome = self._verifier.verify(program) + if outcome.status is VerifyStatus.ACCEPT: + witness = program + witness_source = step.detail or "terminal" + break + if outcome.status is VerifyStatus.UNAVAILABLE: + incomplete = True + failures[f"verifier_unavailable:{outcome.detail}"] = ( + failures.get(f"verifier_unavailable:{outcome.detail}", 0) + 1 + ) + continue + # REJECT: a hard non-witness; keep searching. + failures[f"reject:{outcome.detail or 'invalid'}"] = ( + failures.get(f"reject:{outcome.detail or 'invalid'}", 0) + 1 + ) + continue + + # CONTINUE: expand the next decision state. + child = step.next_state + if child is None: + incomplete = True + failures["incomplete:missing_next_state"] = ( + failures.get("incomplete:missing_next_state", 0) + 1 + ) + continue + child_fp = child.fingerprint + if child_fp in seen: + continue # deterministic dedup of equivalent hard states + seen.add(child_fp) + explored.append(child_fp) + if child.is_bottom: + counters.backtracks += 1 + failures["dead:child_bottom"] = failures.get("dead:child_bottom", 0) + 1 + continue + # Push every live (hole, value) branch of the child in canonical order + # (reversed so the smallest value is popped first). + child_hole = child.holes[0].hole_id + for child_value in reversed(child.holes[0].values): + stack.append((child, child_hole, child_value, depth + 1)) + + verdict, exhausted = _decide(witness is not None, incomplete, stop_reason) + certificate = SupportCertificate( + schema_version=CERTIFICATE_SCHEMA_VERSION, + query=query, + verdict=verdict, + problem_id=self._expander.problem_id, + pack_id=self._expander.pack_id, + constraint_version=self._expander.constraint_version, + bounds=self._expander.bounds, + search_order=SEARCH_ORDER, + explored_state_fingerprints=tuple(explored), + coverage_observations=tuple(sorted(coverage_obs)), + verifier_profile=self._verifier.profile, + witness_source=witness_source if verdict is SupportVerdict.SUPPORTED else None, + witness_digest=( + _sha256(witness) if witness is not None and verdict is SupportVerdict.SUPPORTED else None + ), + failure_counts=tuple(sorted(failures.items())), + exhausted=exhausted, + stop_reason=stop_reason, + ) + return SupportResult( + verdict=verdict, + certificate=certificate, + witness=witness if verdict is SupportVerdict.SUPPORTED else None, + counters=counters.snapshot(), + ) + + +def _decide( + found_witness: bool, incomplete: bool, stop_reason: str | None +) -> tuple[SupportVerdict, bool]: + """Map (witness, incompleteness, budget) to a verdict + exhaustiveness flag.""" + if found_witness: + return SupportVerdict.SUPPORTED, False + if incomplete or stop_reason is not None: + return SupportVerdict.UNKNOWN, False + # Fully explored, complete coverage, no witness. + return SupportVerdict.UNSUPPORTED, True + + +# --------------------------------------------------------------------------- # +# Certificate replay +# --------------------------------------------------------------------------- # + + +@dataclass(frozen=True) +class ReplayResult: + """Structured replay outcome; ``ok`` is true only when no violations remain.""" + + ok: bool + verdict: SupportVerdict + violations: tuple[str, ...] = () + + +def replay_support_certificate( + certificate: SupportCertificate, + *, + state: FiniteDomainState, + expander: ProblemExpander, + verifier: Verifier, +) -> ReplayResult: + """Independently re-check a certificate; never trusts a bare verdict. + + Re-derives identity, reruns the deterministic search, and enforces the + honesty rules: ``UNSUPPORTED`` requires an exhausted, fully-covered search + with no budget stop; ``SUPPORTED`` requires a re-verified witness whose digest + matches; ``UNKNOWN`` is accepted as honest but never as pruning authority. + """ + violations: list[str] = [] + + if certificate.schema_version != CERTIFICATE_SCHEMA_VERSION: + violations.append( + f"schema_version {certificate.schema_version} != {CERTIFICATE_SCHEMA_VERSION}" + ) + if certificate.search_order != SEARCH_ORDER: + violations.append("search_order mismatch") + if state.fingerprint != certificate.query.state_fingerprint: + violations.append("state fingerprint does not match certificate query") + for label, cert_value, live_value in ( + ("problem_id", certificate.problem_id, expander.problem_id), + ("pack_id", certificate.pack_id, expander.pack_id), + ("constraint_version", certificate.constraint_version, expander.constraint_version), + ("verifier_profile", certificate.verifier_profile, verifier.profile), + ): + if cert_value != live_value: + violations.append(f"{label} mismatch: {cert_value!r} != {live_value!r}") + if certificate.bounds != expander.bounds: + violations.append("bounds mismatch") + + # Rerun the search under the same deterministic oracle. + recomputed: SupportResult | None = None + if not violations: + try: + recomputed = EnumerativeSupportOracle(expander, verifier).check( + state, certificate.query + ) + except (ValueError, LookupError) as exc: + violations.append(f"replay could not rerun search: {exc}") + + if recomputed is not None: + if recomputed.verdict != certificate.verdict: + violations.append( + f"verdict changed on replay: {certificate.verdict.value} -> {recomputed.verdict.value}" + ) + if certificate.verdict is SupportVerdict.UNSUPPORTED: + if not certificate.exhausted: + violations.append("UNSUPPORTED certificate is not marked exhausted") + if certificate.stop_reason is not None: + violations.append("UNSUPPORTED certificate has a budget/stop reason") + if any(cov in {"partial", "none"} for cov in certificate.coverage_observations): + violations.append("UNSUPPORTED certificate has incomplete coverage") + if not recomputed.certificate.exhausted: + violations.append("replay did not reach exhaustion for UNSUPPORTED") + elif certificate.verdict is SupportVerdict.SUPPORTED: + if certificate.witness_digest is None: + violations.append("SUPPORTED certificate has no witness digest") + elif recomputed.witness is None: + violations.append("replay found no witness for SUPPORTED") + else: + if _sha256(recomputed.witness) != certificate.witness_digest: + violations.append("witness digest does not match replayed witness") + if verifier.verify(recomputed.witness).status is not VerifyStatus.ACCEPT: + violations.append("replayed witness is not verifier-accepted") + + return ReplayResult( + ok=not violations, + verdict=certificate.verdict, + violations=tuple(violations), + ) diff --git a/tests/test_dsl/test_solver_support.py b/tests/test_dsl/test_solver_support.py new file mode 100644 index 00000000..2a69420c --- /dev/null +++ b/tests/test_dsl/test_solver_support.py @@ -0,0 +1,423 @@ +"""VSS0-04 (SLM-60): exhaustive tri-state support oracle + certificate replay. + +The oracle core is exercised against tiny *closed* fixtures whose entire search +space is known, so every SUPPORTED/UNSUPPORTED/UNKNOWN verdict and every replay +rule can be asserted exactly. Torch-free. +""" + +from __future__ import annotations + +import inspect +import json +from dataclasses import replace + +import pytest + +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleDomain, + HoleId, + SolverBounds, + SupportVerdict, +) +from slm_training.dsl.solver.support import ( + EnumerativeSupportOracle, + ExpandStatus, + ExpandStep, + SupportCertificate, + SupportQuery, + VerifyOutcome, + VerifyStatus, + replay_support_certificate, +) + +# --------------------------------------------------------------------------- # +# Tiny closed fixture: words built letter-by-letter over a known finite tree. +# --------------------------------------------------------------------------- # + +_GENEROUS = SolverBounds( + max_tokens=100_000, + max_nodes=100_000, + max_depth=64, + max_backtracks=100_000, + max_verifier_calls=100_000, +) + + +class _WordExpander: + """Deterministic finite word tree. + + ``tree`` maps a prefix string to a tuple of branches. Each branch is + ``(letter, kind, coverage, next_prefix)`` where ``kind`` is one of + ``continue|terminal|dead|incomplete`` and ``next_prefix`` (optional) forces a + shared successor to exercise duplicate-state suppression. + """ + + def __init__(self, tree, *, bounds=_GENEROUS, constraint_version="v1"): + self._tree = tree + self._bounds = bounds + self._cv = constraint_version + self._prefix_by_fp: dict[str, str] = {} + self._root = self._state_for("") + self._prefix_by_fp[self._root.fingerprint] = "" + + # --- ProblemExpander protocol ---------------------------------------- # + @property + def problem_id(self) -> str: + return self._root.problem_id + + @property + def pack_id(self) -> str: + return "fixture-word" + + @property + def constraint_version(self) -> str: + return self._cv + + @property + def bounds(self) -> SolverBounds: + return self._bounds + + def root_state(self) -> FiniteDomainState: + return self._root + + def value_for(self, prefix: str, letter: str) -> DomainValue: + return DomainValue.create("letter", {"prefix": prefix, "letter": letter}) + + def _state_for(self, prefix: str) -> FiniteDomainState: + branches = self._tree.get(prefix, ()) + hole = HoleId(namespace="word", path=(len(prefix), prefix or "ROOT"), kind="next") + values = tuple(self.value_for(prefix, branch[0]) for branch in branches) + domain = HoleDomain(hole, values, metadata=(("node", prefix or "ROOT"),)) + return FiniteDomainState( + problem_id=f"word:{prefix or 'ROOT'}", + pack_id=self.pack_id, + constraint_version=self._cv, + bounds=self._bounds, + holes=(domain,), + ) + + def successor(self, state, hole_id, value) -> ExpandStep: + prefix = self._prefix_by_fp[state.fingerprint] + payload = value.payload + letter = payload["letter"] + branch = next(b for b in self._tree[prefix] if b[0] == letter) + _letter, kind, coverage = branch[0], branch[1], branch[2] + forced_next = branch[3] if len(branch) > 3 else None + if kind == "terminal": + return ExpandStep( + ExpandStatus.TERMINAL, program=prefix + letter, coverage=coverage, + detail=prefix + letter, + ) + if kind == "dead": + return ExpandStep(ExpandStatus.DEAD, coverage=coverage, detail="bottom") + if kind == "incomplete": + return ExpandStep(ExpandStatus.INCOMPLETE, coverage=coverage, detail="uncovered") + # continue + next_prefix = forced_next if forced_next is not None else prefix + letter + child = self._state_for(next_prefix) + self._prefix_by_fp[child.fingerprint] = next_prefix + return ExpandStep(ExpandStatus.CONTINUE, next_state=child, coverage=coverage) + + +class _AcceptVerifier: + """Accepts programs in a fixed set; everything else is a hard REJECT.""" + + def __init__(self, accept, *, profile="fixture-accept-v1"): + self._accept = set(accept) + self._profile = profile + + @property + def profile(self) -> str: + return self._profile + + def verify(self, program: str) -> VerifyOutcome: + if program in self._accept: + return VerifyOutcome(VerifyStatus.ACCEPT) + return VerifyOutcome(VerifyStatus.REJECT, detail="not-in-accept-set") + + +def _query(expander: _WordExpander, letter: str) -> SupportQuery: + root = expander.root_state() + return SupportQuery( + state_fingerprint=root.fingerprint, + hole_id=root.holes[0].hole_id, + candidate=expander.value_for("", letter), + ) + + +# tree: root -> a -> {x term, y term}; root -> b -> {z term} +_LINEAR_TREE = { + "": (("a", "continue", "complete"), ("b", "continue", "complete")), + "a": (("x", "terminal", "complete"), ("y", "terminal", "complete")), + "b": (("z", "terminal", "complete"),), +} + + +def _run(tree, accept, letter, *, bounds=_GENEROUS): + expander = _WordExpander(tree, bounds=bounds) + verifier = _AcceptVerifier(accept) + oracle = EnumerativeSupportOracle(expander, verifier) + result = oracle.check(expander.root_state(), _query(expander, letter)) + return expander, verifier, result + + +# --------------------------------------------------------------------------- # +# Tri-state verdicts +# --------------------------------------------------------------------------- # + + +def test_supported_returns_witness_and_digest(): + _e, _v, result = _run(_LINEAR_TREE, {"ax"}, "a") + assert result.verdict is SupportVerdict.SUPPORTED + assert result.witness == "ax" + assert result.certificate.witness_digest is not None + assert result.certificate.witness_source is not None + # A witness is valid even though the 'b' subtree was never explored. + assert result.certificate.exhausted is False + + +def test_unsupported_requires_exhaustion_and_complete_coverage(): + # 'b' leads only to 'bz', which is not accepted -> exhausted, complete -> UNSUPPORTED. + _e, _v, result = _run(_LINEAR_TREE, {"ax"}, "b") + assert result.verdict is SupportVerdict.UNSUPPORTED + assert result.certificate.exhausted is True + assert result.certificate.stop_reason is None + assert set(result.certificate.coverage_observations) <= {"complete"} + assert result.witness is None + # The hard rejection was recorded, not silently ignored. + assert any("reject" in code for code, _ in result.certificate.failure_counts) + + +def test_unknown_from_partial_coverage_never_unsupported(): + tree = { + "": (("b", "continue", "complete"),), + "b": (("z", "terminal", "complete"), ("w", "incomplete", "partial")), + } + _e, _v, result = _run(tree, set(), "b") # nothing accepted + assert result.verdict is SupportVerdict.UNKNOWN + assert result.certificate.exhausted is False + assert "partial" in result.certificate.coverage_observations + + +def test_unknown_from_each_budget_class(): + # A deep chain; a tiny node budget forces a budget stop -> UNKNOWN. + tree = {"": (("a", "continue", "complete"),), "a": (("b", "continue", "complete"),), + "ab": (("c", "terminal", "complete"),)} + expander = _WordExpander(tree, bounds=replace(_GENEROUS, max_nodes=1)) + verifier = _AcceptVerifier({"abc"}) + result = EnumerativeSupportOracle(expander, verifier).check( + expander.root_state(), _query(expander, "a") + ) + assert result.verdict is SupportVerdict.UNKNOWN + assert result.certificate.stop_reason == "budget:max_nodes" + assert result.certificate.exhausted is False + + +def test_supported_witness_found_before_a_partial_branch(): + tree = { + "": (("b", "continue", "complete"),), + "b": (("w", "incomplete", "partial"), ("z", "terminal", "complete")), + } + _e, _v, result = _run(tree, {"bz"}, "b") + # Despite a partial branch, a verified witness wins. + assert result.verdict is SupportVerdict.SUPPORTED + assert result.witness == "bz" + + +def test_duplicate_state_suppression(): + # Both 'a' and 'b' route to the shared successor prefix "m". + tree = { + "": (("a", "continue", "complete", "m"), ("b", "continue", "complete", "m")), + "m": (("z", "terminal", "complete"),), + } + expander = _WordExpander(tree) + verifier = _AcceptVerifier(set()) + # Query candidate 'a'; only one child state "m" should be explored/recorded. + result = EnumerativeSupportOracle(expander, verifier).check( + expander.root_state(), _query(expander, "a") + ) + fps = result.certificate.explored_state_fingerprints + assert len(fps) == len(set(fps)) # no duplicate fingerprints recorded + # Exactly one distinct child state ("m") was explored. + assert len(fps) == 1 + + +def test_evidence_is_deterministic_across_runs(): + a = _run(_LINEAR_TREE, {"ax"}, "b")[2].certificate.to_dict() + b = _run(_LINEAR_TREE, {"ax"}, "b")[2].certificate.to_dict() + assert json.dumps(a, sort_keys=True) == json.dumps(b, sort_keys=True) + + +# --------------------------------------------------------------------------- # +# Query / state validation +# --------------------------------------------------------------------------- # + + +def test_stale_fingerprint_query_is_rejected(): + expander = _WordExpander(_LINEAR_TREE) + verifier = _AcceptVerifier({"ax"}) + bad = SupportQuery( + state_fingerprint="0" * 64, # not the state's fingerprint + hole_id=expander.root_state().holes[0].hole_id, + candidate=expander.value_for("", "a"), + ) + with pytest.raises(ValueError, match="stale"): + EnumerativeSupportOracle(expander, verifier).check(expander.root_state(), bad) + + +def test_unknown_candidate_is_rejected(): + expander = _WordExpander(_LINEAR_TREE) + verifier = _AcceptVerifier(set()) + bad = SupportQuery( + state_fingerprint=expander.root_state().fingerprint, + hole_id=expander.root_state().holes[0].hole_id, + candidate=expander.value_for("", "zzz"), # not a live candidate + ) + with pytest.raises(ValueError, match="not in the hole domain"): + EnumerativeSupportOracle(expander, verifier).check(expander.root_state(), bad) + + +# --------------------------------------------------------------------------- # +# Certificate replay +# --------------------------------------------------------------------------- # + + +def test_supported_certificate_replays(): + expander, verifier, result = _run(_LINEAR_TREE, {"ax"}, "a") + replay = replay_support_certificate( + result.certificate, state=expander.root_state(), + expander=_WordExpander(_LINEAR_TREE), verifier=_AcceptVerifier({"ax"}), + ) + assert replay.ok, replay.violations + + +def test_unsupported_certificate_replays(): + expander, verifier, result = _run(_LINEAR_TREE, {"ax"}, "b") + replay = replay_support_certificate( + result.certificate, state=expander.root_state(), + expander=_WordExpander(_LINEAR_TREE), verifier=_AcceptVerifier({"ax"}), + ) + assert replay.ok, replay.violations + assert replay.verdict is SupportVerdict.UNSUPPORTED + + +def test_tampered_witness_digest_is_rejected(): + expander, _v, result = _run(_LINEAR_TREE, {"ax"}, "a") + tampered = replace(result.certificate, witness_digest="f" * 64) + replay = replay_support_certificate( + tampered, state=expander.root_state(), + expander=_WordExpander(_LINEAR_TREE), verifier=_AcceptVerifier({"ax"}), + ) + assert not replay.ok + assert any("witness digest" in v for v in replay.violations) + + +def test_unsupported_rejected_when_not_exhausted(): + expander, _v, result = _run(_LINEAR_TREE, {"ax"}, "b") + forged = replace(result.certificate, exhausted=False) + replay = replay_support_certificate( + forged, state=expander.root_state(), + expander=_WordExpander(_LINEAR_TREE), verifier=_AcceptVerifier({"ax"}), + ) + assert not replay.ok + assert any("exhaust" in v for v in replay.violations) + + +def test_unsupported_rejected_when_coverage_incomplete(): + expander, _v, result = _run(_LINEAR_TREE, {"ax"}, "b") + forged = replace( + result.certificate, + coverage_observations=result.certificate.coverage_observations + ("partial",), + ) + replay = replay_support_certificate( + forged, state=expander.root_state(), + expander=_WordExpander(_LINEAR_TREE), verifier=_AcceptVerifier({"ax"}), + ) + assert not replay.ok + assert any("incomplete coverage" in v for v in replay.violations) + + +def test_stale_constraint_version_replay_is_rejected(): + expander, _v, result = _run(_LINEAR_TREE, {"ax"}, "b") + replay = replay_support_certificate( + result.certificate, state=expander.root_state(), + expander=_WordExpander(_LINEAR_TREE, constraint_version="v2"), # stale + verifier=_AcceptVerifier({"ax"}), + ) + assert not replay.ok + assert any("constraint_version" in v or "fingerprint" in v for v in replay.violations) + + +# --------------------------------------------------------------------------- # +# Serialization + hygiene +# --------------------------------------------------------------------------- # + + +def test_certificate_and_query_round_trip_json(): + _e, _v, result = _run(_LINEAR_TREE, {"ax"}, "b") + cert = result.certificate + restored = SupportCertificate.from_dict(json.loads(json.dumps(cert.to_dict()))) + assert restored == cert + q = cert.query + assert SupportQuery.from_dict(json.loads(json.dumps(q.to_dict()))) == q + + +def test_solver_support_is_torch_free(): + import slm_training.dsl.solver.support as support_mod + import slm_training.dsl.solver.state as state_mod + import slm_training.dsl.solver.openui_support as openui_mod + + for mod in (support_mod, state_mod, openui_mod): + assert "torch" not in inspect.getsource(mod) + + +# --------------------------------------------------------------------------- # +# OpenUI wiring smoke: real compiler forest + lang-core well-formedness. +# --------------------------------------------------------------------------- # + + +def test_openui_expander_wires_forest_and_never_false_unsupported(): + from slm_training.models.dsl_tokenizer import DSLNativeTokenizer + from slm_training.dsl.solver.openui_support import ( + OpenUIForestExpander, + OpenUIWellFormedVerifier, + ) + + tok = DSLNativeTokenizer.build() + prefix = [tok.bos_id, *tok.encode("root=Card([", add_special=False)] + bounds = SolverBounds( + max_tokens=4000, max_nodes=24, max_depth=12, max_backtracks=200, + max_verifier_calls=24, + ) + + def build_expander(): + return OpenUIForestExpander( + tok, prefix, pack_id="openui", constraint_version="test-cv", bounds=bounds + ) + + expander = build_expander() + root = expander.root_state() + assert root.holes and root.holes[0].values, "compiler forest yielded no candidates" + + verifier = OpenUIWellFormedVerifier() + query = SupportQuery( + state_fingerprint=root.fingerprint, + hole_id=root.holes[0].hole_id, + candidate=root.holes[0].values[0], + ) + result = EnumerativeSupportOracle(expander, verifier).check(root, query) + + assert result.verdict in set(SupportVerdict) + # Honesty invariant: UNSUPPORTED only with an exhausted, fully-covered search. + if result.verdict is SupportVerdict.UNSUPPORTED: + assert result.certificate.exhausted + assert set(result.certificate.coverage_observations) <= {"complete"} + # A capability-limited run (bridge unavailable / budget) must stay UNKNOWN, + # never a false UNSUPPORTED. + replay = replay_support_certificate( + result.certificate, state=root, + expander=build_expander(), verifier=OpenUIWellFormedVerifier(), + ) + assert replay.ok, replay.violations From a7cfef4034a4a897e03c9561d8860d9c840bc405 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 23:47:05 +0000 Subject: [PATCH 5/9] Add certificate-checked exact closure over finite domains (SLM-61) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit VSS1-01: implement the deterministic monotone fixed-point operator that orchestrates the VSS0-04 support oracle and removes only candidates carrying a replay-valid UNSUPPORTED certificate. Pure orchestration — it does not reimplement the support search. Torch-free, no decode integration, no ship claim. - dsl/solver/closure.py: exact_closure(state, provider, *, query_order, cache, certificate_store, max_queries) plus CertifiedDeduction / ClosureCounters / ClosureResult / WitnessRef and the SupportProvider protocol + EnumerativeSupportProvider (oracle + replay). Deterministic query order (smallest domain, then HoleId, then canonical value order); per-pass deductions applied against one consistent pass-start state; stale proofs re-queried (cache keyed by state fingerprint + hole/value + backend version); certified bottom only when every value was removed under an accepted certificate; UNKNOWN / failed-replay never shrink a domain. - tests/test_dsl/test_solver_closure.py: tiny fixtures for multi-pass propagation, UNKNOWN/SUPPORTED retention, forged-certificate no-op (state identity unchanged), all-unsupported certified bottom, budgeted partial closure, determinism, cache identity, stale-replay rejection, subset invariant, and torch-free. - solver/__init__ exports the new API; docs add fixed-point pseudocode + pass consistency + stale-proof handling + structurally-solved vs certified-bottom vs partial-closure to verified-scope-solver.md. Verified: pytest test_solver_closure.py test_solver_support.py (31 passed), ruff, repo_policy, git diff --check. Stacked on SLM-60. The 13 check-changed failures are pre-existing environmental DSL/pack/tokenizer failures on the base branch, unrelated to this change. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt --- docs/design/verified-scope-solver.md | 62 ++++ src/slm_training/dsl/solver/__init__.py | 18 ++ src/slm_training/dsl/solver/closure.py | 358 ++++++++++++++++++++++++ tests/test_dsl/test_solver_closure.py | 329 ++++++++++++++++++++++ 4 files changed, 767 insertions(+) create mode 100644 src/slm_training/dsl/solver/closure.py create mode 100644 tests/test_dsl/test_solver_closure.py diff --git a/docs/design/verified-scope-solver.md b/docs/design/verified-scope-solver.md index edf0f36f..55f0c9a2 100644 --- a/docs/design/verified-scope-solver.md +++ b/docs/design/verified-scope-solver.md @@ -196,6 +196,54 @@ one verdict with a replayable `SupportCertificate`: Non-goals honored: no multi-candidate closure loop, no model ranking, no SMT dependency, no decode/runtime flag, and no production-scale performance claim. +## Implemented exact closure (VSS1-01 / SLM-61) + +[`dsl/solver/closure.py`](../../src/slm_training/dsl/solver/closure.py) adds the +monotone fixed-point operator `exact_closure(state, provider, *, query_order, cache, +certificate_store, max_queries)`. It is a **pure orchestration layer** over the +VSS0-04 oracle (a `SupportProvider` = the oracle + its replay checker) — it never +reimplements the support search — and removes only candidates carrying a +replay-valid `UNSUPPORTED` certificate. Reference fixed-point: + +```text +def exact_closure(state, provider): + while True: + if state.is_bottom: return certified_bottom(state) # every value certified-removed + holes = unresolved_holes(state) # domains with > 1 value + if not holes: return structurally_solved(state) # every domain singleton + removals = {} + for hole in order(holes): # smallest domain, then HoleId + for value in hole.values: # canonical value order + r = provider.check(state, query(state, hole, value)) # cached by (fp,hole,value,backend) + if r.verdict is SUPPORTED: keep_witness(r) # kept; alternatives not collapsed + elif r.verdict is UNSUPPORTED: + if provider.replay(r.certificate, state=state).ok: # REQUIRED: replay vs pass-start state + removals[hole].add(value, because=r.certificate) # DESTRUCTIVE — cites certificate + else: record_unknown(value) # stale/tampered proof never removes + else: record_unknown(value) # UNKNOWN never shrinks a domain + if not removals: return fixed_point(state) + state = apply_all(removals, against=state) # one new state per pass (pass-consistent) +``` + +- **Pass consistency.** Every deduction in a pass is computed against the same + pass-start state and applied together to form one new immutable state; the next + pass re-queries against the new fingerprint. A proof that went stale after a + reduction is therefore never reused — the cache is keyed by `state.fingerprint` + (plus hole/value/backend version), so a shrunk state is a cache miss and forces a + fresh query, and every removal replays against the exact pre-refinement state. +- **Three distinct terminal states.** *Structurally solved* = every domain is a + singleton (a candidate chosen per hole; still not a verified terminal). *Certified + bottom* = some domain is empty **because every one of its values was removed under + an accepted certificate** (`reached_fixed_point=True`). *Partial closure* = a + `max_queries` budget stopped the loop with live domains (`reached_fixed_point=False`, + `stop_reason="budget:max_queries"`) — an honest partial, never a bottom or a + solved claim. +- **Honesty.** `UNKNOWN` (and any `UNSUPPORTED` whose certificate fails replay) + never decreases a domain; `result.state` is always a subset of the input and every + `CertifiedDeduction` cites one certificate id per removed value. `CertifiedDeduction` + stores certificate **references** (digests) plus compact summaries; full + certificates live in a caller-provided `certificate_store`. + ## Reference support semantics | Verdict | Requirement | Removal permitted? | @@ -407,3 +455,17 @@ speed claim** is made. Verified: `python -m pytest tests/test_dsl/test_solver_support.py tests/test_dsl/test_solver_state.py tests/test_models/test_compiler_decode.py -q` (92 passed) and `python -m scripts.repo_policy`. + +2026-07-17 — VSS1-01 / SLM-61 implements certificate-checked exact closure +(`dsl/solver/closure.py`): the deterministic monotone fixed point that orchestrates +the VSS0-04 oracle and removes only replay-valid `UNSUPPORTED` candidates, with +pass-consistent application, stale/tampered-proof rejection, certified bottom, and +honest partial-budget stops. Pinned by tiny closed fixtures +(`tests/test_dsl/test_solver_closure.py`): multi-pass propagation, `UNKNOWN`/`SUPPORTED` +retention, a forged `UNSUPPORTED` certificate leaving state identity unchanged, +all-unsupported certified bottom, budgeted partial closure, determinism, and +cache-identity. It adds no branching/decision stack, no model ranker, and no decode +integration; existing runtime paths are untouched and **no ship or speed claim** is +made. Verified: `python -m pytest tests/test_dsl/test_solver_closure.py +tests/test_dsl/test_solver_support.py -q` (31 passed) and +`python -m scripts.repo_policy`. diff --git a/src/slm_training/dsl/solver/__init__.py b/src/slm_training/dsl/solver/__init__.py index b3db1d9b..eb41629c 100644 --- a/src/slm_training/dsl/solver/__init__.py +++ b/src/slm_training/dsl/solver/__init__.py @@ -13,6 +13,16 @@ SolverBounds, SupportVerdict, ) +from slm_training.dsl.solver.closure import ( + CertifiedDeduction, + ClosureCounters, + ClosureResult, + EnumerativeSupportProvider, + SupportProvider, + WitnessRef, + default_query_order, + exact_closure, +) from slm_training.dsl.solver.support import ( EnumerativeSupportOracle, ExpandStatus, @@ -31,8 +41,12 @@ ) __all__ = [ + "CertifiedDeduction", + "ClosureCounters", + "ClosureResult", "DomainValue", "EnumerativeSupportOracle", + "EnumerativeSupportProvider", "ExpandStatus", "ExpandStep", "FiniteDomainState", @@ -45,6 +59,7 @@ "SolverBounds", "SupportCertificate", "SupportOracle", + "SupportProvider", "SupportQuery", "SupportResult", "SupportVerdict", @@ -52,6 +67,9 @@ "Verifier", "VerifyOutcome", "VerifyStatus", + "WitnessRef", "completion_forest_state", + "default_query_order", + "exact_closure", "replay_support_certificate", ] diff --git a/src/slm_training/dsl/solver/closure.py b/src/slm_training/dsl/solver/closure.py new file mode 100644 index 00000000..f968ada1 --- /dev/null +++ b/src/slm_training/dsl/solver/closure.py @@ -0,0 +1,358 @@ +"""Certificate-checked exact closure over finite domains (VSS1-01). + +`exact_closure` is a deterministic, pure orchestration layer on top of the VSS0-04 +support oracle. It repeatedly queries candidate support and removes **only** +candidates carrying a replay-valid ``UNSUPPORTED`` certificate, until it reaches a +fixed point, certified bottom, an all-singleton state, or an honest partial result +under a work budget. It never reimplements the support search; it drives a +:class:`SupportProvider` (the oracle plus its replay checker) and records every +destructive step as a :class:`CertifiedDeduction`. + +Monotonicity and honesty: + +* ``SUPPORTED`` and ``UNKNOWN`` values are always kept; only replay-valid + ``UNSUPPORTED`` values are removed. A domain becomes **certified bottom** only + when *every* value was removed with an accepted certificate. +* All deductions in one pass are computed against a single consistent pass-start + state and applied together to produce one new immutable state; the next pass + re-queries against the new fingerprint so a proof that went stale after a + reduction is never reused. +* Soft scores/logits are not accepted anywhere in this API. + +Semantics are owned by ``docs/design/verified-scope-solver.md``. +""" + +from __future__ import annotations + +import json +from dataclasses import dataclass +from typing import Any, Callable, Protocol + +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleDomain, + HoleId, + SupportVerdict, +) +from slm_training.dsl.solver.support import ( + EnumerativeSupportOracle, + ProblemExpander, + ReplayResult, + SupportCertificate, + SupportQuery, + SupportResult, + Verifier, + replay_support_certificate, +) + + +def _canonical_json(value: Any) -> str: + return json.dumps( + value, allow_nan=False, ensure_ascii=False, separators=(",", ":"), sort_keys=True + ) + + +# --------------------------------------------------------------------------- # +# Provider seam: an oracle that can also replay its own certificates +# --------------------------------------------------------------------------- # + + +class SupportProvider(Protocol): + """A support oracle plus its replay checker and a stable backend version.""" + + @property + def backend_version(self) -> str: ... + + def check(self, state: FiniteDomainState, query: SupportQuery) -> SupportResult: ... + + def replay( + self, certificate: SupportCertificate, *, state: FiniteDomainState + ) -> ReplayResult: ... + + +class EnumerativeSupportProvider: + """Bundles :class:`EnumerativeSupportOracle` with certificate replay.""" + + def __init__(self, expander: ProblemExpander, verifier: Verifier) -> None: + self._expander = expander + self._verifier = verifier + self._oracle = EnumerativeSupportOracle(expander, verifier) + + @property + def backend_version(self) -> str: + return f"enumerative/{self._verifier.profile}" + + def check(self, state: FiniteDomainState, query: SupportQuery) -> SupportResult: + return self._oracle.check(state, query) + + def replay( + self, certificate: SupportCertificate, *, state: FiniteDomainState + ) -> ReplayResult: + return replay_support_certificate( + certificate, state=state, expander=self._expander, verifier=self._verifier + ) + + +# --------------------------------------------------------------------------- # +# Closure records +# --------------------------------------------------------------------------- # + + +@dataclass(frozen=True) +class WitnessRef: + """A kept ``SUPPORTED`` candidate and its certificate/witness digests.""" + + hole_id: HoleId + value: DomainValue + certificate_id: str + witness_digest: str | None + witness_source: str | None + + def to_dict(self) -> dict[str, Any]: + return { + "hole_id": self.hole_id.to_dict(), + "value": self.value.to_dict(), + "certificate_id": self.certificate_id, + "witness_digest": self.witness_digest, + "witness_source": self.witness_source, + } + + +@dataclass(frozen=True) +class CertifiedDeduction: + """One destructive domain reduction, each removal citing a certificate.""" + + before_fingerprint: str + after_fingerprint: str + hole_id: HoleId + removed: tuple[DomainValue, ...] + certificate_ids: tuple[str, ...] + reason: str + + def to_dict(self) -> dict[str, Any]: + return { + "before_fingerprint": self.before_fingerprint, + "after_fingerprint": self.after_fingerprint, + "hole_id": self.hole_id.to_dict(), + "removed": [value.to_dict() for value in self.removed], + "certificate_ids": list(self.certificate_ids), + "reason": self.reason, + } + + +@dataclass(frozen=True) +class ClosureCounters: + passes: int = 0 + support_queries: int = 0 + cache_hits: int = 0 + supported: int = 0 + unsupported: int = 0 + unknown: int = 0 + candidates_removed: int = 0 + verifier_calls: int = 0 + expanded_nodes: int = 0 + + def to_dict(self) -> dict[str, int]: + return { + "passes": self.passes, + "support_queries": self.support_queries, + "cache_hits": self.cache_hits, + "supported": self.supported, + "unsupported": self.unsupported, + "unknown": self.unknown, + "candidates_removed": self.candidates_removed, + "verifier_calls": self.verifier_calls, + "expanded_nodes": self.expanded_nodes, + } + + +@dataclass(frozen=True) +class ClosureResult: + state: FiniteDomainState + deductions: tuple[CertifiedDeduction, ...] + unknown_queries: tuple[SupportQuery, ...] + witnesses: tuple[WitnessRef, ...] + counters: ClosureCounters + reached_fixed_point: bool + stop_reason: str | None = None + + +# --------------------------------------------------------------------------- # +# Query order +# --------------------------------------------------------------------------- # + +QueryOrder = Callable[[FiniteDomainState], list[HoleDomain]] +DEFAULT_QUERY_ORDER = "smallest-domain-then-hole-id-v1" + + +def default_query_order(state: FiniteDomainState) -> list[HoleDomain]: + """Unresolved holes: smallest live domain first, then canonical ``HoleId``.""" + unresolved = [hole for hole in state.holes if len(hole.values) > 1] + return sorted(unresolved, key=lambda hole: (len(hole.values), hole.hole_id.sort_key)) + + +class _MutCounters: + __slots__ = ( + "passes", "support_queries", "cache_hits", "supported", "unsupported", + "unknown", "candidates_removed", "verifier_calls", "expanded_nodes", + ) + + def __init__(self) -> None: + for name in self.__slots__: + setattr(self, name, 0) + + def snapshot(self) -> ClosureCounters: + return ClosureCounters(**{name: getattr(self, name) for name in self.__slots__}) + + +def _cache_key( + state: FiniteDomainState, hole_id: HoleId, value: DomainValue, backend_version: str +) -> str: + # state.fingerprint already subsumes pack/constraint/bounds/hole domains. + return _canonical_json( + [state.fingerprint, hole_id.to_dict(), value.to_dict(), backend_version] + ) + + +# --------------------------------------------------------------------------- # +# Exact closure +# --------------------------------------------------------------------------- # + + +def exact_closure( + state: FiniteDomainState, + provider: SupportProvider, + *, + query_order: QueryOrder = default_query_order, + cache: dict[str, SupportResult] | None = None, + certificate_store: dict[str, SupportCertificate] | None = None, + max_queries: int | None = None, +) -> ClosureResult: + """Deterministic monotone fixed point that removes only certified candidates.""" + if not isinstance(state, FiniteDomainState): + raise ValueError("exact_closure requires a FiniteDomainState") + counters = _MutCounters() + deductions: list[CertifiedDeduction] = [] + unknown_queries: list[SupportQuery] = [] + witnesses: list[WitnessRef] = [] + current = state + stop_reason: str | None = None + reached = False + + while True: + if current.is_bottom: + reached = True # certified bottom (only certified removals got us here) + break + ordered = query_order(current) + if not ordered: # every domain singleton + reached = True + break + counters.passes += 1 + pass_removals: dict[HoleId, tuple[tuple[DomainValue, ...], tuple[str, ...]]] = {} + budget_hit = False + + for hole in ordered: + removed: list[DomainValue] = [] + cert_ids: list[str] = [] + for value in hole.values: + if max_queries is not None and counters.support_queries >= max_queries: + budget_hit = True + break + query = SupportQuery( + state_fingerprint=current.fingerprint, + hole_id=hole.hole_id, + candidate=value, + ) + key = _cache_key(current, hole.hole_id, value, provider.backend_version) + if cache is not None and key in cache: + result = cache[key] + counters.cache_hits += 1 + else: + result = provider.check(current, query) + counters.support_queries += 1 + counters.verifier_calls += result.counters.verifier_calls + counters.expanded_nodes += result.counters.nodes + if cache is not None: + cache[key] = result + + if result.verdict is SupportVerdict.SUPPORTED: + counters.supported += 1 + witnesses.append( + WitnessRef( + hole_id=hole.hole_id, + value=value, + certificate_id=result.certificate.digest, + witness_digest=result.certificate.witness_digest, + witness_source=result.certificate.witness_source, + ) + ) + if certificate_store is not None: + certificate_store[result.certificate.digest] = result.certificate + elif result.verdict is SupportVerdict.UNSUPPORTED: + counters.unsupported += 1 + # Replay/validate against the exact pre-refinement state before + # removing anything. A stale or tampered proof does not remove. + replay = provider.replay(result.certificate, state=current) + if replay.ok and replay.verdict is SupportVerdict.UNSUPPORTED: + removed.append(value) + cert_ids.append(result.certificate.digest) + if certificate_store is not None: + certificate_store[result.certificate.digest] = result.certificate + else: + counters.unknown += 1 + unknown_queries.append(query) + else: # UNKNOWN + counters.unknown += 1 + unknown_queries.append(query) + if removed: + retained = tuple(v for v in hole.values if v not in set(removed)) + pass_removals[hole.hole_id] = (tuple(removed), tuple(cert_ids)) + del retained # retained is recomputed below from the pass-start state + if budget_hit: + break + + if not pass_removals: + reached = not budget_hit + if budget_hit: + stop_reason = "budget:max_queries" + break + + # Apply every deduction against the single pass-start state. + before_fp = current.fingerprint + new_state = current + for hole_id in sorted(pass_removals, key=lambda h: h.sort_key): + removed, _cert_ids = pass_removals[hole_id] + live = current.domain(hole_id).values + retained = tuple(v for v in live if v not in set(removed)) + new_state = new_state.refine(hole_id, retained) + after_fp = new_state.fingerprint + for hole_id in sorted(pass_removals, key=lambda h: h.sort_key): + removed, cert_ids_t = pass_removals[hole_id] + counters.candidates_removed += len(removed) + deductions.append( + CertifiedDeduction( + before_fingerprint=before_fp, + after_fingerprint=after_fp, + hole_id=hole_id, + removed=removed, + certificate_ids=cert_ids_t, + reason="certified_unsupported", + ) + ) + current = new_state + + if budget_hit: + stop_reason = "budget:max_queries" + reached = False + break + + return ClosureResult( + state=current, + deductions=tuple(deductions), + unknown_queries=tuple(unknown_queries), + witnesses=tuple(witnesses), + counters=counters.snapshot(), + reached_fixed_point=reached, + stop_reason=stop_reason, + ) diff --git a/tests/test_dsl/test_solver_closure.py b/tests/test_dsl/test_solver_closure.py new file mode 100644 index 00000000..ee2d6a22 --- /dev/null +++ b/tests/test_dsl/test_solver_closure.py @@ -0,0 +1,329 @@ +"""VSS1-01 (SLM-61): certificate-checked exact closure over finite domains. + +Closure is a pure orchestration layer over the VSS0-04 oracle, so it is tested +against a stub :class:`SupportProvider` whose verdicts are an exact function of the +current state — this pins multi-pass propagation, stale/tampered-certificate +rejection, certified bottom, partial-budget stops, determinism, and cache identity +without depending on the oracle's search. Torch-free. +""" + +from __future__ import annotations + +import hashlib +import inspect + +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleDomain, + HoleId, + SolverBounds, + SupportVerdict, +) +from slm_training.dsl.solver.support import ( + ReplayResult, + SupportCertificate, + SupportQuery, + SupportResult, + SearchCounters, +) +from slm_training.dsl.solver.closure import ( + CertifiedDeduction, + ClosureResult, + WitnessRef, + default_query_order, + exact_closure, +) + +_BOUNDS = SolverBounds( + max_tokens=1000, max_nodes=1000, max_depth=32, max_backtracks=1000, + max_verifier_calls=1000, +) + + +def _sha(text: str) -> str: + return hashlib.sha256(text.encode()).hexdigest() + + +def _val(name: str) -> DomainValue: + return DomainValue.create("v", {"v": name}) + + +def _hole(name: str) -> HoleId: + return HoleId(namespace="closure-test", path=(name,), kind="slot") + + +def _state(domains: dict[str, list[str]], *, constraint_version: str = "v1") -> FiniteDomainState: + holes = tuple( + HoleDomain(_hole(name), tuple(_val(v) for v in values)) + for name, values in domains.items() + ) + return FiniteDomainState( + problem_id="closure-test", + pack_id="fixture", + constraint_version=constraint_version, + bounds=_BOUNDS, + holes=holes, + ) + + +class _RuleProvider: + """Stub oracle whose verdict is an exact function of the current state. + + Certificates are canonical for ``(state, query, verdict)``, so an honest + replay reproduces them and any tamper/stale mismatch is caught. + """ + + def __init__(self, rule, *, profile: str = "stub-v1"): + self._rule = rule + self._profile = profile + + @property + def backend_version(self) -> str: + return f"stub/{self._profile}" + + def _cert(self, state, query, verdict) -> SupportCertificate: + common = dict( + schema_version=1, query=query, verdict=verdict, + problem_id=state.problem_id, pack_id=state.pack_id, + constraint_version=state.constraint_version, bounds=state.bounds, + search_order="canonical-domain-value-v1", + explored_state_fingerprints=(), verifier_profile=self._profile, + ) + if verdict is SupportVerdict.UNSUPPORTED: + return SupportCertificate( + **common, coverage_observations=("complete",), exhausted=True, + ) + if verdict is SupportVerdict.SUPPORTED: + witness = f"witness:{query.candidate.payload_json}" + return SupportCertificate( + **common, coverage_observations=("complete",), + witness_source="stub", witness_digest=_sha(witness), exhausted=False, + ) + return SupportCertificate( + **common, coverage_observations=("partial",), exhausted=False, + stop_reason="incomplete", + ) + + def check(self, state, query) -> SupportResult: + verdict = self._rule(state, query.hole_id, query.candidate) + cert = self._cert(state, query, verdict) + witness = ( + f"witness:{query.candidate.payload_json}" + if verdict is SupportVerdict.SUPPORTED + else None + ) + return SupportResult(verdict, cert, witness=witness, counters=SearchCounters(nodes=1)) + + def replay(self, certificate, *, state) -> ReplayResult: + violations: list[str] = [] + if state.fingerprint != certificate.query.state_fingerprint: + violations.append("stale fingerprint") + recomputed = self._rule(state, certificate.query.hole_id, certificate.query.candidate) + if recomputed != certificate.verdict: + violations.append("verdict changed") + if certificate.verdict is SupportVerdict.UNSUPPORTED: + if not certificate.exhausted: + violations.append("not exhausted") + if any(c in {"partial", "none"} for c in certificate.coverage_observations): + violations.append("incomplete coverage") + expected = self._cert(state, certificate.query, recomputed) + if expected.digest != certificate.digest: + violations.append("digest mismatch") + return ReplayResult(ok=not violations, verdict=certificate.verdict, violations=tuple(violations)) + + +def _v(value: DomainValue) -> str: + return value.payload["v"] + + +# --------------------------------------------------------------------------- # +# Multi-pass propagation +# --------------------------------------------------------------------------- # + + +def _propagation_rule(state, hole_id, value): + name = _v(value) + if name in {"a1", "b1"}: + return SupportVerdict.UNSUPPORTED + if name in {"a3", "b2"}: + return SupportVerdict.SUPPORTED + if name == "a2": + b = next(h for h in state.holes if h.hole_id == _hole("B")) + b1_present = any(_v(dv) == "b1" for dv in b.values) + return SupportVerdict.UNKNOWN if b1_present else SupportVerdict.UNSUPPORTED + return SupportVerdict.UNKNOWN + + +def test_multipass_propagation_removes_only_after_earlier_reduction(): + state = _state({"A": ["a1", "a2", "a3"], "B": ["b1", "b2"]}) + result = exact_closure(state, _RuleProvider(_propagation_rule)) + assert result.reached_fixed_point + live = {h.hole_id.path[0]: sorted(_v(v) for v in h.values) for h in result.state.holes} + assert live == {"A": ["a3"], "B": ["b2"]} + # a2 was removed in a *later* pass than a1/b1 (needs >= 2 passes). + assert result.counters.passes >= 2 + # a2 was UNKNOWN in pass 1 and UNSUPPORTED in pass 2 -> it appears in a later + # deduction, and was recorded unknown at least once. + removed_names = {_v(v) for d in result.deductions for v in d.removed} + assert removed_names == {"a1", "b1", "a2"} + assert any(q.candidate.payload["v"] == "a2" for q in result.unknown_queries) + # SUPPORTED witnesses are kept and recorded. + assert {w.value.payload["v"] for w in result.witnesses} >= {"a3", "b2"} + + +def test_every_removed_value_has_a_certificate_and_state_is_subset(): + state = _state({"A": ["a1", "a2", "a3"], "B": ["b1", "b2"]}) + result = exact_closure(state, _RuleProvider(_propagation_rule)) + orig = {_v(v) for h in state.holes for v in h.values} + kept = {_v(v) for h in result.state.holes for v in h.values} + assert kept <= orig # monotone subset + for deduction in result.deductions: + assert len(deduction.certificate_ids) == len(deduction.removed) + assert all(cid for cid in deduction.certificate_ids) + + +# --------------------------------------------------------------------------- # +# Honesty: UNKNOWN never removes; tampered / stale proofs never mutate state +# --------------------------------------------------------------------------- # + + +def test_unknown_and_supported_are_kept(): + # Everything is UNKNOWN or SUPPORTED -> no removals, immediate fixed point. + def rule(state, hole_id, value): + return SupportVerdict.SUPPORTED if _v(value) == "keep" else SupportVerdict.UNKNOWN + + state = _state({"A": ["keep", "maybe", "dunno"]}) + result = exact_closure(state, _RuleProvider(rule)) + assert result.reached_fixed_point + assert result.state == state # unchanged + assert not result.deductions + assert result.counters.candidates_removed == 0 + + +def test_tampered_unsupported_certificate_cannot_change_state(): + # Verdict says UNSUPPORTED but the certificate is forged (exhausted=False), + # so replay fails and nothing is removed. + class _Dishonest(_RuleProvider): + def check(self, state, query): + result = super().check(state, query) + if result.verdict is SupportVerdict.UNSUPPORTED: + from dataclasses import replace + forged = replace(result.certificate, exhausted=False) + return SupportResult(result.verdict, forged, counters=result.counters) + return result + + state = _state({"A": ["a1", "a3"]}) # a1 unsupported, a3 supported + result = exact_closure(state, _Dishonest(_propagation_rule)) + assert result.state == state # identity unchanged + assert not result.deductions + # The value was seen as unsupported but demoted to unknown because replay failed. + assert result.counters.candidates_removed == 0 + assert any(q.candidate.payload["v"] == "a1" for q in result.unknown_queries) + + +def test_stale_certificate_is_rejected_by_replay(): + provider = _RuleProvider(_propagation_rule) + s0 = _state({"A": ["a1", "a3"], "B": ["b1", "b2"]}) + query = SupportQuery(s0.fingerprint, _hole("A"), _val("a1")) + result = provider.check(s0, query) + # Replay the s0 certificate against a *different* state -> stale. + s1 = _state({"A": ["a1", "a3"], "B": ["b2"]}) + replay = provider.replay(result.certificate, state=s1) + assert not replay.ok + assert any("stale" in v for v in replay.violations) + + +# --------------------------------------------------------------------------- # +# Certified bottom + partial budget +# --------------------------------------------------------------------------- # + + +def test_all_unsupported_yields_certified_bottom(): + def rule(state, hole_id, value): + return SupportVerdict.UNSUPPORTED + + state = _state({"A": ["a1", "a2"]}) + result = exact_closure(state, _RuleProvider(rule)) + assert result.state.is_bottom + assert result.reached_fixed_point + assert result.counters.candidates_removed == 2 + + +def test_partial_budget_stops_with_live_domains(): + def rule(state, hole_id, value): + return SupportVerdict.UNSUPPORTED if _v(value) == "a1" else SupportVerdict.UNKNOWN + + state = _state({"A": ["a1", "a2", "a3"], "B": ["b1", "b2", "b3"]}) + result = exact_closure(state, _RuleProvider(rule), max_queries=1) + assert not result.reached_fixed_point + assert result.stop_reason == "budget:max_queries" + assert result.counters.support_queries <= 1 + # Domains remain live. + assert any(len(h.values) > 1 for h in result.state.holes) + + +# --------------------------------------------------------------------------- # +# Determinism + cache identity +# --------------------------------------------------------------------------- # + + +def test_closure_is_deterministic(): + state = _state({"A": ["a1", "a2", "a3"], "B": ["b1", "b2"]}) + a = exact_closure(state, _RuleProvider(_propagation_rule)) + b = exact_closure(state, _RuleProvider(_propagation_rule)) + assert a.state == b.state + assert [d.to_dict() for d in a.deductions] == [d.to_dict() for d in b.deductions] + assert a.counters.to_dict() == b.counters.to_dict() + + +def test_cache_reuses_results_by_full_identity(): + state = _state({"A": ["a1", "a2", "a3"], "B": ["b1", "b2"]}) + cache: dict = {} + first = exact_closure(state, _RuleProvider(_propagation_rule), cache=cache) + assert first.counters.cache_hits == 0 + # A second closure over the same state + a shared cache reuses stored results. + second = exact_closure(state, _RuleProvider(_propagation_rule), cache=cache) + assert second.counters.cache_hits > 0 + assert second.state == first.state + # A different backend version must miss the cache (identity includes it). + third = exact_closure( + state, _RuleProvider(_propagation_rule, profile="other-vX"), cache=cache + ) + assert third.counters.support_queries > 0 + + +def test_default_query_order_is_smallest_domain_first(): + state = _state({"A": ["a1", "a2", "a3"], "B": ["b1", "b2"], "C": ["c1"]}) + order = default_query_order(state) + names = [h.hole_id.path[0] for h in order] + assert names == ["B", "A"] # C is singleton (resolved), B(2) before A(3) + + +def test_certificate_store_collects_full_certificates(): + state = _state({"A": ["a1", "a3"]}) + store: dict = {} + result = exact_closure(state, _RuleProvider(_propagation_rule), certificate_store=store) + # Every deduction certificate id resolves to a stored full certificate. + for deduction in result.deductions: + for cid in deduction.certificate_ids: + assert cid in store + assert store[cid].digest == cid + + +def test_records_round_trip_json(): + state = _state({"A": ["a1", "a3"], "B": ["b1", "b2"]}) + result = exact_closure(state, _RuleProvider(_propagation_rule)) + import json + + for deduction in result.deductions: + blob = json.dumps(deduction.to_dict(), sort_keys=True) + assert "before_fingerprint" in json.loads(blob) + for witness in result.witnesses: + assert "certificate_id" in witness.to_dict() + + +def test_solver_closure_is_torch_free(): + import slm_training.dsl.solver.closure as closure_mod + + assert "torch" not in inspect.getsource(closure_mod) From 095581c96f6715f7c56a77c48c7dc590b29e0e8e Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 23:57:30 +0000 Subject: [PATCH 6/9] Remove unused test imports to satisfy ruff (SLM-61) The prior commit staged the test file before the F401 unused-import fix was applied, so CI's `ruff check .` failed on CertifiedDeduction/ClosureResult/ WitnessRef. Drop them; only default_query_order and exact_closure are used. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt --- tests/test_dsl/test_solver_closure.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/tests/test_dsl/test_solver_closure.py b/tests/test_dsl/test_solver_closure.py index ee2d6a22..eca7d24e 100644 --- a/tests/test_dsl/test_solver_closure.py +++ b/tests/test_dsl/test_solver_closure.py @@ -28,9 +28,6 @@ SearchCounters, ) from slm_training.dsl.solver.closure import ( - CertifiedDeduction, - ClosureResult, - WitnessRef, default_query_order, exact_closure, ) From d6ee8d74eaa187ec92c6906cb39647d1139af6a5 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 18 Jul 2026 00:09:04 +0000 Subject: [PATCH 7/9] Add bounded proof-carrying search controller (SLM-62) VSS1-02: implement the deterministic search controller that alternates exact closure (irreversible, certificate-backed deletion) with reversible branching (rankers order only, never membership). Torch-free, not wired into decode, no ship claim. The generic controller is the new owner; LatticeSearchState is retained unchanged as the compiler-forest adapter (documented compatibility seam). - dsl/solver/controller.py: search(state, provider, terminal_checker, *, ranker, hole_selector, ...) plus SearchStatus (SOLVED / CERTIFIED_UNSAT / UNKNOWN / BUDGET_EXHAUSTED), CandidateRanker + BaselineRanker, TerminalChecker/Outcome, SearchDecision, Nogood, SearchResult. Smallest-domain-first hole selection; ranker permutation validated (missing/extra/duplicate rejected); local nogoods are request-local and never serialized as certified deductions; CERTIFIED_UNSAT only when the whole finite tree closes by certified deductions with no UNKNOWN/verifier-rejection/budget truncation; every SOLVED carries a verifier report; budgets return UNKNOWN/BUDGET_EXHAUSTED, never unsat. - tests/test_dsl/test_solver_controller.py: tiny fixtures for deductions-before- decision, solve after one/many decisions, rollback-to-alternate, certified unsat vs unknown-prevents-unsat, terminal-verifier-failure backtrack, nogood-not-a- deduction, ranker permutation validation, adversarial-ranker membership safety, determinism, and budget stops. - solver/__init__ exports; docs add the search state machine + the certified- deduction/reversible-decision/local-nogood/certified-contradiction/timeout table to verified-scope-solver.md and a controller note to lattice-recursive-search.md. Verified: pytest test_solver_controller.py test_lattice_search.py + full solver suite (94 passed), full-repo ruff, repo_policy, git diff --check. Stacked on SLM-61. The lattice-search compatibility tests pass unchanged. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt --- docs/design/lattice-recursive-search.md | 15 + docs/design/verified-scope-solver.md | 58 ++++ src/slm_training/dsl/solver/__init__.py | 22 ++ src/slm_training/dsl/solver/controller.py | 401 ++++++++++++++++++++++ tests/test_dsl/test_solver_controller.py | 292 ++++++++++++++++ 5 files changed, 788 insertions(+) create mode 100644 src/slm_training/dsl/solver/controller.py create mode 100644 tests/test_dsl/test_solver_controller.py diff --git a/docs/design/lattice-recursive-search.md b/docs/design/lattice-recursive-search.md index 950a9137..23cb70c8 100644 --- a/docs/design/lattice-recursive-search.md +++ b/docs/design/lattice-recursive-search.md @@ -66,6 +66,21 @@ extendable therefore never authorizes removal; only a replayed support certifica does. The oracle is not wired into decode, so this section changes no runtime behavior. +### Proof-carrying search controller (VSS1-02) + +[`dsl/solver/controller.py`](../../src/slm_training/dsl/solver/controller.py) +generalizes this hard/soft split into a bounded controller: exact closure owns +irreversible certificate-backed deletion, a `CandidateRanker` orders only the live +values (never adds/drops one), and reversible decisions plus local nogoods drive +bounded backtracking. It terminates as `SOLVED` (with a final verifier report), +`CERTIFIED_UNSAT` (only when the whole finite tree closes by certified deductions +with no UNKNOWN/verifier-rejection/budget truncation), or `UNKNOWN` / +`BUDGET_EXHAUSTED`. This is the new generic owner; `LatticeSearchState` here is the +retained compiler-forest adapter and is unchanged. The full state machine and the +certified-deduction / reversible-decision / local-nogood / certified-contradiction / +timeout table live in +[verified-scope-solver.md](verified-scope-solver.md). Not wired into decode. + ## Campaign design (V9) The registered runnable rows are hypotheses, not results. The matched controls separate the diff --git a/docs/design/verified-scope-solver.md b/docs/design/verified-scope-solver.md index 55f0c9a2..3e371458 100644 --- a/docs/design/verified-scope-solver.md +++ b/docs/design/verified-scope-solver.md @@ -244,6 +244,48 @@ def exact_closure(state, provider): stores certificate **references** (digests) plus compact summaries; full certificates live in a caller-provided `certificate_store`. +## Implemented search controller (VSS1-02 / SLM-62) + +[`dsl/solver/controller.py`](../../src/slm_training/dsl/solver/controller.py) adds +`search(state, provider, terminal_checker, *, ranker, hole_selector, ...)`: a +bounded controller that alternates exact closure with reversible branching. It is +the new **generic** owner; the compiler-forest search `LatticeSearchState` +(`fastpath/lattice_search.py`) is retained unchanged as the forest-specific adapter +(its callers/tests are untouched — the documented compatibility seam). + +State machine (deterministic; a `CandidateRanker` orders live values only): + +```text +loop: + closure = exact_closure(state) # certified, irreversible deletions + if state is ⊥: # closure emptied a domain (all certified) + backtrack; at level 0 and no uncertified branch -> CERTIFIED_UNSAT + elif structurally solved: + out = terminal_checker(state) # materialize + final pack verifier + if out.accepted: return SOLVED(out.report) # never SOLVED without a report + else: record nogood; backtrack # verifier reject is a conflict, not solved + else: + hole = smallest live domain # then HoleId (deterministic) + order = ranker.rank(state, hole, live) # REQUIRED: a permutation of live values + apply order[0] as a reversible decision; push the rest on the trail + budgets (nodes / backtracks / decisions) -> UNKNOWN | BUDGET_EXHAUSTED, never unsat +``` + +Five distinct outcomes the controller keeps separate: + +| Concept | Reversible? | Proof status | +| --- | --- | --- | +| **certified deduction** | No | `exact_closure` removal with a replay-valid `UNSUPPORTED` certificate. | +| **reversible decision** | Yes | A ranker-ordered live value on the trail; undone on backtrack. Creates no legality. | +| **local nogood** | Yes (request-local) | A conflict record (`certified_bottom` / `terminal_verifier_failure` / budget). **Never** a certified deduction unless a later support query certifies it. | +| **certificate-backed global contradiction** | No | `CERTIFIED_UNSAT` — the whole finite tree closed by certified deductions with **no** UNKNOWN, verifier-rejection, or budget truncation anywhere. | +| **timeout / unknown** | — | `UNKNOWN` / `BUDGET_EXHAUSTED`. A budget or capability limit is never relabeled `CERTIFIED_UNSAT`. | + +Soundness: a learned/adversarial ranker cannot alter live hard membership (the +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. + ## Reference support semantics | Verdict | Requirement | Removal permitted? | @@ -469,3 +511,19 @@ integration; existing runtime paths are untouched and **no ship or speed claim** made. Verified: `python -m pytest tests/test_dsl/test_solver_closure.py tests/test_dsl/test_solver_support.py -q` (31 passed) and `python -m scripts.repo_policy`. + +2026-07-18 — VSS1-02 / SLM-62 implements the bounded proof-carrying search +controller (`dsl/solver/controller.py`): closure + reversible branching with a +soft-only `CandidateRanker`, local nogoods, and sound `SOLVED` / +`CERTIFIED_UNSAT` / `UNKNOWN` / `BUDGET_EXHAUSTED` termination. The generic +controller is the new owner; `LatticeSearchState` is retained unchanged as the +compiler-forest adapter (compatibility seam). Pinned by tiny closed fixtures +(`tests/test_dsl/test_solver_controller.py`): certified deductions before the first +decision, solve after one/many decisions, rollback to an alternate, root +`CERTIFIED_UNSAT` only when every branch is proof-closed, UNKNOWN/verifier-rejection +preventing certified unsat, ranker permutation validation (an adversarial ranker +cannot alter hard membership), determinism, and budget stops. No TwoTower/diffusion +integration, no learned energy, no persistent clause DB, and **no ship claim**. +Verified: `python -m pytest tests/test_dsl/test_solver_controller.py +tests/test_dsl/test_lattice_search.py -q` (94 in the full solver+compat suite) and +`python -m scripts.repo_policy`. diff --git a/src/slm_training/dsl/solver/__init__.py b/src/slm_training/dsl/solver/__init__.py index eb41629c..cb91a09b 100644 --- a/src/slm_training/dsl/solver/__init__.py +++ b/src/slm_training/dsl/solver/__init__.py @@ -13,6 +13,18 @@ SolverBounds, SupportVerdict, ) +from slm_training.dsl.solver.controller import ( + BaselineRanker, + CandidateRanker, + Nogood, + SearchDecision, + SearchResult, + SearchStatus, + TerminalChecker, + TerminalOutcome, + default_hole_selector, + search, +) from slm_training.dsl.solver.closure import ( CertifiedDeduction, ClosureCounters, @@ -41,10 +53,20 @@ ) __all__ = [ + "BaselineRanker", + "CandidateRanker", "CertifiedDeduction", "ClosureCounters", "ClosureResult", "DomainValue", + "Nogood", + "SearchDecision", + "SearchResult", + "SearchStatus", + "TerminalChecker", + "TerminalOutcome", + "default_hole_selector", + "search", "EnumerativeSupportOracle", "EnumerativeSupportProvider", "ExpandStatus", diff --git a/src/slm_training/dsl/solver/controller.py b/src/slm_training/dsl/solver/controller.py new file mode 100644 index 00000000..a01bb96c --- /dev/null +++ b/src/slm_training/dsl/solver/controller.py @@ -0,0 +1,401 @@ +"""Bounded proof-carrying search controller (VSS1-02). + +Alternates exact closure (irreversible, certificate-backed candidate deletion) +with reversible branching (rankers choose only order, never membership). It keeps +the repository's hard/soft separation strict: + +* **Certified deduction** — a domain reduction produced by `exact_closure`, each + removal citing a replay-valid `UNSUPPORTED` certificate. Irreversible. +* **Reversible decision** — a chosen live value recorded on a decision stack and + undone on backtracking. A `CandidateRanker` only permutes the exact live values; + it can neither add nor drop a candidate. +* **Local nogood** — a request-local record that a decision branch conflicted. It + is **not** a certified deduction and is never serialized as one. +* **Certificate-backed global contradiction** — `CERTIFIED_UNSAT`, returned only + when the whole finite tree closes by certified deductions with no UNKNOWN, + verifier-rejection, or budget truncation anywhere. +* **Timeout / unknown** — `UNKNOWN` / `BUDGET_EXHAUSTED`, never relabeled unsat. + +Ownership: this is the new generic controller. The existing compiler-forest search +`LatticeSearchState` (`fastpath/lattice_search.py`) is retained unchanged as the +forest-specific adapter; its callers and tests are untouched. Semantics are owned +by ``docs/design/verified-scope-solver.md``. +""" + +from __future__ import annotations + +import json +from dataclasses import dataclass +from enum import Enum +from typing import Any, Protocol + +from slm_training.dsl.solver.closure import ( + CertifiedDeduction, + SupportProvider, + exact_closure, +) +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleId, + SolverBounds, +) +from slm_training.dsl.solver.support import SearchCounters, SupportCertificate + +JsonValue = Any + + +def _canonical_json(value: Any) -> str: + return json.dumps( + value, allow_nan=False, ensure_ascii=False, separators=(",", ":"), sort_keys=True + ) + + +class SearchStatus(str, Enum): + SOLVED = "solved" + CERTIFIED_UNSAT = "certified_unsat" + UNKNOWN = "unknown" + BUDGET_EXHAUSTED = "budget_exhausted" + + +# --------------------------------------------------------------------------- # +# Injected seams: ranker (soft) and terminal checker (final verifier) +# --------------------------------------------------------------------------- # + + +class CandidateRanker(Protocol): + """Orders the exact live values for a hole; never adds or drops a value.""" + + @property + def ranker_id(self) -> str: ... + + def rank( + self, state: FiniteDomainState, hole_id: HoleId, values: tuple[DomainValue, ...] + ) -> tuple[DomainValue, ...]: ... + + +class BaselineRanker: + """Deterministic identity ordering (values arrive canonically ordered).""" + + @property + def ranker_id(self) -> str: + return "baseline-canonical-v1" + + def rank( + self, state: FiniteDomainState, hole_id: HoleId, values: tuple[DomainValue, ...] + ) -> tuple[DomainValue, ...]: + return tuple(values) + + +@dataclass(frozen=True) +class TerminalOutcome: + """Result of materializing + verifying a structurally-solved state.""" + + accepted: bool + source: str | None = None + report: JsonValue | None = None + detail: str = "" + + +class TerminalChecker(Protocol): + """Materializes a structurally-solved state and runs the final verifier.""" + + def check(self, state: FiniteDomainState) -> TerminalOutcome: ... + + +# --------------------------------------------------------------------------- # +# Records +# --------------------------------------------------------------------------- # + + +@dataclass(frozen=True) +class SearchDecision: + decision_id: str + before_fingerprint: str + after_fingerprint: str + level: int + hole_id: HoleId + chosen: DomainValue + alternatives: tuple[DomainValue, ...] + ranker_id: str + + def to_dict(self) -> dict[str, Any]: + return { + "decision_id": self.decision_id, + "before_fingerprint": self.before_fingerprint, + "after_fingerprint": self.after_fingerprint, + "level": self.level, + "hole_id": self.hole_id.to_dict(), + "chosen": self.chosen.to_dict(), + "alternatives": [value.to_dict() for value in self.alternatives], + "ranker_id": self.ranker_id, + } + + +@dataclass(frozen=True) +class Nogood: + """A request-local conflict record; NOT a certified deduction.""" + + problem_id: str + constraint_version: str + bounds: SolverBounds + assignment: tuple[tuple[HoleId, DomainValue], ...] + provenance: str + + def to_dict(self) -> dict[str, Any]: + return { + "problem_id": self.problem_id, + "constraint_version": self.constraint_version, + "bounds": self.bounds.to_dict(), + "assignment": [ + [hole.to_dict(), value.to_dict()] for hole, value in self.assignment + ], + "provenance": self.provenance, + } + + @property + def key(self) -> str: + return _canonical_json( + { + "problem_id": self.problem_id, + "constraint_version": self.constraint_version, + "bounds": self.bounds.to_dict(), + "assignment": [ + [hole.to_dict(), value.to_dict()] for hole, value in self.assignment + ], + } + ) + + +@dataclass(frozen=True) +class SearchResult: + status: SearchStatus + state: FiniteDomainState + source: str | None + verifier_report: JsonValue | None + deductions: tuple[CertifiedDeduction, ...] + decisions: tuple[SearchDecision, ...] + nogoods: tuple[Nogood, ...] + counters: SearchCounters + stop_reason: str | None = None + + +def default_hole_selector(state: FiniteDomainState) -> HoleId | None: + """Smallest live domain first, then canonical ``HoleId`` (deterministic).""" + unresolved = [hole for hole in state.holes if len(hole.values) > 1] + if not unresolved: + return None + best = min(unresolved, key=lambda hole: (len(hole.values), hole.hole_id.sort_key)) + return best.hole_id + + +def _validate_permutation( + permuted: tuple[DomainValue, ...], values: tuple[DomainValue, ...] +) -> None: + live = set(values) + seen = set(permuted) + if len(permuted) != len(values): + raise ValueError("ranker returned a different candidate count") + if len(seen) != len(permuted): + raise ValueError("ranker returned a duplicate candidate") + if seen != live: + missing = live - seen + extra = seen - live + raise ValueError( + f"ranker altered live candidates (missing={len(missing)}, extra={len(extra)})" + ) + + +@dataclass +class _Frame: + pre_state: FiniteDomainState + hole_id: HoleId + chosen: DomainValue + remaining: list[DomainValue] + level: int + + +@dataclass +class _Mut: + nodes: int = 0 + backtracks: int = 0 + verifier_calls: int = 0 + decisions: int = 0 + support_queries: int = 0 + + def counters(self) -> SearchCounters: + return SearchCounters( + nodes=self.nodes, + tokens=self.support_queries, + depth=self.decisions, + backtracks=self.backtracks, + verifier_calls=self.verifier_calls, + ) + + +def search( + state: FiniteDomainState, + provider: SupportProvider, + terminal_checker: TerminalChecker, + *, + ranker: CandidateRanker | None = None, + hole_selector=default_hole_selector, + cache: dict[str, Any] | None = None, + certificate_store: dict[str, SupportCertificate] | None = None, + max_decisions: int = 10_000, + max_backtracks: int | None = None, +) -> SearchResult: + """Bounded closure + reversible branching; sound tri-state termination.""" + if not isinstance(state, FiniteDomainState): + raise ValueError("search requires a FiniteDomainState") + ranker = ranker or BaselineRanker() + if max_backtracks is None: + max_backtracks = state.bounds.max_backtracks + counters = _Mut() + deductions: list[CertifiedDeduction] = [] + decisions: list[SearchDecision] = [] + nogoods: list[Nogood] = [] + stack: list[_Frame] = [] + current = state + level = 0 + # Any non-certified reason a branch closed (UNKNOWN closure, verifier rejection, + # budget) means the tree is not fully proof-closed -> UNSAT cannot be certified. + saw_uncertified = False + + def record_nogood(hole_id: HoleId, value: DomainValue, provenance: str) -> None: + nogood = Nogood( + problem_id=current.problem_id, + constraint_version=current.constraint_version, + bounds=current.bounds, + assignment=((hole_id, value),), + provenance=provenance, + ) + if all(existing.key != nogood.key for existing in nogoods): + nogoods.append(nogood) + + def backtrack(provenance: str) -> bool: + """Restore the latest pre-decision state and take the next alternative.""" + nonlocal current, level + while stack: + frame = stack[-1] + counters.backtracks += 1 + record_nogood(frame.hole_id, frame.chosen, provenance) + if counters.backtracks > max_backtracks: + return False + if frame.remaining: + frame.chosen = frame.remaining.pop(0) + current = frame.pre_state.with_decision(frame.hole_id, frame.chosen) + level = frame.level + 1 + # The alternative is a fresh decision at the same point; log it so + # the whole trajectory (including backtracked attempts) replays. + counters.decisions += 1 + decisions.append( + SearchDecision( + decision_id=f"d{counters.decisions}", + before_fingerprint=frame.pre_state.fingerprint, + after_fingerprint=current.fingerprint, + level=level, + hole_id=frame.hole_id, + chosen=frame.chosen, + alternatives=tuple(frame.remaining), + ranker_id=ranker.ranker_id, + ) + ) + return True + stack.pop() + return False + + while True: + closure = exact_closure( + current, provider, cache=cache, certificate_store=certificate_store + ) + deductions.extend(closure.deductions) + counters.nodes += 1 + counters.verifier_calls += closure.counters.verifier_calls + counters.support_queries += closure.counters.support_queries + current = closure.state + # A closure that left unknowns or was budget-truncated cannot license unsat. + if closure.unknown_queries or not closure.reached_fixed_point: + saw_uncertified = True + + if current.is_bottom: + # Certified bottom: closure removes only certified-unsupported values. + if not backtrack("certified_bottom"): + status = ( + SearchStatus.CERTIFIED_UNSAT + if not saw_uncertified + else SearchStatus.UNKNOWN + ) + return _result(status, current, None, None, deductions, decisions, + nogoods, counters, + None if status is SearchStatus.CERTIFIED_UNSAT + else "exhausted_with_unknown") + continue + + if current.is_structurally_solved: + outcome = terminal_checker.check(current) + counters.verifier_calls += 1 + if outcome.accepted: + return _result(SearchStatus.SOLVED, current, outcome.source, + outcome.report, deductions, decisions, nogoods, counters, + None) + # Verifier rejection is a conflict, not a certified deduction. + saw_uncertified = True + if not backtrack("terminal_verifier_failure"): + return _result(SearchStatus.UNKNOWN, current, None, outcome.report, + deductions, decisions, nogoods, counters, + "terminal_rejected_exhausted") + continue + + # Budgets before branching. + if counters.decisions >= max_decisions: + return _result(SearchStatus.BUDGET_EXHAUSTED, current, None, None, + deductions, decisions, nogoods, counters, "budget:max_decisions") + if counters.nodes > current.bounds.max_nodes: + return _result(SearchStatus.BUDGET_EXHAUSTED, current, None, None, + deductions, decisions, nogoods, counters, "budget:max_nodes") + + hole_id = hole_selector(current) + if hole_id is None: # defensive: no unresolved hole though not solved + saw_uncertified = True + if not backtrack("no_branching_hole"): + return _result(SearchStatus.UNKNOWN, current, None, None, deductions, + decisions, nogoods, counters, "no_branching_hole") + continue + live = current.domain(hole_id).values + permuted = ranker.rank(current, hole_id, live) + _validate_permutation(permuted, live) # ranker cannot alter membership + chosen, alternatives = permuted[0], permuted[1:] + pre = current + after = current.with_decision(hole_id, chosen) + counters.decisions += 1 + decisions.append( + SearchDecision( + decision_id=f"d{counters.decisions}", + before_fingerprint=pre.fingerprint, + after_fingerprint=after.fingerprint, + level=level + 1, + hole_id=hole_id, + chosen=chosen, + alternatives=alternatives, + ranker_id=ranker.ranker_id, + ) + ) + stack.append(_Frame(pre, hole_id, chosen, list(alternatives), level)) + current = after + level += 1 + + +def _result(status, state, source, report, deductions, decisions, nogoods, counters, + stop_reason) -> SearchResult: + return SearchResult( + status=status, + state=state, + source=source, + verifier_report=report, + deductions=tuple(deductions), + decisions=tuple(decisions), + nogoods=tuple(nogoods), + counters=counters.counters(), + stop_reason=stop_reason, + ) diff --git a/tests/test_dsl/test_solver_controller.py b/tests/test_dsl/test_solver_controller.py new file mode 100644 index 00000000..853bb46e --- /dev/null +++ b/tests/test_dsl/test_solver_controller.py @@ -0,0 +1,292 @@ +"""VSS1-02 (SLM-61): bounded proof-carrying search controller. + +Tiny finite problems with known branches pin the separation of certified +deductions (irreversible, closure-owned) from reversible decisions (ranker-ordered) +and local nogoods, and the sound tri-state termination: CERTIFIED_UNSAT only when +the whole tree closes by certified deductions with no UNKNOWN / verifier-rejection / +budget truncation. Torch-free. +""" + +from __future__ import annotations + +import hashlib +import inspect + +import pytest + +from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleDomain, + HoleId, + SolverBounds, + SupportVerdict, +) +from slm_training.dsl.solver.support import ( + ReplayResult, + SearchCounters, + SupportCertificate, + SupportResult, +) +from slm_training.dsl.solver.controller import ( + BaselineRanker, + SearchStatus, + TerminalOutcome, + search, +) + +_BOUNDS = SolverBounds( + max_tokens=1000, max_nodes=1000, max_depth=32, max_backtracks=1000, + max_verifier_calls=1000, +) + + +def _sha(text: str) -> str: + return hashlib.sha256(text.encode()).hexdigest() + + +def _val(name: str) -> DomainValue: + return DomainValue.create("v", {"v": name}) + + +def _hole(name: str) -> HoleId: + return HoleId(namespace="ctl-test", path=(name,), kind="slot") + + +def _state(domains: dict[str, list[str]]) -> FiniteDomainState: + holes = tuple( + HoleDomain(_hole(name), tuple(_val(v) for v in values)) + for name, values in domains.items() + ) + return FiniteDomainState( + problem_id="ctl-test", pack_id="fixture", constraint_version="v1", + bounds=_BOUNDS, holes=holes, + ) + + +def _vname(value: DomainValue) -> str: + return value.payload["v"] + + +class _RuleProvider: + """State-dependent stub oracle with canonical, replayable certificates.""" + + def __init__(self, rule, *, profile="stub-v1"): + self._rule = rule + self._profile = profile + + @property + def backend_version(self) -> str: + return f"stub/{self._profile}" + + def _cert(self, state, query, verdict) -> SupportCertificate: + common = dict( + schema_version=1, query=query, verdict=verdict, problem_id=state.problem_id, + pack_id=state.pack_id, constraint_version=state.constraint_version, + bounds=state.bounds, search_order="canonical-domain-value-v1", + explored_state_fingerprints=(), verifier_profile=self._profile, + ) + if verdict is SupportVerdict.UNSUPPORTED: + return SupportCertificate(**common, coverage_observations=("complete",), exhausted=True) + if verdict is SupportVerdict.SUPPORTED: + return SupportCertificate( + **common, coverage_observations=("complete",), witness_source="stub", + witness_digest=_sha(query.candidate.payload_json), exhausted=False, + ) + return SupportCertificate( + **common, coverage_observations=("partial",), exhausted=False, stop_reason="incomplete", + ) + + def check(self, state, query) -> SupportResult: + verdict = self._rule(state, query.hole_id, query.candidate) + return SupportResult(verdict, self._cert(state, query, verdict), counters=SearchCounters(nodes=1)) + + def replay(self, certificate, *, state) -> ReplayResult: + violations = [] + if state.fingerprint != certificate.query.state_fingerprint: + violations.append("stale") + recomputed = self._rule(state, certificate.query.hole_id, certificate.query.candidate) + if recomputed != certificate.verdict: + violations.append("verdict") + if certificate.verdict is SupportVerdict.UNSUPPORTED and not certificate.exhausted: + violations.append("not exhausted") + if self._cert(state, certificate.query, recomputed).digest != certificate.digest: + violations.append("digest") + return ReplayResult(ok=not violations, verdict=certificate.verdict, violations=tuple(violations)) + + +class _Terminal: + """Accepts a structurally-solved assignment iff `accept(assignment)` is true.""" + + def __init__(self, accept): + self._accept = accept + + def check(self, state) -> TerminalOutcome: + assignment = {h.hole_id.path[0]: _vname(h.values[0]) for h in state.holes} + ok = self._accept(assignment) + return TerminalOutcome(accepted=ok, source="fixture" if ok else None, + report={"assignment": assignment, "accepted": ok}) + + +_ALL_UNKNOWN = lambda state, hole, value: SupportVerdict.UNKNOWN # noqa: E731 +_ACCEPT_ALL = lambda assignment: True # noqa: E731 + + +def _run(domains, rule, accept, **kw): + return search(_state(domains), _RuleProvider(rule), _Terminal(accept), **kw) + + +# --------------------------------------------------------------------------- # +# Certified deductions before decisions; solving +# --------------------------------------------------------------------------- # + + +def test_exact_deductions_before_first_decision(): + def rule(state, hole, value): + return SupportVerdict.UNSUPPORTED if _vname(value) == "x_bad" else SupportVerdict.UNKNOWN + + result = _run({"X": ["x_ok", "x_bad"], "Y": ["y1", "y2"]}, rule, + lambda a: a == {"X": "x_ok", "Y": "y1"}) + assert result.status is SearchStatus.SOLVED + # x_bad was removed by closure before any decision; decisions only concern Y. + removed = {_vname(v) for d in result.deductions for v in d.removed} + assert "x_bad" in removed + assert all(d.hole_id.path[0] == "Y" for d in result.decisions) + + +def test_solve_after_one_and_multiple_decisions(): + one = _run({"X": ["x1", "x2"]}, _ALL_UNKNOWN, lambda a: a["X"] == "x1") + assert one.status is SearchStatus.SOLVED + assert one.source is not None and one.verifier_report is not None + assert len(one.decisions) == 1 + + multi = _run({"X": ["x1", "x2"], "Y": ["y1", "y2"]}, _ALL_UNKNOWN, + lambda a: a == {"X": "x1", "Y": "y1"}) + assert multi.status is SearchStatus.SOLVED + assert len(multi.decisions) == 2 + + +def test_failed_first_branch_rolls_back_to_alternate(): + # Only x2 yields an acceptable terminal; x1 is rejected -> backtrack -> x2. + result = _run({"X": ["x1", "x2"]}, _ALL_UNKNOWN, lambda a: a["X"] == "x2") + assert result.status is SearchStatus.SOLVED + assert [_vname(d.chosen) for d in result.decisions] == ["x1", "x2"] + # A local nogood was recorded for the failed x1 branch... + assert result.nogoods + assert any(_vname(v) == "x1" for ng in result.nogoods for _h, v in ng.assignment) + # ...but it is NOT a certified deduction. + removed = {_vname(v) for d in result.deductions for v in d.removed} + assert "x1" not in removed + + +# --------------------------------------------------------------------------- # +# Sound termination +# --------------------------------------------------------------------------- # + + +def test_root_certified_unsat_only_when_all_branches_proof_closed(): + result = _run({"X": ["a", "b"]}, + lambda s, h, v: SupportVerdict.UNSUPPORTED, _ACCEPT_ALL) + assert result.status is SearchStatus.CERTIFIED_UNSAT + assert result.state.is_bottom + assert result.deductions + assert not result.decisions + + +def test_unknown_branch_prevents_certified_unsat(): + # 'a' is certified-unsupported, 'b' is UNKNOWN and its terminal is rejected. + def rule(state, hole, value): + return SupportVerdict.UNSUPPORTED if _vname(value) == "a" else SupportVerdict.UNKNOWN + + result = _run({"X": ["a", "b"]}, rule, lambda a: False) # terminal rejects everything + assert result.status is SearchStatus.UNKNOWN + assert result.status is not SearchStatus.CERTIFIED_UNSAT + + +def test_terminal_verifier_failure_causes_conflict_backtrack(): + # Single value, terminal rejects it -> no alternatives -> honest UNKNOWN. + result = _run({"X": ["x1", "x2"]}, _ALL_UNKNOWN, lambda a: False) + assert result.status is SearchStatus.UNKNOWN + assert result.nogoods # verifier failures recorded as nogoods + assert all("verifier" in ng.provenance or "certified" in ng.provenance + for ng in result.nogoods) + + +# --------------------------------------------------------------------------- # +# Ranker safety +# --------------------------------------------------------------------------- # + + +class _ReverseRanker: + ranker_id = "reverse-vX" + + def rank(self, state, hole_id, values): + return tuple(reversed(values)) + + +class _DroppingRanker: + ranker_id = "drop-vX" + + def rank(self, state, hole_id, values): + return values[:-1] # drops a candidate + + +class _AddingRanker: + ranker_id = "add-vX" + + def rank(self, state, hole_id, values): + return values + (DomainValue.create("v", {"v": "phantom"}),) + + +class _DupRanker: + ranker_id = "dup-vX" + + def rank(self, state, hole_id, values): + return (values[0],) + values + + +@pytest.mark.parametrize("ranker", [_DroppingRanker(), _AddingRanker(), _DupRanker()]) +def test_ranker_that_alters_membership_is_rejected(ranker): + with pytest.raises(ValueError): + search(_state({"X": ["x1", "x2"]}), _RuleProvider(_ALL_UNKNOWN), _Terminal(_ACCEPT_ALL), + ranker=ranker) + + +def test_adversarial_but_valid_ranker_cannot_change_hard_membership(): + domains = {"X": ["x1", "x2"], "Y": ["y1", "y2"]} + accept = lambda a: a == {"X": "x2", "Y": "y2"} # noqa: E731 + baseline = search(_state(domains), _RuleProvider(_ALL_UNKNOWN), _Terminal(accept), + ranker=BaselineRanker()) + reversed_run = search(_state(domains), _RuleProvider(_ALL_UNKNOWN), _Terminal(accept), + ranker=_ReverseRanker()) + # Both reach the same verified solution; only the trajectory order differs. + assert baseline.status is reversed_run.status is SearchStatus.SOLVED + assert baseline.state == reversed_run.state + + +# --------------------------------------------------------------------------- # +# Determinism + budgets +# --------------------------------------------------------------------------- # + + +def test_deterministic_baseline_trajectory(): + domains = {"X": ["x1", "x2"], "Y": ["y1", "y2"]} + accept = lambda a: a == {"X": "x2", "Y": "y1"} # noqa: E731 + a = _run(domains, _ALL_UNKNOWN, accept) + b = _run(domains, _ALL_UNKNOWN, accept) + assert [d.to_dict() for d in a.decisions] == [d.to_dict() for d in b.decisions] + assert a.counters.to_dict() == b.counters.to_dict() + assert a.state == b.state + + +def test_decision_budget_stops_honestly(): + result = _run({"X": ["x1", "x2"], "Y": ["y1", "y2"]}, _ALL_UNKNOWN, lambda a: False, + max_decisions=1) + assert result.status is SearchStatus.BUDGET_EXHAUSTED + assert result.stop_reason == "budget:max_decisions" + + +def test_solver_controller_is_torch_free(): + import slm_training.dsl.solver.controller as controller_mod + + assert "torch" not in inspect.getsource(controller_mod) From 1ad2e31ad28b4df89abfa0574e279f57385f7bc8 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 18 Jul 2026 00:56:23 +0000 Subject: [PATCH 8/9] Integrate exact closure into compiler decode behind a flag (SLM-63) VSS1-03 wires certificate-checked exact closure into the compiler-tree / choice decode path behind a disabled-by-default feature flag. When verified_solver_decode is on, _compiler_ltr_decode_one prunes the authoritative CompletionForest to the certified live subset before any soft ranking; the model then scores only surviving candidates. - dsl/solver/decode.py: solver_prune adapts the forest to a one-hole FiniteDomainState, runs exact_closure, and removes only candidates that were certified UNSUPPORTED with a replay-valid certificate (removed = input_domain - survivors). UNKNOWN stays live (keep_and_rank); survivors keep full CompletionPath identity, forced suffixes, and forest order, so a soft ranker can never reintroduce a removed candidate. A certified bottom yields an empty forest so the existing dead-end/rollback path runs rather than an unverified fallback. Torch-free. - models/twotower.py: _solver_prune_forest builds the OpenUI expander/verifier provider and calls solver_prune; guarded by a single getattr so default decode is byte-identical. An unsupported tokenizer/pack raises a capability error instead of silently taking a weaker path. - Eight backward-compatible config fields on TwoTowerConfig and ModelBuildConfig (verified_solver_decode + solver_*), plumbed through factory.apply_runtime_overrides and scripts/evaluate_model.py; missing fields on old checkpoints default. No new model parameter. Tests: tests/test_dsl/test_solver_decode.py (Torch-free removal / keep / certified-bottom / coverage / policy) and tests/test_models/test_solver_decode_integration.py (disabled-mode byte parity, config/checkpoint round-trip, real-closure subset, capability error, seam gated by the flag). Disabled by default; the enabled path is unmeasured. No train, eval, benchmark, or checkpoint ran, and this makes no correctness, speed, or ship claim. Docs updated: verified-scope-solver.md, lattice-recursive-search.md, quality-experiment-matrix.md config glossary, MODEL_CARD.md (flag exists and is unmeasured; no checkpoint row). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt --- docs/MODEL_CARD.md | 1 + docs/design/lattice-recursive-search.md | 19 ++ docs/design/quality-experiment-matrix.md | 29 +++ docs/design/verified-scope-solver.md | 85 +++++++++ scripts/evaluate_model.py | 18 ++ src/slm_training/dsl/solver/decode.py | 93 +++++++++ .../harnesses/model_build/config.py | 9 + .../harnesses/model_build/factory.py | 22 +++ src/slm_training/models/twotower.py | 69 +++++++ tests/test_dsl/test_solver_decode.py | 152 +++++++++++++++ .../test_solver_decode_integration.py | 178 ++++++++++++++++++ 11 files changed, 675 insertions(+) create mode 100644 src/slm_training/dsl/solver/decode.py create mode 100644 tests/test_dsl/test_solver_decode.py create mode 100644 tests/test_models/test_solver_decode_integration.py diff --git a/docs/MODEL_CARD.md b/docs/MODEL_CARD.md index a745c509..be2f55b7 100644 --- a/docs/MODEL_CARD.md +++ b/docs/MODEL_CARD.md @@ -125,6 +125,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) | --- diff --git a/docs/design/lattice-recursive-search.md b/docs/design/lattice-recursive-search.md index 23cb70c8..7481dc01 100644 --- a/docs/design/lattice-recursive-search.md +++ b/docs/design/lattice-recursive-search.md @@ -81,6 +81,25 @@ certified-deduction / reversible-decision / local-nogood / certified-contradicti 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. + ## Campaign design (V9) The registered runnable rows are hypotheses, not results. The matched controls separate the diff --git a/docs/design/quality-experiment-matrix.md b/docs/design/quality-experiment-matrix.md index f613615e..9aac9a7b 100644 --- a/docs/design/quality-experiment-matrix.md +++ b/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 \ + --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: diff --git a/docs/design/verified-scope-solver.md b/docs/design/verified-scope-solver.md index 3e371458..51e7deaa 100644 --- a/docs/design/verified-scope-solver.md +++ b/docs/design/verified-scope-solver.md @@ -286,6 +286,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? | @@ -400,6 +459,7 @@ the closure. | `ChoiceTokenizer` / `ChoiceDecodeState` (`models/choice_tokenizer.py:172`/`:608`) | Grammar-closed choice IR; length-aware legality (`allowed_ids`, `exhaustive_allowed_ids`, `minimal_completion_length`). | **Retained.** The choice IR is the late-realization and verification surface. Not duplicated. | | `HoleId`, `SolverBounds`, `DomainValue`, `HoleDomain`, `FiniteDomainState` (`dsl/solver/state.py`) | Immutable JSON-safe finite-domain carrier with canonical hard-state identity and monotone operations. | **Implemented by VSS0-03.** Torch-free and not invoked by default; soft scores and proof artifacts remain outside the state. | | `completion_forest_state` (`dsl/solver/adapters.py`) | One-hole projection of full compiler completion paths plus coverage and `UNKNOWN` provenance. | **Implemented by VSS0-03.** Retains the compiler as owner; a singleton solves only the projection. | +| `solver_prune` (`dsl/solver/decode.py`), `_solver_prune_forest` (`models/twotower.py`) | Decode-time forest pruning to the certificate-checked live subset, before soft ranking. | **Implemented by VSS1-03 behind `verified_solver_decode` (default off).** Removes only replay-valid `UNSUPPORTED`; keeps `UNKNOWN`; disabled-mode decode is byte-identical. | | `verification capsule`, `proof certificate` | Not implemented yet. | **Future VSS issues.** Capsule solving and replayable proof ownership are not duplicated here. | ## End-to-end example (partial coverage → live `UNKNOWN`) @@ -527,3 +587,28 @@ integration, no learned energy, no persistent clause DB, and **no ship claim**. Verified: `python -m pytest tests/test_dsl/test_solver_controller.py tests/test_dsl/test_lattice_search.py -q` (94 in the full solver+compat suite) and `python -m scripts.repo_policy`. + +2026-07-18 — VSS1-03 / SLM-63 integrates certificate-checked exact closure into +the compiler-tree / choice decode path behind a disabled-by-default flag +(`dsl/solver/decode.py` `solver_prune`; `models/twotower.py` +`_solver_prune_forest`, called in `_compiler_ltr_decode_one` after +`build_completion_forest`). Eight backward-compatible config fields +(`verified_solver_decode` + `solver_*`) round-trip on `TwoTowerConfig` / +`ModelBuildConfig`, plumb through `factory.apply_runtime_overrides` and +`scripts/evaluate_model.py`, and default on old checkpoints; no new model +parameter. When enabled, closure runs before soft ranking and removes **only** +replay-valid `UNSUPPORTED` candidates (`removed = input_domain − survivors`); +`UNKNOWN` stays live (`keep_and_rank`); survivors keep full `CompletionPath` +identity/forced suffixes and forest order (a ranker cannot reintroduce a removed +candidate); a certified bottom yields an empty forest so the existing +dead-end/rollback path runs (never an unverified fallback); an unsupported +tokenizer/pack raises a capability error rather than silently taking a weaker +path. With the flag off the seam is skipped and decode is byte-identical. Pinned +by `tests/test_models/test_solver_decode_integration.py` (disabled parity, config +round-trip, real-closure subset, capability error, seam-gated invocation) and the +Torch-free `tests/test_dsl/test_solver_decode.py` (removal/keep/bottom/coverage). +No train/eval/benchmark/checkpoint ran; the enabled path is **unmeasured** and +makes **no correctness, speed, or ship claim**. Verified: `python -m pytest +tests/test_models/test_solver_decode_integration.py +tests/test_models/test_compiler_decode.py tests/test_dsl/test_solver_decode.py +tests/test_dsl/test_solver_controller.py -q` and `python -m scripts.repo_policy`. diff --git a/scripts/evaluate_model.py b/scripts/evaluate_model.py index 4e192a08..79c7902d 100644 --- a/scripts/evaluate_model.py +++ b/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, diff --git a/src/slm_training/dsl/solver/decode.py b/src/slm_training/dsl/solver/decode.py new file mode 100644 index 00000000..77d1e97f --- /dev/null +++ b/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 diff --git a/src/slm_training/harnesses/model_build/config.py b/src/slm_training/harnesses/model_build/config.py index 63bb9a6e..83c83685 100644 --- a/src/slm_training/harnesses/model_build/config.py +++ b/src/slm_training/harnesses/model_build/config.py @@ -120,6 +120,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 diff --git a/src/slm_training/harnesses/model_build/factory.py b/src/slm_training/harnesses/model_build/factory.py index 8f4573d6..194d2198 100644 --- a/src/slm_training/harnesses/model_build/factory.py +++ b/src/slm_training/harnesses/model_build/factory.py @@ -70,6 +70,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", @@ -293,6 +301,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 diff --git a/src/slm_training/models/twotower.py b/src/slm_training/models/twotower.py index 982b94dd..e50f2521 100644 --- a/src/slm_training/models/twotower.py +++ b/src/slm_training/models/twotower.py @@ -279,6 +279,18 @@ class TwoTowerConfig: compiler_search_stagnation_patience: int = 2 compiler_search_backtrack_limit: int = 8 compiler_search_local_nogoods: bool = False + # VSS1-03 certified-solver decode: exact closure prunes the compiler forest to + # the certificate-checked live subset before soft ranking. Disabled by default; + # ``False`` is byte-identical to existing decode. Deterministic budgets are + # authoritative (wall timer is advisory 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" # none | summary | full # A4 minimum-content decode contract (compiler-tree decode only): # 0 -> off (empty layouts remain legal completions); # >0 -> require at least this many components before EOS is admitted; @@ -3493,6 +3505,58 @@ def record_choice( ) return tuple(paths[chosen].token_ids) + def _solver_prune_forest(self, forest, prefix): + """VSS1-03: prune the compiler forest to the certified live subset. + + Only reached when ``verified_solver_decode`` is on. Runs certificate-checked + exact closure (the VSS0-04 oracle) over the forest and drops only candidates + proven ``UNSUPPORTED`` with a replay-valid certificate; ``UNKNOWN`` candidates + are kept (``keep_and_rank``) so the ordinary soft ranker still sees them. An + unsupported tokenizer/pack fails with a clear capability error (never a + silent weaker path). + """ + from slm_training.dsl.language_contract import contract_id + from slm_training.dsl.solver.closure import EnumerativeSupportProvider + from slm_training.dsl.solver.decode import solver_prune + from slm_training.dsl.solver.openui_support import ( + OpenUIForestExpander, + OpenUIWellFormedVerifier, + ) + from slm_training.dsl.solver.state import SolverBounds + from slm_training.models.dsl_tokenizer import is_dsl_native_tokenizer + + if not is_dsl_native_tokenizer(self.tokenizer): + raise ValueError( + "verified_solver_decode requires a DSL-native tokenizer/pack; " + f"{type(self.tokenizer).__name__} is unsupported" + ) + if forest.coverage != "complete" or not forest.paths: + return forest # closure is authoritative only over an exhaustive set + + max_nodes = int(getattr(self.config, "solver_max_nodes", 512) or 512) + bounds = SolverBounds( + max_tokens=max(1, max_nodes * 64), + max_nodes=max_nodes, + max_depth=int(getattr(self.config, "solver_max_depth", 64) or 64), + max_backtracks=int(getattr(self.config, "solver_max_backtracks", 64) or 64), + max_verifier_calls=int( + getattr(self.config, "solver_max_verifier_calls", 64) or 64 + ), + ) + cv = contract_id() + window = int(getattr(self.config, "grammar_draft_window", 8) or 8) + expander = OpenUIForestExpander( + self.tokenizer, prefix, pack_id="openui", constraint_version=cv, + bounds=bounds, max_path_tokens=window, + ) + provider = EnumerativeSupportProvider(expander, OpenUIWellFormedVerifier()) + policy = str(getattr(self.config, "solver_unknown_policy", "keep_and_rank")) + pruned, _result = solver_prune( + forest, prefix, provider, pack_id="openui", constraint_version=cv, + bounds=bounds, unknown_policy=policy, state=expander.root_state(), cache={}, + ) + return pruned + def _compiler_ltr_decode_one( self, ctx: torch.Tensor, @@ -3582,6 +3646,11 @@ def _compiler_ltr_decode_one( ), min_content=self._effective_min_content(slot_contract), ) + if getattr(self.config, "verified_solver_decode", False): + # VSS1-03: certified exact closure prunes the forest to the live + # subset before any soft ranking. Disabled by default (guard above), + # so the default decode path is untouched. + forest = self._solver_prune_forest(forest, prefix) # Partial coverage still contains individually grammar-admitted # paths. Tree/restricted modes must consume those paths; falling # back merely because the vocabulary is not exhaustive discards diff --git a/tests/test_dsl/test_solver_decode.py b/tests/test_dsl/test_solver_decode.py new file mode 100644 index 00000000..64a6e9c9 --- /dev/null +++ b/tests/test_dsl/test_solver_decode.py @@ -0,0 +1,152 @@ +"""VSS1-03 (SLM-63): decode-time forest pruning via exact closure — core logic. + +Torch-free unit tests for `solver_prune`: it removes a candidate only when its +UNSUPPORTED certificate replays, keeps UNKNOWN candidates, returns a subset (so a +later ranker can never reintroduce a removed candidate), leaves non-`complete` +coverage untouched, and yields an empty forest on certified bottom. The full +decode wiring/parity is covered under tests/test_models/. +""" + +from __future__ import annotations + +import hashlib + +import pytest + +from slm_training.dsl.grammar.fastpath.compiler_draft import CompletionForest, CompletionPath +from slm_training.dsl.solver.decode import solver_prune +from slm_training.dsl.solver.state import SolverBounds, SupportVerdict +from slm_training.dsl.solver.support import ( + ReplayResult, + SearchCounters, + SupportCertificate, + SupportResult, +) + +_BOUNDS = SolverBounds( + max_tokens=1000, max_nodes=1000, max_depth=32, max_backtracks=1000, + max_verifier_calls=1000, +) + + +def _sha(text: str) -> str: + return hashlib.sha256(text.encode()).hexdigest() + + +class _RuleProvider: + """Verdict is a function of the candidate's token_ids; certificates replay.""" + + def __init__(self, rule): + self._rule = rule + + @property + def backend_version(self) -> str: + return "stub/decode-v1" + + def _cert(self, state, query, verdict) -> SupportCertificate: + common = dict( + schema_version=1, query=query, verdict=verdict, problem_id=state.problem_id, + pack_id=state.pack_id, constraint_version=state.constraint_version, + bounds=state.bounds, search_order="canonical-domain-value-v1", + explored_state_fingerprints=(), verifier_profile="stub", + ) + if verdict is SupportVerdict.UNSUPPORTED: + return SupportCertificate(**common, coverage_observations=("complete",), exhausted=True) + if verdict is SupportVerdict.SUPPORTED: + return SupportCertificate( + **common, coverage_observations=("complete",), witness_source="stub", + witness_digest=_sha(query.candidate.payload_json), exhausted=False, + ) + return SupportCertificate(**common, coverage_observations=("partial",), exhausted=False) + + def check(self, state, query) -> SupportResult: + verdict = self._rule(tuple(query.candidate.payload["token_ids"])) + return SupportResult(verdict, self._cert(state, query, verdict), counters=SearchCounters(nodes=1)) + + def replay(self, certificate, *, state) -> ReplayResult: + violations = [] + if state.fingerprint != certificate.query.state_fingerprint: + violations.append("stale") + recomputed = self._rule(tuple(certificate.query.candidate.payload["token_ids"])) + if recomputed != certificate.verdict: + violations.append("verdict") + if certificate.verdict is SupportVerdict.UNSUPPORTED and not certificate.exhausted: + violations.append("not exhausted") + if self._cert(state, certificate.query, recomputed).digest != certificate.digest: + violations.append("digest") + return ReplayResult(ok=not violations, verdict=certificate.verdict, violations=tuple(violations)) + + +def _forest(coverage="complete"): + return CompletionForest( + (CompletionPath((10,), "a"), CompletionPath((20,), "b"), CompletionPath((30,), "c")), + coverage, + ("NAME", "COMPONENT"), + ) + + +def _kinds(forest): + return [p.kind for p in forest.paths] + + +def test_removes_only_certified_unsupported_and_keeps_unknown(): + rule = lambda tids: SupportVerdict.UNSUPPORTED if tids == (10,) else SupportVerdict.UNKNOWN # noqa: E731 + forest = _forest() + pruned, result = solver_prune( + forest, [1, 2, 3], _RuleProvider(rule), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + ) + # Only the certified-unsupported candidate (10,) is dropped; UNKNOWNs kept. + assert _kinds(pruned) == ["b", "c"] + # Subset of the original -> a ranker cannot reintroduce the removed candidate. + assert set(p.token_ids for p in pruned.paths) < set(p.token_ids for p in forest.paths) + assert pruned.coverage == "complete" and pruned.terminals == forest.terminals + assert result is not None and result.counters.candidates_removed == 1 + + +def test_all_unsupported_yields_empty_forest_certified_bottom(): + forest = _forest() + pruned, result = solver_prune( + forest, [1], _RuleProvider(lambda tids: SupportVerdict.UNSUPPORTED), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + ) + assert pruned.paths == () # certified bottom -> decode dead-end/rollback handles it + assert result is not None and result.state.is_bottom + + +def test_all_unknown_keeps_forest_identity(): + forest = _forest() + pruned, result = solver_prune( + forest, [1], _RuleProvider(lambda tids: SupportVerdict.UNKNOWN), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + ) + assert pruned is forest # nothing removed -> identity preserved + assert result is not None + + +def test_non_complete_coverage_is_never_pruned(): + for coverage in ("partial", "none"): + forest = _forest(coverage) + pruned, result = solver_prune( + forest, [1], _RuleProvider(lambda tids: SupportVerdict.UNSUPPORTED), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + ) + # Closure is authoritative only over an exhaustive candidate set. + assert pruned is forest + assert result is None + + +def test_unsupported_policy_rejected(): + with pytest.raises(ValueError, match="solver_unknown_policy"): + solver_prune( + _forest(), [1], _RuleProvider(lambda tids: SupportVerdict.UNKNOWN), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + unknown_policy="drop_unknown", + ) + + +def test_decode_module_is_torch_free(): + import inspect + import slm_training.dsl.solver.decode as decode_mod + + assert "torch" not in inspect.getsource(decode_mod) diff --git a/tests/test_models/test_solver_decode_integration.py b/tests/test_models/test_solver_decode_integration.py new file mode 100644 index 00000000..34b45970 --- /dev/null +++ b/tests/test_models/test_solver_decode_integration.py @@ -0,0 +1,178 @@ +"""VSS1-03 (SLM-63): model-level decode integration for ``verified_solver_decode``. + +Torch-bearing integration tests for the compiler-tree decode seam: + +* the solver config fields default disabled and round-trip through + ``dataclasses.asdict`` (the config/checkpoint metadata path), with old + checkpoints missing the fields falling back to defaults; +* ``verified_solver_decode=False`` is byte-identical decode (the parity + regression on a fixed fixture/seed); +* ``_solver_prune_forest`` runs real certificate-checked closure over a real + ``CompletionForest`` and never invents a candidate the forest lacked; +* an unsupported tokenizer/pack raises a clear capability error rather than + silently taking a weaker path; +* the decode loop invokes the solver seam only when the flag is enabled. + +The core ``solver_prune`` removal/keep/certified-bottom/coverage semantics (with a +fake certifying provider) live in ``tests/test_dsl/test_solver_decode.py``; this +file only pins the Torch model wiring. +""" + +from __future__ import annotations + +import dataclasses + +import pytest +import torch + +from slm_training.dsl.grammar.fastpath.compiler_draft import ( + CompletionForest, + build_completion_forest, +) +from slm_training.dsl.schema import ExampleRecord +from slm_training.models.twotower import TwoTowerConfig, TwoTowerModel + +_SOLVER_DEFAULTS = { + "verified_solver_decode": False, + "solver_max_nodes": 512, + "solver_max_depth": 64, + "solver_max_backtracks": 64, + "solver_max_verifier_calls": 64, + "solver_max_wall_ms": 0, + "solver_unknown_policy": "keep_and_rank", + "solver_certificate_mode": "summary", +} + + +def _model(**config_overrides) -> TwoTowerModel: + record = ExampleRecord( + id="compiler", + prompt="card", + openui='root = Card([title])\ntitle = TextContent(":hero.title")\n', + placeholders=[":hero.title"], + split="train", + source="fixture", + ) + config = TwoTowerConfig( + context_backend="scratch", + output_tokenizer="lexer", + d_model=32, + n_heads=2, + context_layers=1, + denoiser_layers=1, + max_prompt_len=32, + max_target_len=32, + grammar_ltr_max_tokens=32, + gen_steps=1, + seed=0, + **config_overrides, + ) + model = TwoTowerModel.from_records([record], config=config, device="cpu") + model.eval() + return model + + +def test_solver_fields_default_disabled() -> None: + config = TwoTowerConfig(context_backend="scratch", output_tokenizer="lexer") + for field, expected in _SOLVER_DEFAULTS.items(): + assert getattr(config, field) == expected + assert config.verified_solver_decode is False + + +def test_solver_config_round_trips_and_old_checkpoints_default() -> None: + config = TwoTowerConfig( + context_backend="scratch", + output_tokenizer="lexer", + verified_solver_decode=True, + solver_max_nodes=8, + solver_max_depth=4, + solver_max_backtracks=3, + solver_max_verifier_calls=5, + solver_max_wall_ms=7, + solver_unknown_policy="keep_and_rank", + solver_certificate_mode="full", + ) + dumped = dataclasses.asdict(config) + for field in _SOLVER_DEFAULTS: + assert field in dumped, f"{field} missing from serialized config" + + fields = TwoTowerConfig.__dataclass_fields__ + restored = TwoTowerConfig(**{k: v for k, v in dumped.items() if k in fields}) + assert restored.verified_solver_decode is True + assert restored.solver_max_nodes == 8 + assert restored.solver_max_wall_ms == 7 + assert restored.solver_certificate_mode == "full" + + # An old checkpoint dict missing every solver field falls back to defaults + # (strict for existing tensors, tolerant only of new config defaults). + legacy = { + k: v + for k, v in dumped.items() + if k != "verified_solver_decode" and not k.startswith("solver_") + } + legacy_config = TwoTowerConfig(**{k: v for k, v in legacy.items() if k in fields}) + for field, expected in _SOLVER_DEFAULTS.items(): + assert getattr(legacy_config, field) == expected + + +def test_disabled_flag_is_decode_identical() -> None: + baseline = _model() + ctx, ctx_pad = baseline._encode_context(["card"]) + expected = baseline._compiler_ltr_decode_one( + ctx, ctx_pad, 24, mode="tree", slot_contract=None + ) + + off = _model(verified_solver_decode=False) + ctx2, ctx_pad2 = off._encode_context(["card"]) + ids = off._compiler_ltr_decode_one( + ctx2, ctx_pad2, 24, mode="tree", slot_contract=None + ) + assert torch.equal(ids, expected) + + +def test_solver_prune_forest_runs_real_closure_and_returns_subset() -> None: + model = _model(verified_solver_decode=True, solver_max_nodes=4) + prefix = [model.tokenizer.bos_id] + forest = build_completion_forest(model.tokenizer, prefix) + assert forest.coverage == "complete" and forest.paths + + pruned = model._solver_prune_forest(forest, prefix) + assert isinstance(pruned, CompletionForest) + assert pruned.coverage == forest.coverage + original = {(p.kind, tuple(p.token_ids)) for p in forest.paths} + survivors = {(p.kind, tuple(p.token_ids)) for p in pruned.paths} + # Closure may only remove candidates; it never invents one the forest lacked. + assert survivors <= original + + +def test_enabled_requires_dsl_native_tokenizer() -> None: + model = _model(verified_solver_decode=True) + prefix = [model.tokenizer.bos_id] + forest = build_completion_forest(model.tokenizer, prefix) + model.tokenizer = object() # not a DSLNativeTokenizer/pack + with pytest.raises(ValueError, match="DSL-native"): + model._solver_prune_forest(forest, prefix) + + +def test_decode_invokes_solver_only_when_enabled() -> None: + # A spy proves the flag gates the seam call without paying the (deliberately + # expensive) real-solver cost on every decode step. Returning the forest + # unchanged keeps decode on the baseline trajectory. + calls = {"n": 0} + + def _spy(forest, prefix): + calls["n"] += 1 + return forest + + off = _model(verified_solver_decode=False) + off._solver_prune_forest = _spy # type: ignore[assignment] + ctx, ctx_pad = off._encode_context(["card"]) + off._compiler_ltr_decode_one(ctx, ctx_pad, 8, mode="tree", slot_contract=None) + assert calls["n"] == 0 # disabled: seam never called + + calls["n"] = 0 + on = _model(verified_solver_decode=True) + on._solver_prune_forest = _spy # type: ignore[assignment] + ctx2, ctx_pad2 = on._encode_context(["card"]) + on._compiler_ltr_decode_one(ctx2, ctx_pad2, 8, mode="tree", slot_contract=None) + assert calls["n"] >= 1 # enabled: pruned at least once before soft ranking From d6f88d778d91303df683c889f839337ef2b11e5a Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 18 Jul 2026 01:33:24 +0000 Subject: [PATCH 9/9] Persist and replay solver deductions, decisions, and metrics (SLM-64) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit VSS1-04 makes every verified-solver transition replayable and measured on the existing decode trace + telemetry owners — no second trace store, no new output root, no custom format. - dsl/solver/replay.py (new, 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 — the ten VSS1-04 invariants as human-readable strings: fingerprint lineage, live-only removals + full-mode certificate tamper detection (same canonical-JSON digest as SupportCertificate.digest), unknown-never-removes, single-live decisions, backtrack lineage, nogood-not-a-deduction, solved-has-report, certified-unsat purity, counter agreement, and truncation honesty. Closure never claims "solved". - harnesses/distill/trace_store.py: decode trace schema version 2 -> 3 (backward-compatible v1/v2 readers), DecodeTraceRecorder.record_solver sidecar, and replay_violations extended to run the solver invariants on any solver events present (decode-only traces unaffected). - 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: _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; the disabled decode path is unchanged. Events and certificates store only token/path ids and SHA-256 digests — never raw region/user text. Tests: tests/test_dsl/test_solver_replay.py (validator + real-ClosureResult round-trip + tamper) and tests/test_harnesses/distill/test_solver_trace.py (recorder capture, clean replay, counters, historical compat). Docs: meta-model-traces.md, telemetry.md, verified-scope-solver.md, and a dated fixture-evidence note. Fixture-grade wiring only; no train/eval/benchmark/checkpoint ran, and this makes no solver-quality, correctness, speed, or ship claim. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt --- docs/design/meta-model-traces.md | 31 + docs/design/telemetry.md | 26 + docs/design/verified-scope-solver.md | 56 ++ .../vss1-04-solver-trace-replay-20260718.md | 65 ++ src/slm_training/dsl/solver/replay.py | 575 ++++++++++++++++++ .../harnesses/distill/trace_store.py | 44 +- src/slm_training/models/decode_stats.py | 35 ++ src/slm_training/models/twotower.py | 67 +- tests/test_dsl/test_solver_replay.py | 339 +++++++++++ .../distill/test_solver_trace.py | 120 ++++ 10 files changed, 1352 insertions(+), 6 deletions(-) create mode 100644 docs/design/vss1-04-solver-trace-replay-20260718.md create mode 100644 src/slm_training/dsl/solver/replay.py create mode 100644 tests/test_dsl/test_solver_replay.py create mode 100644 tests/test_harnesses/distill/test_solver_trace.py diff --git a/docs/design/meta-model-traces.md b/docs/design/meta-model-traces.md index 805db55d..55e00fd0 100644 --- a/docs/design/meta-model-traces.md +++ b/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 diff --git a/docs/design/telemetry.md b/docs/design/telemetry.md index 8f456aae..d13ac6ec 100644 --- a/docs/design/telemetry.md +++ b/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_.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 diff --git a/docs/design/verified-scope-solver.md b/docs/design/verified-scope-solver.md index 51e7deaa..215a33c4 100644 --- a/docs/design/verified-scope-solver.md +++ b/docs/design/verified-scope-solver.md @@ -345,6 +345,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? | @@ -612,3 +646,25 @@ makes **no correctness, speed, or ship claim**. Verified: `python -m pytest tests/test_models/test_solver_decode_integration.py tests/test_models/test_compiler_decode.py tests/test_dsl/test_solver_decode.py tests/test_dsl/test_solver_controller.py -q` and `python -m scripts.repo_policy`. + +2026-07-18 — VSS1-04 / SLM-64 makes solver transitions replayable and measured +without a second trace store (`dsl/solver/replay.py` event builders + +`solver_replay_violations`; decode trace schema `version = 3` with backward-compat +v1/v2 readers). `models/twotower._record_solver_metrics` (gated on an attached +`DecodeTraceRecorder`) emits `solver_state`/`support_result`/`certified_deduction`/ +`solver_terminal` for closure decode; a bounded `solver` sidecar carries +mode-serialized certificates + counters (`none`/`summary`/`full`); solver work +counters + `solver_ms` ride the existing `DecodeStats` → `metrics["decode_stats"]` +envelope (zero on the default path). `harnesses/distill/trace_store.replay_violations` +now also runs the ten solver invariants (fingerprint lineage, live-only removals + +`full`-mode certificate tamper detection, unknown-never-removes, single-live +decisions, backtrack lineage, nogood-not-a-deduction, solved-has-report, +certified-unsat purity, counter agreement, truncation honesty). Only ids/digests +are stored — no raw region/user text; closure never claims `solved`. Pinned by +`tests/test_dsl/test_solver_replay.py` and +`tests/test_harnesses/distill/test_solver_trace.py`. No train/eval/benchmark/ +checkpoint ran; **no solver-quality or ship claim**. Verified: `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` and +`python -m scripts.repo_policy`. diff --git a/docs/design/vss1-04-solver-trace-replay-20260718.md b/docs/design/vss1-04-solver-trace-replay-20260718.md new file mode 100644 index 00000000..fd0a2ffa --- /dev/null +++ b/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.** diff --git a/src/slm_training/dsl/solver/replay.py b/src/slm_training/dsl/solver/replay.py new file mode 100644 index 00000000..885313e2 --- /dev/null +++ b/src/slm_training/dsl/solver/replay.py @@ -0,0 +1,575 @@ +"""Replayable solver-transition trace events + validator (VSS1-04 / SLM-64). + +Torch-free. Turns the certified-solver artifacts (exact-closure / search results +and their certificates) into typed, replayable events recorded inside the +existing ``DecodeTraceRecorder.events`` stream, and validates that every +destructive transition is consistent and — in ``full`` certificate mode — +certificate-checked. + +Honesty invariants (owned here; see ``docs/design/verified-scope-solver.md``): + +* ``unknown`` support never removes a candidate; +* a ``certified_deduction`` removes only currently-live values and cites a + certificate; in ``full`` mode that certificate must be present and its + recomputed digest must equal its id (tamper detection); +* a ``nogood`` is never a certified deduction — a "deduction" with no certificate + is a nogood masquerading as proof and is a violation; +* ``certified_unsat`` is impossible once any ``unknown`` / budget / truncation + appears on the path; +* a ``solved`` terminal must carry a final verifier report; +* a truncated (bounded) snapshot is reported as **non-replayable**, never + accepted as an exhaustive proof. + +The event stream is a subset of the schema per producer: exact-closure decode +emits ``solver_state`` / ``support_result`` / ``certified_deduction`` / +``solver_terminal``; the reversible search controller additionally emits +``decision`` / ``backtrack`` / ``nogood``. The validator handles the full schema. + +This module writes no Torch, runs no model, and makes no quality/ship claim. +""" + +from __future__ import annotations + +import hashlib +import json +from typing import Any + +SOLVER_TRACE_SCHEMA_VERSION = 1 + +SOLVER_EVENT_KINDS = frozenset( + { + "solver_state", + "support_result", + "certified_deduction", + "decision", + "backtrack", + "nogood", + "solver_terminal", + } +) + +CERTIFICATE_MODES = ("none", "summary", "full") + +# Bounded live-value snapshot per ``solver_state`` (privacy + boundedness). +_MAX_DOMAIN_SNAPSHOT = 512 + +# Verifier-report keys whose string values are provenance labels (never user +# text); every other string is dropped so no raw region text can leak. +_REPORT_STR_ALLOW = frozenset({"name", "profile", "status", "verifier", "verdict"}) + + +def _canonical(obj: Any) -> str: + return json.dumps(obj, sort_keys=True, separators=(",", ":"), default=str) + + +def _digest(obj: Any) -> str: + return hashlib.sha256(_canonical(obj).encode()).hexdigest() + + +def _value_key(value_dict: dict) -> str: + return _canonical(value_dict) + + +def _hole_key(hole_dict: dict) -> str: + return _canonical(hole_dict) + + +# --------------------------------------------------------------------------- # +# Event builders +# --------------------------------------------------------------------------- # + + +def solver_state_event(state, *, max_snapshot: int = _MAX_DOMAIN_SNAPSHOT) -> dict: + """A ``solver_state`` event with a bounded live-domain snapshot. + + ``domain`` maps each hole to its live value keys so the validator can verify + deductions/decisions remove/select only live values. If the snapshot exceeds + ``max_snapshot`` it is truncated and ``trace_truncated`` is set — the validator + then refuses to treat the trace as a replayable exhaustive proof. + """ + domain: dict[str, list[str]] = {} + total = 0 + truncated = False + for hole in state.holes: + hole_key = _hole_key(hole.hole_id.to_dict()) + values: list[str] = [] + for value in hole.values: + if total >= max_snapshot: + truncated = True + break + values.append(_value_key(value.to_dict())) + total += 1 + domain[hole_key] = values + if truncated: + break + return { + "kind": "solver_state", + "state_fingerprint": state.fingerprint, + "problem_id": state.problem_id, + "pack_id": state.pack_id, + "constraint_version": state.constraint_version, + "bounds": state.bounds.to_dict(), + "decision_level": state.decision_level, + "domain_summary": state.summary(), + "domain": domain, + "trace_truncated": truncated, + } + + +def support_result_event( + *, + state_fingerprint: str, + hole_id_dict: dict, + candidate_dict: dict, + verdict: str, + certificate_id: str | None = None, + witness_digest: str | None = None, + stop_reason: str | None = None, + coverage: tuple[str, ...] = (), + counters: dict | None = None, +) -> dict: + return { + "kind": "support_result", + "state_fingerprint": state_fingerprint, + "hole_id": hole_id_dict, + "candidate": candidate_dict, + "verdict": verdict, + "certificate_id": certificate_id, + "witness_digest": witness_digest, + "stop_reason": stop_reason, + "coverage": list(coverage), + "counters": counters or {}, + } + + +def certified_deduction_event(deduction) -> dict: + return {"kind": "certified_deduction", **deduction.to_dict()} + + +def decision_event(decision) -> dict: + return {"kind": "decision", **decision.to_dict()} + + +def backtrack_event( + *, + from_fingerprint: str, + to_fingerprint: str, + from_level: int, + to_level: int, + decision_id: str, + conflict_kind: str, +) -> dict: + return { + "kind": "backtrack", + "from_fingerprint": from_fingerprint, + "to_fingerprint": to_fingerprint, + "from_level": from_level, + "to_level": to_level, + "decision_id": decision_id, + "conflict_kind": conflict_kind, + } + + +def nogood_event(nogood) -> dict: + return {"kind": "nogood", **nogood.to_dict()} + + +def _summarize_report(report: Any) -> Any: + if report is None: + return None + if isinstance(report, bool): + return report + if isinstance(report, (int, float)): + return report + if isinstance(report, str): + return report[:64] + if isinstance(report, dict): + summary: dict[str, Any] = {} + for key, value in report.items(): + if isinstance(value, bool) or isinstance(value, (int, float)): + summary[key] = value + elif isinstance(value, str) and key in _REPORT_STR_ALLOW: + summary[key] = value[:64] + return summary + return None + + +def solver_terminal_event( + *, + status: str, + source_digest: str | None = None, + verifier_report: Any = None, + certificate_mode: str = "full", + trace_truncated: bool = False, +) -> dict: + return { + "kind": "solver_terminal", + "status": str(status), + "source_digest": source_digest, + "verifier_report": _summarize_report(verifier_report), + "certificate_mode": certificate_mode, + "trace_truncated": bool(trace_truncated), + } + + +# --------------------------------------------------------------------------- # +# Certificate serialization by mode +# --------------------------------------------------------------------------- # + + +def serialize_certificates(certificate_store: dict, mode: str) -> dict: + """Bounded, mode-gated certificate artifacts keyed by certificate id. + + ``none`` → ``{}`` (aggregate counters/status only); ``summary`` → compact, + non-replayable descriptors; ``full`` → the replay material (each cert's + ``to_dict()``, whose recomputed digest must equal its id). + """ + if mode not in CERTIFICATE_MODES: + raise ValueError(f"unsupported solver_certificate_mode: {mode!r}") + if mode == "none": + return {} + out: dict[str, dict] = {} + for cid, cert in certificate_store.items(): + payload = cert.to_dict() + if mode == "full": + out[cid] = payload + else: # summary + out[cid] = { + "schema_version": payload.get("schema_version"), + "verdict": payload.get("verdict"), + "exhausted": payload.get("exhausted"), + "coverage_observations": payload.get("coverage_observations"), + "witness_digest": payload.get("witness_digest"), + } + return out + + +# --------------------------------------------------------------------------- # +# Producers: solver result -> ordered event stream +# --------------------------------------------------------------------------- # + + +def solver_events_from_closure( + result, + root_state, + *, + certificate_mode: str = "full", +) -> list[dict]: + """Event stream for one exact-closure decode prune. + + Ordered: root ``solver_state``, ``support_result`` (supported witnesses then + unknown queries), ``certified_deduction`` (closure application order — passes + chain by fingerprint), and a ``solver_terminal``. + """ + events: list[dict] = [solver_state_event(root_state)] + for witness in result.witnesses: + events.append( + support_result_event( + state_fingerprint=root_state.fingerprint, + hole_id_dict=witness.hole_id.to_dict(), + candidate_dict=witness.value.to_dict(), + verdict="supported", + certificate_id=witness.certificate_id, + witness_digest=witness.witness_digest, + coverage=("complete",), + ) + ) + for query in result.unknown_queries: + events.append( + support_result_event( + state_fingerprint=query.state_fingerprint, + hole_id_dict=query.hole_id.to_dict(), + candidate_dict=query.candidate.to_dict(), + verdict="unknown", + stop_reason=result.stop_reason, + ) + ) + for deduction in result.deductions: + events.append(certified_deduction_event(deduction)) + truncated = any(e.get("trace_truncated") for e in events) + events.append( + solver_terminal_event( + status=closure_status(result), + certificate_mode=certificate_mode, + trace_truncated=truncated, + ) + ) + return events + + +def closure_status(result) -> str: + """Honest terminal status for a closure *prune*. + + Closure never claims ``solved``: it prunes to a live subset but does not + itself materialize a verifier-accepted terminal (that is the controller's job, + and the decode's own final validate). It reports ``certified_unsat`` only on a + certified bottom, ``budget_exhausted`` on a budget stop, else ``unknown``. + """ + if result.state.is_bottom: + return "certified_unsat" + if result.stop_reason and result.stop_reason.startswith("budget"): + return "budget_exhausted" + return "unknown" + + +def solver_events_from_search( + result, + root_state, + *, + certificate_mode: str = "full", + verifier_report: Any = None, +) -> list[dict]: + """Event stream for a reversible search-controller run (decisions/nogoods).""" + events: list[dict] = [solver_state_event(root_state)] + for deduction in result.deductions: + events.append(certified_deduction_event(deduction)) + for decision in result.decisions: + events.append(decision_event(decision)) + for nogood in result.nogoods: + events.append(nogood_event(nogood)) + events.append( + solver_terminal_event( + status=getattr(result.status, "value", str(result.status)), + verifier_report=verifier_report + if verifier_report is not None + else result.verifier_report, + certificate_mode=certificate_mode, + ) + ) + return events + + +# --------------------------------------------------------------------------- # +# Aggregate counters +# --------------------------------------------------------------------------- # + + +def solver_trace_counters(events: list[dict]) -> dict[str, int]: + """Per-kind aggregate counts derived from an event stream (for invariant 9).""" + counts = { + "solver_states": 0, + "support_supported": 0, + "support_unsupported": 0, + "support_unknown": 0, + "certified_deductions": 0, + "certified_removed": 0, + "decisions": 0, + "backtracks": 0, + "nogoods": 0, + } + for event in events: + kind = event.get("kind") + if kind == "solver_state": + counts["solver_states"] += 1 + elif kind == "support_result": + verdict = event.get("verdict") + if verdict == "supported": + counts["support_supported"] += 1 + elif verdict == "unsupported": + counts["support_unsupported"] += 1 + elif verdict == "unknown": + counts["support_unknown"] += 1 + elif kind == "certified_deduction": + counts["certified_deductions"] += 1 + counts["certified_removed"] += len(event.get("removed", [])) + elif kind == "decision": + counts["decisions"] += 1 + elif kind == "backtrack": + counts["backtracks"] += 1 + elif kind == "nogood": + counts["nogoods"] += 1 + return counts + + +# --------------------------------------------------------------------------- # +# Replay validator +# --------------------------------------------------------------------------- # + + +def solver_replay_violations( + events: list[dict], + *, + certificates: dict | None = None, + certificate_mode: str = "full", + counters: dict | None = None, +) -> list[str]: + """Validate one solver event stream; empty list ⇒ replayable. + + Returns human-readable violation strings (never raises). Checks the ten + VSS1-04 invariants: fingerprint lineage, live-only removals + certificate + replay (full mode), unknown-never-removes, single-live decisions, backtrack + lineage, nogood-not-a-deduction, solved-has-report, certified-unsat purity, + counter agreement, and truncation honesty. + """ + certificates = certificates or {} + violations: list[str] = [] + + active_fp: str | None = None + live: dict[str, set[str]] = {} + # backtrack targets: fingerprint -> (level, live snapshot) + recorded: dict[str, tuple[int, dict[str, set[str]]]] = {} + pending_before: str | None = None + pending_after: str | None = None + saw_unknown = False + saw_budget = False + saw_truncation = False + + def commit_pending() -> None: + nonlocal active_fp, pending_before, pending_after + if pending_before is not None and pending_after is not None: + active_fp = pending_after + pending_before = None + pending_after = None + + for index, event in enumerate(events): + kind = event.get("kind") + if kind not in SOLVER_EVENT_KINDS: + violations.append(f"event {index}: unknown solver event kind {kind!r}") + continue + if event.get("trace_truncated"): + saw_truncation = True + + if kind == "solver_state": + commit_pending() + active_fp = event.get("state_fingerprint") + live = { + hole_key: set(values) + for hole_key, values in (event.get("domain") or {}).items() + } + recorded[active_fp] = ( + int(event.get("decision_level", 0)), + {h: set(v) for h, v in live.items()}, + ) + + elif kind == "support_result": + verdict = event.get("verdict") + if verdict == "unknown": + saw_unknown = True + if event.get("stop_reason", "") and str( + event.get("stop_reason") + ).startswith("budget"): + saw_budget = True + + elif kind == "certified_deduction": + before = event.get("before_fingerprint") + after = event.get("after_fingerprint") + # Passes share a before/after; a new before commits the prior pass. + if before != pending_before: + commit_pending() + if active_fp is not None and before != active_fp: + violations.append( + f"event {index}: deduction before_fingerprint " + f"{before!r} != active state {active_fp!r}" + ) + pending_before = before + pending_after = after + hole_key = _hole_key(event.get("hole_id", {})) + removed = [_value_key(v) for v in event.get("removed", [])] + cert_ids = event.get("certificate_ids", []) + if not cert_ids: + violations.append( + f"event {index}: certified_deduction cites no certificate " + "(a nogood must not be relabeled a certified deduction)" + ) + live_here = live.get(hole_key, set()) + for value_key in removed: + if value_key not in live_here: + violations.append( + f"event {index}: deduction removes non-live value at hole" + ) + else: + live_here.discard(value_key) + live[hole_key] = live_here + if certificate_mode == "full": + for cid in cert_ids: + if cid not in certificates: + violations.append( + f"event {index}: certificate {cid[:12]}… missing in full mode" + ) + elif _digest(certificates[cid]) != cid: + violations.append( + f"event {index}: certificate {cid[:12]}… digest mismatch (tampered)" + ) + + elif kind == "decision": + commit_pending() + before = event.get("before_fingerprint") + if active_fp is not None and before != active_fp: + violations.append( + f"event {index}: decision before_fingerprint " + f"{before!r} != active state {active_fp!r}" + ) + hole_key = _hole_key(event.get("hole_id", {})) + chosen = _value_key(event.get("chosen", {})) + live_here = live.get(hole_key, set()) + if chosen not in live_here: + violations.append( + f"event {index}: decision selects a non-live value" + ) + alternatives = {_value_key(v) for v in event.get("alternatives", [])} + expected_alts = live_here - {chosen} + if alternatives != expected_alts: + violations.append( + f"event {index}: decision alternatives do not match remaining live values" + ) + after = event.get("after_fingerprint") + recorded[before] = ( + int(event.get("level", 0)), + {h: set(v) for h, v in live.items()}, + ) + live = {h: set(v) for h, v in live.items()} + live[hole_key] = {chosen} + active_fp = after + + elif kind == "backtrack": + commit_pending() + to_fp = event.get("to_fingerprint") + to_level = int(event.get("to_level", 0)) + if to_fp not in recorded: + violations.append( + f"event {index}: backtrack to unrecorded state {to_fp!r}" + ) + else: + level, snapshot = recorded[to_fp] + if level != to_level: + violations.append( + f"event {index}: backtrack to_level {to_level} != recorded level {level}" + ) + active_fp = to_fp + live = {h: set(v) for h, v in snapshot.items()} + + elif kind == "nogood": + if not event.get("provenance"): + violations.append( + f"event {index}: nogood missing provenance" + ) + + elif kind == "solver_terminal": + commit_pending() + status = event.get("status") + if status == "solved" and event.get("verifier_report") is None: + violations.append( + f"event {index}: solved terminal without a verifier report" + ) + if status == "certified_unsat" and ( + saw_unknown or saw_budget or saw_truncation + ): + violations.append( + f"event {index}: certified_unsat with unknown/budget/truncation on the path" + ) + + if saw_truncation: + violations.append( + "solver trace is truncated: bounded evidence is not a replayable " + "exhaustive proof" + ) + + if counters is not None: + derived = solver_trace_counters(events) + for key, value in derived.items(): + if key in counters and int(counters[key]) != int(value): + violations.append( + f"counter {key} mismatch: trace {counters[key]} != events {value}" + ) + + return violations diff --git a/src/slm_training/harnesses/distill/trace_store.py b/src/slm_training/harnesses/distill/trace_store.py index eed05f13..829b200a 100644 --- a/src/slm_training/harnesses/distill/trace_store.py +++ b/src/slm_training/harnesses/distill/trace_store.py @@ -21,7 +21,7 @@ from pathlib import Path from typing import Any, Iterator -TRACE_VERSION = 2 +TRACE_VERSION = 3 # Config keys that change decode behavior (used for the decode-config hash). _DECODE_KEYS = ( @@ -109,6 +109,9 @@ def __init__( self.repair_commit_count = 0 self.remask_count = 0 self._depth = 0 + # VSS1-04: mode-serialized solver certificates + aggregate counters the + # replay validator needs (None until record_solver is called). + self.solver: dict[str, Any] | None = None # ── model-side hooks ───────────────────────────────────────────────── @@ -155,6 +158,16 @@ def step( def event(self, kind: str, **payload: Any) -> None: self.events.append({"kind": kind, "depth": self._depth, **payload}) + def record_solver(self, solver_block: dict[str, Any]) -> None: + """Attach the VSS1-04 solver certificate/counter block for replay. + + The typed solver transition events themselves are appended via + ``event("solver_state"|...)``; this stores the mode-serialized (bounded) + certificates and aggregate counters the replay validator cross-checks. + Overwrites any prior block (one solver run per decode trace). + """ + self.solver = dict(solver_block) + def end(self, *, canvas: list[int] | None = None, text: str | None = None) -> None: self._depth = max(0, self._depth - 1) if self._depth > 0: @@ -178,7 +191,7 @@ def finalize( final = dict(self.final or {}) if final_text is not None: final["text"] = final_text - return { + trace = { "version": TRACE_VERSION, "meta": {**self.meta, **meta}, "steps": self.steps, @@ -195,6 +208,11 @@ def finalize( "labels": labels or {}, "recorded_at": datetime.now(timezone.utc).isoformat(), } + if self.solver is not None: + # VSS1-04 solver certificate/counter sidecar; absent on non-solver + # traces so historical v1/v2 readers are unaffected. + trace["solver"] = self.solver + return trace class TraceStore: @@ -383,6 +401,28 @@ def replay_violations(trace: dict[str, Any]) -> list[str]: final = (trace.get("final") or {}).get("canvas") if steps and final is None: violations.append("trace has steps but no final canvas") + + # VSS1-04: validate any solver-transition events via the solver replay + # checker. Decode-only traces carry no such events, so this is a no-op there + # and historical v1/v2 traces are unaffected. + from slm_training.dsl.solver.replay import ( + SOLVER_EVENT_KINDS, + solver_replay_violations, + ) + + solver_events = [ + e for e in trace.get("events", []) if e.get("kind") in SOLVER_EVENT_KINDS + ] + if solver_events: + solver = trace.get("solver") or {} + violations.extend( + solver_replay_violations( + solver_events, + certificates=solver.get("certificates"), + certificate_mode=solver.get("certificate_mode", "summary"), + counters=solver.get("counters"), + ) + ) return violations diff --git a/src/slm_training/models/decode_stats.py b/src/slm_training/models/decode_stats.py index a9f13207..19f563f3 100644 --- a/src/slm_training/models/decode_stats.py +++ b/src/slm_training/models/decode_stats.py @@ -93,6 +93,26 @@ class DecodeStats: constraint_graph_edges: int = 0 completion_bound_known: int = 0 completion_bound_unknown: int = 0 + # VSS1-04 (SLM-64): verified-solver decode work metrics. Zero on every + # historical/default path (solver disabled); solver wall time is separated + # from denoiser_ms/projection_ms. Names are stable and documented in + # docs/design/telemetry.md. + solver_ms: float = 0.0 + solver_enabled: int = 0 + solver_closure_passes: int = 0 + solver_support_queries: int = 0 + solver_support_cache_hits: int = 0 + solver_supported: int = 0 + solver_unsupported: int = 0 + solver_unknown: int = 0 + solver_certified_removed: int = 0 + solver_decisions: int = 0 + solver_backtracks: int = 0 + solver_nogoods: int = 0 + solver_expanded_nodes: int = 0 + solver_verifier_calls: int = 0 + solver_certificate_replay_failures: int = 0 + solver_terminal_status: str = "" constrained_dead_ends: int = 0 constrained_dead_end_last_position: int = -1 constrained_dead_end_forced_rank: int = -1 @@ -247,6 +267,21 @@ def aggregate_stats(rows: list[DecodeStats]) -> dict[str, Any]: "constraint_graph_edges", "completion_bound_known", "completion_bound_unknown", + "solver_ms", + "solver_enabled", + "solver_closure_passes", + "solver_support_queries", + "solver_support_cache_hits", + "solver_supported", + "solver_unsupported", + "solver_unknown", + "solver_certified_removed", + "solver_decisions", + "solver_backtracks", + "solver_nogoods", + "solver_expanded_nodes", + "solver_verifier_calls", + "solver_certificate_replay_failures", ] out: dict[str, Any] = {"n": len(rows)} for key in keys: diff --git a/src/slm_training/models/twotower.py b/src/slm_training/models/twotower.py index e50f2521..6be88001 100644 --- a/src/slm_training/models/twotower.py +++ b/src/slm_training/models/twotower.py @@ -3523,6 +3523,7 @@ def _solver_prune_forest(self, forest, prefix): OpenUIWellFormedVerifier, ) from slm_training.dsl.solver.state import SolverBounds + from slm_training.models.decode_stats import get_active_stats, timed_ms from slm_training.models.dsl_tokenizer import is_dsl_native_tokenizer if not is_dsl_native_tokenizer(self.tokenizer): @@ -3551,12 +3552,70 @@ def _solver_prune_forest(self, forest, prefix): ) provider = EnumerativeSupportProvider(expander, OpenUIWellFormedVerifier()) policy = str(getattr(self.config, "solver_unknown_policy", "keep_and_rank")) - pruned, _result = solver_prune( - forest, prefix, provider, pack_id="openui", constraint_version=cv, - bounds=bounds, unknown_policy=policy, state=expander.root_state(), cache={}, - ) + root_state = expander.root_state() + certificate_store: dict = {} + stats = get_active_stats() + # Solver wall time is separated from denoiser_ms/projection_ms (VSS1-04). + with timed_ms(stats, "solver_ms"): + pruned, result = solver_prune( + forest, prefix, provider, pack_id="openui", constraint_version=cv, + bounds=bounds, unknown_policy=policy, state=root_state, cache={}, + certificate_store=certificate_store, + ) + if result is not None: + self._record_solver_metrics( + result, root_state, certificate_store, stats + ) return pruned + def _record_solver_metrics(self, result, root_state, certificate_store, stats): + """VSS1-04: fold solver work into decode stats and, when a trace recorder + is attached, emit replayable solver-transition events + a bounded + certificate/counter sidecar. Counters ride the existing DecodeStats + envelope; nothing is emitted when neither stats nor a recorder is active. + """ + from slm_training.dsl.solver.replay import ( + SOLVER_TRACE_SCHEMA_VERSION, + closure_status, + serialize_certificates, + solver_events_from_closure, + solver_trace_counters, + ) + + if stats is not None: + counters = result.counters + stats.solver_enabled = 1 + stats.solver_closure_passes += counters.passes + stats.solver_support_queries += counters.support_queries + stats.solver_support_cache_hits += counters.cache_hits + stats.solver_supported += counters.supported + stats.solver_unsupported += counters.unsupported + stats.solver_unknown += counters.unknown + stats.solver_certified_removed += counters.candidates_removed + stats.solver_expanded_nodes += counters.expanded_nodes + stats.solver_verifier_calls += counters.verifier_calls + stats.solver_terminal_status = closure_status(result) + + recorder = getattr(self, "trace_recorder", None) + if recorder is None: + return + mode = str(getattr(self.config, "solver_certificate_mode", "summary")) + events = solver_events_from_closure( + result, root_state, certificate_mode=mode + ) + for event in events: + kind = event["kind"] + payload = {key: value for key, value in event.items() if key != "kind"} + recorder.event(kind, **payload) + recorder.record_solver( + { + "schema_version": SOLVER_TRACE_SCHEMA_VERSION, + "certificate_mode": mode, + "certificates": serialize_certificates(certificate_store, mode), + "counters": solver_trace_counters(events), + } + ) + def _compiler_ltr_decode_one( self, ctx: torch.Tensor, diff --git a/tests/test_dsl/test_solver_replay.py b/tests/test_dsl/test_solver_replay.py new file mode 100644 index 00000000..89352ad1 --- /dev/null +++ b/tests/test_dsl/test_solver_replay.py @@ -0,0 +1,339 @@ +"""VSS1-04 (SLM-64): solver-transition replay events + validator — core logic. + +Torch-free tests for `dsl/solver/replay.py`: a clean full-mode stream replays +with zero violations, and every honesty invariant (fingerprint lineage, +live-only removals, certificate tamper detection, unknown-never-removes, +single-live decisions, backtrack lineage, nogood-not-a-deduction, +solved-has-report, certified-unsat purity, counter agreement, truncation +honesty) is independently detected. Model wiring/parity is covered under +tests/test_models/ and tests/test_harnesses/. +""" + +from __future__ import annotations + +import copy + +import pytest + +from slm_training.dsl.solver.replay import ( + CERTIFICATE_MODES, + SOLVER_EVENT_KINDS, + _digest, + serialize_certificates, + solver_replay_violations, + solver_trace_counters, +) + +_ROOT = "fp_root" +_S1 = "fp_s1" + + +def _cert_payload(tag: str) -> dict: + # An opaque certificate dict whose id is its own sha256 digest (as in the + # real store: certificate_store[cert.digest] = cert). + return { + "schema_version": 1, + "verdict": "unsupported", + "exhausted": True, + "coverage_observations": ["complete"], + "tag": tag, + } + + +def _hole(name: str = "h0") -> dict: + return {"namespace": "ns", "path": [name], "kind": "component"} + + +def _val(token: int) -> dict: + return {"tag": "path", "value": f'{{"token_ids":[{token}]}}'} + + +def _clean_full_trace(): + """A valid full-mode stream: root state, one certified removal, solved.""" + cert = _cert_payload("c1") + cid = _digest(cert) + events = [ + { + "kind": "solver_state", + "state_fingerprint": _ROOT, + "problem_id": "p", + "pack_id": "openui", + "constraint_version": "cv", + "bounds": {}, + "decision_level": 0, + "domain_summary": {"hole_count": 1}, + # value keys are canonical-JSON of the value dict (validator convention) + "domain": {_hole_str(): [_valkey(10), _valkey(20), _valkey(30)]}, + "trace_truncated": False, + }, + { + "kind": "certified_deduction", + "before_fingerprint": _ROOT, + "after_fingerprint": _S1, + "hole_id": _hole(), + "removed": [_val(10)], + "certificate_ids": [cid], + "reason": "certified_unsupported", + }, + { + "kind": "solver_terminal", + "status": "solved", + "source_digest": "src", + "verifier_report": {"name": "OpenUIWellFormed", "accepted": True}, + "certificate_mode": "full", + "trace_truncated": False, + }, + ] + certificates = {cid: cert} + return events, certificates + + +def _hole_str() -> str: + from slm_training.dsl.solver.replay import _hole_key + + return _hole_key(_hole()) + + +def _valkey(token: int) -> str: + from slm_training.dsl.solver.replay import _value_key + + return _value_key(_val(token)) + + +def test_clean_full_trace_replays_without_violations(): + events, certs = _clean_full_trace() + assert solver_replay_violations(events, certificates=certs, certificate_mode="full") == [] + + +def test_deduction_removing_non_live_value_is_detected(): + # "unknown-preservation": a value kept (never in the live snapshot) cannot be + # certified-removed. + events, certs = _clean_full_trace() + events[1]["removed"] = [_val(99)] # 99 was never live + violations = solver_replay_violations(events, certificates=certs, certificate_mode="full") + assert any("non-live" in v for v in violations) + + +def test_missing_certificate_is_detected(): + events, _certs = _clean_full_trace() + violations = solver_replay_violations(events, certificates={}, certificate_mode="full") + assert any("missing" in v for v in violations) + + +def test_tampered_certificate_is_detected(): + events, certs = _clean_full_trace() + cid = next(iter(certs)) + certs[cid] = {**certs[cid], "tag": "TAMPERED"} # digest no longer matches id + violations = solver_replay_violations(events, certificates=certs, certificate_mode="full") + assert any("digest mismatch" in v or "tampered" in v.lower() for v in violations) + + +def test_nogood_relabeled_as_deduction_is_detected(): + events, certs = _clean_full_trace() + events[1]["certificate_ids"] = [] # a deduction with no certificate is a nogood + violations = solver_replay_violations(events, certificates=certs, certificate_mode="full") + assert any("nogood" in v.lower() for v in violations) + + +def test_solved_without_verifier_report_is_detected(): + events, certs = _clean_full_trace() + events[-1]["verifier_report"] = None + violations = solver_replay_violations(events, certificates=certs, certificate_mode="full") + assert any("without a verifier report" in v for v in violations) + + +def test_certified_unsat_with_unknown_is_detected(): + events, certs = _clean_full_trace() + events.insert(1, { + "kind": "support_result", + "state_fingerprint": _ROOT, + "hole_id": _hole(), + "candidate": _val(20), + "verdict": "unknown", + "certificate_id": None, + "witness_digest": None, + "stop_reason": None, + "coverage": [], + "counters": {}, + }) + events[-1]["status"] = "certified_unsat" + violations = solver_replay_violations(events, certificates=certs, certificate_mode="full") + assert any("certified_unsat" in v for v in violations) + + +def test_bad_before_fingerprint_lineage_is_detected(): + events, certs = _clean_full_trace() + events[1]["before_fingerprint"] = "fp_wrong" + violations = solver_replay_violations(events, certificates=certs, certificate_mode="full") + assert any("!= active state" in v for v in violations) + + +def test_backtrack_to_unrecorded_state_is_detected(): + events, certs = _clean_full_trace() + events.insert(2, { + "kind": "backtrack", + "from_fingerprint": _S1, + "to_fingerprint": "fp_never_recorded", + "from_level": 1, + "to_level": 0, + "decision_id": "d0", + "conflict_kind": "certified_bottom", + }) + violations = solver_replay_violations(events, certificates=certs, certificate_mode="full") + assert any("unrecorded state" in v for v in violations) + + +def test_truncated_trace_is_non_replayable(): + events, certs = _clean_full_trace() + events[0]["trace_truncated"] = True + violations = solver_replay_violations(events, certificates=certs, certificate_mode="full") + assert any("truncated" in v for v in violations) + + +def test_counter_mismatch_is_detected(): + events, certs = _clean_full_trace() + counters = solver_trace_counters(events) + counters["certified_deductions"] += 5 # lie about the count + violations = solver_replay_violations( + events, certificates=certs, certificate_mode="full", counters=counters + ) + assert any("counter" in v for v in violations) + + +def test_matching_counters_pass(): + events, certs = _clean_full_trace() + counters = solver_trace_counters(events) + assert solver_replay_violations( + events, certificates=certs, certificate_mode="full", counters=counters + ) == [] + + +def test_summary_and_none_modes_are_honest_about_limits(): + events, certs = _clean_full_trace() + cid = next(iter(certs)) + + class _Cert: + def __init__(self, payload): + self._p = payload + + def to_dict(self): + return self._p + + store = {cid: _Cert(certs[cid])} + full = serialize_certificates(store, "full") + summary = serialize_certificates(store, "summary") + none = serialize_certificates(store, "none") + assert none == {} + # summary drops the replay material (no 'tag'); full keeps it. + assert "tag" in full[cid] and "tag" not in summary[cid] + # In summary mode a tampered cert is NOT caught (summary is not a replay + # guarantee) — honest limitation, not a false pass in full mode. + tampered = copy.deepcopy(events) + tampered_certs = {cid: {**certs[cid], "tag": "X"}} + assert solver_replay_violations( + tampered, certificates=tampered_certs, certificate_mode="summary" + ) == [] + assert solver_replay_violations( + tampered, certificates=tampered_certs, certificate_mode="full" + ) != [] + + +def test_no_raw_text_leaks_into_terminal_report(): + from slm_training.dsl.solver.replay import solver_terminal_event + + event = solver_terminal_event( + status="solved", + verifier_report={ + "name": "OpenUIWellFormed", + "accepted": True, + "secret_note": "user typed their password here", + }, + ) + report = event["verifier_report"] + assert report["name"] == "OpenUIWellFormed" + assert report["accepted"] is True + assert "secret_note" not in report # non-allowlisted string dropped + + +def test_bad_mode_rejected(): + with pytest.raises(ValueError, match="solver_certificate_mode"): + serialize_certificates({}, "drop") + assert set(CERTIFICATE_MODES) == {"none", "summary", "full"} + assert "solver_state" in SOLVER_EVENT_KINDS + + +def test_closure_events_round_trip_replays_and_detects_tamper(): + """A real ClosureResult (with a real SupportCertificate) round-trips through + the producer + serializer and replays clean in full mode; tampering the + stored certificate breaks the digest check.""" + from slm_training.dsl.solver.closure import ( + CertifiedDeduction, + ClosureCounters, + ClosureResult, + ) + from slm_training.dsl.solver.replay import ( + serialize_certificates, + solver_events_from_closure, + ) + from slm_training.dsl.solver.state import ( + DomainValue, + FiniteDomainState, + HoleDomain, + HoleId, + SolverBounds, + SupportVerdict, + ) + from slm_training.dsl.solver.support import ( + SEARCH_ORDER, + SupportCertificate, + SupportQuery, + ) + + bounds = SolverBounds( + max_tokens=100, max_nodes=100, max_depth=8, max_backtracks=8, + max_verifier_calls=100, + ) + hole = HoleId(namespace="ns", path=("h0",), kind="component") + v_keep = DomainValue(tag="path", payload_json='{"token_ids":[20]}') + v_drop = DomainValue(tag="path", payload_json='{"token_ids":[10]}') + root = FiniteDomainState( + problem_id="p", pack_id="openui", constraint_version="cv", bounds=bounds, + holes=(HoleDomain(hole_id=hole, values=(v_drop, v_keep), metadata={}),), + ) + refined = root.refine(hole, (v_keep,)) + cert = SupportCertificate( + schema_version=1, + query=SupportQuery( + state_fingerprint=root.fingerprint, hole_id=hole, candidate=v_drop + ), + verdict=SupportVerdict.UNSUPPORTED, + problem_id="p", pack_id="openui", constraint_version="cv", bounds=bounds, + search_order=SEARCH_ORDER, explored_state_fingerprints=(), + coverage_observations=("complete",), verifier_profile="stub", exhausted=True, + ) + cid = cert.digest + deduction = CertifiedDeduction( + before_fingerprint=root.fingerprint, after_fingerprint=refined.fingerprint, + hole_id=hole, removed=(v_drop,), certificate_ids=(cid,), + reason="certified_unsupported", + ) + result = ClosureResult( + state=refined, deductions=(deduction,), unknown_queries=(), witnesses=(), + counters=ClosureCounters( + passes=1, support_queries=2, unsupported=1, candidates_removed=1 + ), + reached_fixed_point=True, + ) + events = solver_events_from_closure(result, root, certificate_mode="full") + certs = serialize_certificates({cid: cert}, "full") + assert solver_replay_violations( + events, certificates=certs, certificate_mode="full" + ) == [] + # The producer never claims a bare closure prune is "solved". + terminal = next(e for e in events if e["kind"] == "solver_terminal") + assert terminal["status"] == "unknown" + # Tamper the stored certificate -> digest no longer matches its id. + certs[cid] = {**certs[cid], "verifier_profile": "TAMPERED"} + assert solver_replay_violations( + events, certificates=certs, certificate_mode="full" + ) != [] diff --git a/tests/test_harnesses/distill/test_solver_trace.py b/tests/test_harnesses/distill/test_solver_trace.py new file mode 100644 index 00000000..e6aca6bd --- /dev/null +++ b/tests/test_harnesses/distill/test_solver_trace.py @@ -0,0 +1,120 @@ +"""VSS1-04 (SLM-64): model-level solver trace + replay + decode-stats wiring. + +Attaches a `DecodeTraceRecorder` to a solver-enabled TwoTower and drives one +`_solver_prune_forest` decision (fast — no full decode loop). Asserts the +recorder captures replayable solver-transition events + a bounded certificate +sidecar (`replay_violations` clean), the solver work-metric counters land in the +`DecodeStats` envelope (zero on the default path), and historical decode-only +traces still replay. Core validator semantics live in +tests/test_dsl/test_solver_replay.py. +""" + +from __future__ import annotations + +from slm_training.dsl.grammar.fastpath.compiler_draft import build_completion_forest +from slm_training.dsl.schema import ExampleRecord +from slm_training.harnesses.distill.trace_store import ( + DecodeTraceRecorder, + replay_violations, +) +from slm_training.models.decode_stats import DecodeStats, aggregate_stats, collect_decode_stats +from slm_training.models.twotower import TwoTowerConfig, TwoTowerModel + + +def _solver_model(): + record = ExampleRecord( + id="compiler", + prompt="card", + openui='root = Card([title])\ntitle = TextContent(":hero.title")\n', + placeholders=[":hero.title"], + split="train", + source="fixture", + ) + config = TwoTowerConfig( + context_backend="scratch", + output_tokenizer="lexer", + d_model=32, + n_heads=2, + context_layers=1, + denoiser_layers=1, + max_prompt_len=32, + max_target_len=32, + grammar_ltr_max_tokens=32, + gen_steps=1, + seed=0, + verified_solver_decode=True, + solver_max_nodes=4, + solver_certificate_mode="full", + ) + model = TwoTowerModel.from_records([record], config=config, device="cpu") + model.eval() + return model + + +def test_recorder_captures_replayable_solver_events(): + model = _solver_model() + prefix = [model.tokenizer.bos_id] + forest = build_completion_forest(model.tokenizer, prefix) + recorder = DecodeTraceRecorder() + model.trace_recorder = recorder + + model._solver_prune_forest(forest, prefix) + + from slm_training.dsl.solver.replay import SOLVER_EVENT_KINDS + + solver_events = [e for e in recorder.events if e.get("kind") in SOLVER_EVENT_KINDS] + assert solver_events, "expected solver-transition events on the recorder" + assert any(e["kind"] == "solver_state" for e in solver_events) + assert any(e["kind"] == "solver_terminal" for e in solver_events) + assert recorder.solver is not None + assert recorder.solver["certificate_mode"] == "full" + + trace = recorder.finalize() + assert trace["version"] == 3 + assert "solver" in trace + # The captured solver stream replays with zero violations. + assert replay_violations(trace) == [] + + +def test_solver_counters_land_in_decode_stats_envelope(): + model = _solver_model() + prefix = [model.tokenizer.bos_id] + forest = build_completion_forest(model.tokenizer, prefix) + + with collect_decode_stats() as stats: + model._solver_prune_forest(forest, prefix) + + assert stats.solver_enabled == 1 + assert stats.solver_terminal_status in {"unknown", "certified_unsat", "budget_exhausted"} + # Solver time is tracked separately from denoiser/projection. + assert stats.solver_ms >= 0.0 + # Counters surface (only) under metrics["decode_stats"] via aggregate_stats. + agg = aggregate_stats([stats]) + assert "solver_enabled_sum" in agg + assert "solver_support_queries_sum" in agg + + +def test_solver_counters_default_zero_when_disabled(): + stats = DecodeStats() + assert stats.solver_enabled == 0 + assert stats.solver_ms == 0.0 + assert stats.solver_certified_removed == 0 + assert stats.solver_terminal_status == "" + agg = aggregate_stats([stats]) + assert agg["solver_enabled_sum"] == 0.0 + assert agg["solver_certified_removed_mean"] == 0.0 + + +def test_historical_decode_only_trace_still_replays(): + # A v2-style decode trace with no solver events / no solver block is + # unaffected by the VSS1-04 replay extension. + trace = { + "version": 2, + "meta": {}, + "steps": [ + {"step": 0, "canvas": [5, 0], "commits": [{"t": 0, "id": 5}], "remasks": []} + ], + "events": [], + "final": {"canvas": [5, 2], "text": "x"}, + } + assert replay_violations(trace) == []