SLM-66: VSS2-02 capsule solve plans, SCC joint solving, and interface summaries#342
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
…ogramSpec scopes (SLM-65) - Add src/slm_training/data/progspec/capsules.py with DependencyKind, ScopeNode, ScopeEdge, VerificationCapsule, CapsuleGraph, and derive_capsule_graph. - Reuse derive_scope_contracts for stable statement scopes; build nodes only from STATEMENT contracts plus a synthetic root interface. - Attach nested component_call/child_list contracts as member paths on the nearest containing statement/root. - Walk the typed AST to add REFERENCE edges for binder uses, EXTERNAL edges for slot/template inputs, and ROOT_OUTPUT edge. - Detect forward references/undefined binders and fail closed. - Compute SCC-derived capsules with Tarjan. - Export public names from slm_training.data.progspec. - Add regression tests in tests/test_data/test_progspec.py. - Document in docs/design/vss2-01-verification-capsules.md. Caveats: fixture wiring only; no model/ship claim.
…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
…ce summaries SLM-66 - Add capsule_solver.py with topological solve plans, SCC joint problems, predecessor blocking, input/output flow, and local/global disagreement recording. All dataclasses are JSON-round-trippable. - Extend DslPack with optional capsule hooks (problem builder, summary extractor, materializer, local/global oracle). - Add to_dict/from_dict to TerminalOutcome, SearchDecision, Nogood, SearchResult, and CertifiedDeduction to support result serialization. - Tweak enumerative oracle to prefer unresolved holes for multi-hole children. - Fix latent pack registration bug: _ensure_builtin_packs now uses a _BUILTINS_LOADED flag so early register_pack calls no longer hide builtins. - Add 10 regression tests in tests/test_dsl/test_capsule_solver.py and docs/design/vss2-02-capsule-solver.md. Verified: 110 targeted tests passed; full changed-check 418 passed, 5 skipped; repo_policy ok; git diff --check clean.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
|
Warning Review limit reached
Next review available in: 42 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 (8)
✨ 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 |
# Conflicts: # docs/design/lattice-recursive-search.md # docs/design/verified-scope-solver.md # src/slm_training/dsl/solver/__init__.py # src/slm_training/dsl/solver/closure.py # src/slm_training/dsl/solver/controller.py # src/slm_training/dsl/solver/support.py
Tyler-R-Kendrick
force-pushed
the
slm-66-vss2-02-capsule-solver
branch
from
July 18, 2026 05:17
acdbc74 to
e76bc2b
Compare
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.
Closes SLM-66.
What changed
src/slm_training/dsl/solver/capsule_solver.pywith deterministic topological solve plans, SCC joint-problem detection, predecessor blocking, input/output flow, local/global verifier disagreement recording, and JSON-round-trippable result types.DslPackwith optional capsule hooks (capsule_problem_builder,capsule_summary_extractor,capsule_materializer,capsule_local_oracle,capsule_global_oracle).TerminalOutcome,SearchDecision,Nogood,SearchResult, andCertifiedDeduction.openui/toy-layout/graphql.tests/test_dsl/test_capsule_solver.py.docs/design/vss2-02-capsule-solver.md.Verified
pytest tests/test_dsl/test_capsule_solver.py tests/test_dsl/test_solver_*.py tests/test_data/test_progspec.py -q→ 110 passed..githooks/check-changed→ 418 passed, 5 skipped, 12 deselected.python -m scripts.repo_policyok;git diff --checkclean.Caveats