From 8de7bc8d09e84e8e26f3548802ecf819d0e9876a Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 20:50:03 +0000 Subject: [PATCH 1/6] 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/6] 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/6] 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/6] 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/6] 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/6] 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, )