Integrate exact closure into compiler decode behind a flag (SLM-63)#340
Merged
Conversation
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MeD6nTTabPQhva7pXtTMNj
…SLM-60) 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
VSS1-02: implement the deterministic search controller that alternates exact closure (irreversible, certificate-backed deletion) with reversible branching (rankers order only, never membership). Torch-free, not wired into decode, no ship claim. The generic controller is the new owner; LatticeSearchState is retained unchanged as the compiler-forest adapter (documented compatibility seam). - dsl/solver/controller.py: search(state, provider, terminal_checker, *, ranker, hole_selector, ...) plus SearchStatus (SOLVED / CERTIFIED_UNSAT / UNKNOWN / BUDGET_EXHAUSTED), CandidateRanker + BaselineRanker, TerminalChecker/Outcome, SearchDecision, Nogood, SearchResult. Smallest-domain-first hole selection; ranker permutation validated (missing/extra/duplicate rejected); local nogoods are request-local and never serialized as certified deductions; CERTIFIED_UNSAT only when the whole finite tree closes by certified deductions with no UNKNOWN/verifier-rejection/budget truncation; every SOLVED carries a verifier report; budgets return UNKNOWN/BUDGET_EXHAUSTED, never unsat. - tests/test_dsl/test_solver_controller.py: tiny fixtures for deductions-before- decision, solve after one/many decisions, rollback-to-alternate, certified unsat vs unknown-prevents-unsat, terminal-verifier-failure backtrack, nogood-not-a- deduction, ranker permutation validation, adversarial-ranker membership safety, determinism, and budget stops. - solver/__init__ exports; docs add the search state machine + the certified- deduction/reversible-decision/local-nogood/certified-contradiction/timeout table to verified-scope-solver.md and a controller note to lattice-recursive-search.md. Verified: pytest test_solver_controller.py test_lattice_search.py + full solver suite (94 passed), full-repo ruff, repo_policy, git diff --check. Stacked on SLM-61. The lattice-search compatibility tests pass unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
VSS1-03 wires certificate-checked exact closure into the compiler-tree / choice decode path behind a disabled-by-default feature flag. When verified_solver_decode is on, _compiler_ltr_decode_one prunes the authoritative CompletionForest to the certified live subset before any soft ranking; the model then scores only surviving candidates. - dsl/solver/decode.py: solver_prune adapts the forest to a one-hole FiniteDomainState, runs exact_closure, and removes only candidates that were certified UNSUPPORTED with a replay-valid certificate (removed = input_domain - survivors). UNKNOWN stays live (keep_and_rank); survivors keep full CompletionPath identity, forced suffixes, and forest order, so a soft ranker can never reintroduce a removed candidate. A certified bottom yields an empty forest so the existing dead-end/rollback path runs rather than an unverified fallback. Torch-free. - models/twotower.py: _solver_prune_forest builds the OpenUI expander/verifier provider and calls solver_prune; guarded by a single getattr so default decode is byte-identical. An unsupported tokenizer/pack raises a capability error instead of silently taking a weaker path. - Eight backward-compatible config fields on TwoTowerConfig and ModelBuildConfig (verified_solver_decode + solver_*), plumbed through factory.apply_runtime_overrides and scripts/evaluate_model.py; missing fields on old checkpoints default. No new model parameter. Tests: tests/test_dsl/test_solver_decode.py (Torch-free removal / keep / certified-bottom / coverage / policy) and tests/test_models/test_solver_decode_integration.py (disabled-mode byte parity, config/checkpoint round-trip, real-closure subset, capability error, seam gated by the flag). Disabled by default; the enabled path is unmeasured. No train, eval, benchmark, or checkpoint ran, and this makes no correctness, speed, or ship claim. Docs updated: verified-scope-solver.md, lattice-recursive-search.md, quality-experiment-matrix.md config glossary, MODEL_CARD.md (flag exists and is unmeasured; no checkpoint row). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
|
Warning Review limit reached
Next review available in: 54 minutes Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (11)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
This was referenced Jul 18, 2026
# Conflicts: # docs/design/lattice-recursive-search.md # docs/design/verified-scope-solver.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
VSS1-03 — decode integration behind a disabled-by-default flag
Wires certificate-checked exact closure (VSS1-01) into the compiler-tree / choice
decode path so closure runs before soft ranking; the model then scores only
the surviving live candidate set. Gated by
verified_solver_decode(defaultoff), so default decode is byte-identical.
Stacked on #337 (SLM-62). Base branch is
claude/slm-62-search-controller; review after #337 merges.What changed
dsl/solver/decode.py(new) —solver_pruneadapts the authoritativeCompletionForestto a one-holeFiniteDomainState, runsexact_closure, andremoves only candidates certified
UNSUPPORTEDwith a replay-validcertificate (
removed = input_domain − survivors).UNKNOWNstays live(
keep_and_rank); survivors keep fullCompletionPathidentity, forcedsuffixes, and forest order — so a soft ranker can never reintroduce a
certified-removed candidate. A certified bottom yields an empty forest so
the existing dead-end/rollback path runs (never an unverified fallback).
Torch-free.
models/twotower.py—_solver_prune_forestbuilds the OpenUIexpander/verifier provider and calls
solver_prune, invoked in_compiler_ltr_decode_oneright afterbuild_completion_forest, behind asingle
getattrguard. An unsupported tokenizer/pack raises a capabilityerror rather than silently taking a weaker path while reporting solver mode.
TwoTowerConfigandModelBuildConfig(verified_solver_decode+solver_*),plumbed through
factory.apply_runtime_overridesandscripts/evaluate_model.py. Missing fields on existing checkpoints default; nonew model parameter.
verified-scope-solver.md(implemented section + reference row +dated note),
lattice-recursive-search.md(decode-integration subsection),quality-experiment-matrix.md(config glossary),MODEL_CARD.md(flag existsand is unmeasured; no checkpoint row).
Tests
tests/test_dsl/test_solver_decode.py— Torch-free: removes only certifiedUNSUPPORTED, keepsUNKNOWN, subset (ranker can't reintroduce), certifiedbottom → empty forest, non-
completecoverage untouched, policy guard.tests/test_models/test_solver_decode_integration.py— Torch model seam:disabled-mode byte parity (fixed seed/fixture), config/checkpoint round-trip
(+ old-checkpoint defaults),
_solver_prune_forestruns real closure andreturns a subset, capability error, and the decode loop invokes the seam only
when enabled.
Verified:
python -m pytest tests/test_models/test_solver_decode_integration.py tests/test_models/test_compiler_decode.py tests/test_dsl/test_solver_decode.py tests/test_dsl/test_solver_controller.py -q(all pass) andpython -m scripts.repo_policy(ok).ruff checkclean;git diff --checkclean.
Honesty
Disabled by default; the enabled path is unmeasured. No train, eval,
benchmark, or checkpoint ran, and this makes no correctness, speed, or ship
claim.
Follow-up (not in this PR): the closure
status/certificate (solver_certificate_mode)is computed but not yet surfaced into decode stats/trace; wiring that into the
trace store is a documented next step.
Note on unrelated CI failures
The changed-file test hook also selects suites with failures that are
pre-existing on
main/ environmental, not introduced here (confirmed byrunning the same node IDs with this branch's changes stashed): AgentV Node SDK
absent (
npm cinot run), pack-verifier bridge unavailable,build_train_data/task_evalpublish CLIs, and thetest_dsl_tokenizervocab bound (≤480vs theDEFAULT_MACRO_SLOTS=64→ 500 vocab introduced by #275). None touch the solverdecode path.
Closes SLM-63.
🤖 Generated with Claude Code
https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
Generated by Claude Code