Add bounded proof-carrying search controller (SLM-62)#337
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
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
📝 WalkthroughWalkthroughAdds a generic bounded proof-carrying search controller with certified closure, reversible branching, validated candidate ranking, structured outcomes, public package exports, design documentation, and tests covering soundness, determinism, and budget handling. ChangesProof-carrying search controller
Estimated code review effort: 4 (Complex) | ~45 minutes Sequence Diagram(s)sequenceDiagram
participant Caller
participant SearchController
participant SupportProvider
participant TerminalChecker
Caller->>SearchController: submit state and bounds
SearchController->>SupportProvider: request exact closure
SupportProvider-->>SearchController: certified deductions or outcome
SearchController->>SearchController: branch, backtrack, and record nogoods
SearchController->>TerminalChecker: verify solved state
TerminalChecker-->>SearchController: terminal result
SearchController-->>Caller: return SearchResult
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 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
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 5
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/design/verified-scope-solver.md`:
- Line 284: Update the “local nogood” row in the verified-scope solver
documentation to remove budget from the listed conflict-record causes. Keep
budget exhaustion classified only as an incomplete-search outcome, while
preserving the remaining nogood cases and the requirement for later
support-query certification.
In `@src/slm_training/dsl/solver/controller.py`:
- Around line 358-368: Validate the hole_id returned by hole_selector before
calling current.domain(hole_id) in the branching flow. Require it to identify an
existing domain with more than one live value; otherwise handle it through the
existing no_branching_hole backtracking/result path, preventing exceptions and
repeated no-op decisions.
- Around line 335-341: Update the structurally solved branch in the controller
method containing terminal_checker.check so an accepted TerminalOutcome is
returned as SOLVED only when outcome.report is present; otherwise reject or
downgrade it according to the existing search-status behavior. Add a focused
test covering accepted=True with report=None and verifying the documented result
contract.
- Around line 276-304: Separate backtrack budget exhaustion from complete
search-tree exhaustion in backtrack() and its callers so certified UNSAT is
reported only when no alternatives remain. Enforce max_decisions before
recording every alternative decision and max_nodes before each closure
transition, including paths around the logic at lines 308–356. Add regressions
covering zero backtracks with a live sibling, an alternative exceeding
max_decisions, and a second closure exceeding max_nodes; leave one runnable
assert-based check or focused test file.
- Around line 265-274: Update record_nogood and its callers so each
Nogood.assignment contains the complete active decision stack through the
conflicting frame, rather than only the frame’s hole_id and chosen value.
Preserve decision order and include parent assignments before the conflicting
decision, so distinct contextual conflicts retain distinct keys and valid
assignments are not overgeneralized.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro Plus
Run ID: c903faad-8928-416d-887d-195b8061d465
📒 Files selected for processing (5)
docs/design/lattice-recursive-search.mddocs/design/verified-scope-solver.mdsrc/slm_training/dsl/solver/__init__.pysrc/slm_training/dsl/solver/controller.pytests/test_dsl/test_solver_controller.py
| | --- | --- | --- | | ||
| | **certified deduction** | No | `exact_closure` removal with a replay-valid `UNSUPPORTED` certificate. | | ||
| | **reversible decision** | Yes | A ranker-ordered live value on the trail; undone on backtrack. Creates no legality. | | ||
| | **local nogood** | Yes (request-local) | A conflict record (`certified_bottom` / `terminal_verifier_failure` / budget). **Never** a certified deduction unless a later support query certifies it. | |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Do not classify budget truncation as a nogood.
A budget stop provides no evidence that the current assignment conflicts. Remove / budget from this row; budget exhaustion must remain only an incomplete-search outcome.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/design/verified-scope-solver.md` at line 284, Update the “local nogood”
row in the verified-scope solver documentation to remove budget from the listed
conflict-record causes. Keep budget exhaustion classified only as an
incomplete-search outcome, while preserving the remaining nogood cases and the
requirement for later support-query certification.
Comment on lines
+265
to
+274
| def record_nogood(hole_id: HoleId, value: DomainValue, provenance: str) -> None: | ||
| nogood = Nogood( | ||
| problem_id=current.problem_id, | ||
| constraint_version=current.constraint_version, | ||
| bounds=current.bounds, | ||
| assignment=((hole_id, value),), | ||
| provenance=provenance, | ||
| ) | ||
| if all(existing.key != nogood.key for existing in nogoods): | ||
| nogoods.append(nogood) |
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win
Record the complete decision context in each nogood.
A child conflict currently records only (frame.hole_id, frame.chosen). That value may be valid under another parent assignment, so the emitted unary nogood is false and deduplication can erase distinct contextual conflicts. Build assignment from the active stack through the conflicting frame.
Also applies to: 276-305
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/slm_training/dsl/solver/controller.py` around lines 265 - 274, Update
record_nogood and its callers so each Nogood.assignment contains the complete
active decision stack through the conflicting frame, rather than only the
frame’s hole_id and chosen value. Preserve decision order and include parent
assignments before the conflicting decision, so distinct contextual conflicts
retain distinct keys and valid assignments are not overgeneralized.
Comment on lines
+276
to
+304
| def backtrack(provenance: str) -> bool: | ||
| """Restore the latest pre-decision state and take the next alternative.""" | ||
| nonlocal current, level | ||
| while stack: | ||
| frame = stack[-1] | ||
| counters.backtracks += 1 | ||
| record_nogood(frame.hole_id, frame.chosen, provenance) | ||
| if counters.backtracks > max_backtracks: | ||
| return False | ||
| if frame.remaining: | ||
| frame.chosen = frame.remaining.pop(0) | ||
| current = frame.pre_state.with_decision(frame.hole_id, frame.chosen) | ||
| level = frame.level + 1 | ||
| # The alternative is a fresh decision at the same point; log it so | ||
| # the whole trajectory (including backtracked attempts) replays. | ||
| counters.decisions += 1 | ||
| decisions.append( | ||
| SearchDecision( | ||
| decision_id=f"d{counters.decisions}", | ||
| before_fingerprint=frame.pre_state.fingerprint, | ||
| after_fingerprint=current.fingerprint, | ||
| level=level, | ||
| hole_id=frame.hole_id, | ||
| chosen=frame.chosen, | ||
| alternatives=tuple(frame.remaining), | ||
| ranker_id=ranker.ranker_id, | ||
| ) | ||
| ) | ||
| return True |
There was a problem hiding this comment.
🎯 Functional Correctness | 🔴 Critical | 🏗️ Heavy lift
Do not conflate budget exhaustion with complete tree exhaustion.
backtrack() returns False both when the stack is exhausted and when max_backtracks is exceeded. A certified-bottom branch can therefore produce CERTIFIED_UNSAT while unexplored alternatives remain. Alternative decisions also bypass max_decisions, and the next closure can exceed max_nodes before that budget is checked.
Return a distinct backtrack-budget outcome and enforce decision/node limits before every corresponding transition. Add regressions for zero backtracks with a live sibling, an alternative exceeding max_decisions, and a second closure exceeding max_nodes.
As per coding guidelines, “Non-trivial logic must leave one runnable check behind, such as an assert-based self-check or one small test file.”
Also applies to: 308-356
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/slm_training/dsl/solver/controller.py` around lines 276 - 304, Separate
backtrack budget exhaustion from complete search-tree exhaustion in backtrack()
and its callers so certified UNSAT is reported only when no alternatives remain.
Enforce max_decisions before recording every alternative decision and max_nodes
before each closure transition, including paths around the logic at lines
308–356. Add regressions covering zero backtracks with a live sibling, an
alternative exceeding max_decisions, and a second closure exceeding max_nodes;
leave one runnable assert-based check or focused test file.
Source: Coding guidelines
Comment on lines
+335
to
+341
| if current.is_structurally_solved: | ||
| outcome = terminal_checker.check(current) | ||
| counters.verifier_calls += 1 | ||
| if outcome.accepted: | ||
| return _result(SearchStatus.SOLVED, current, outcome.source, | ||
| outcome.report, deductions, decisions, nogoods, counters, | ||
| None) |
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win
Require a verifier report before returning SOLVED.
TerminalOutcome(accepted=True, report=None) currently yields SOLVED, violating the documented result contract. Reject or downgrade an accepted outcome without a report, and add a test for this case.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/slm_training/dsl/solver/controller.py` around lines 335 - 341, Update the
structurally solved branch in the controller method containing
terminal_checker.check so an accepted TerminalOutcome is returned as SOLVED only
when outcome.report is present; otherwise reject or downgrade it according to
the existing search-status behavior. Add a focused test covering accepted=True
with report=None and verifying the documented result contract.
Comment on lines
+358
to
+368
| hole_id = hole_selector(current) | ||
| if hole_id is None: # defensive: no unresolved hole though not solved | ||
| saw_uncertified = True | ||
| if not backtrack("no_branching_hole"): | ||
| return _result(SearchStatus.UNKNOWN, current, None, None, deductions, | ||
| decisions, nogoods, counters, "no_branching_hole") | ||
| continue | ||
| live = current.domain(hole_id).values | ||
| permuted = ranker.rank(current, hole_id, live) | ||
| _validate_permutation(permuted, live) # ranker cannot alter membership | ||
| chosen, alternatives = permuted[0], permuted[1:] |
There was a problem hiding this comment.
🩺 Stability & Availability | 🟡 Minor | ⚡ Quick win
Validate the selected hole before branching.
An injected selector can return a missing or singleton hole, causing an exception or repeated no-op decisions until budget exhaustion. Require the returned ID to identify a domain with more than one live value.
As per coding guidelines, “Always perform input validation at trust boundaries.”
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/slm_training/dsl/solver/controller.py` around lines 358 - 368, Validate
the hole_id returned by hole_selector before calling current.domain(hole_id) in
the branching flow. Require it to identify an existing domain with more than one
live value; otherwise handle it through the existing no_branching_hole
backtracking/result path, preventing exceptions and repeated no-op decisions.
Source: Coding guidelines
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.
Summary
Implements the bounded proof-carrying search controller for the Verified Scope Solving project (SLM-62 / VSS1-02): a deterministic controller that alternates exact closure (irreversible, certificate-backed deletion) with reversible branching where rankers order only the live values and never touch hard membership.
Ownership
Per the issue's choice, this is a new generic controller in
dsl/solver/controller.py. The existing compiler-forest searchLatticeSearchState(fastpath/lattice_search.py) is retained unchanged as the forest-specific adapter — its callers andtests/test_dsl/test_lattice_search.pyare untouched and still pass (the documented compatibility seam).Changes
dsl/solver/controller.py—search(state, provider, terminal_checker, *, ranker, hole_selector, max_decisions, max_backtracks, ...)plusSearchStatus(SOLVED/CERTIFIED_UNSAT/UNKNOWN/BUDGET_EXHAUSTED),CandidateRanker+BaselineRanker,TerminalChecker/TerminalOutcome,SearchDecision,Nogood,SearchResult. Smallest-live-domain hole selection (thenHoleId); the ranker's return is validated to be a permutation of the live values (missing/extra/duplicate → rejected); local nogoods are request-local with conflict provenance and are never serialized as certified deductions.dsl/solver/__init__.py— exports the controller API.verified-scope-solver.md; a controller note inlattice-recursive-search.md.Soundness (acceptance criteria)
CERTIFIED_UNSATis impossible when any required branch was UNKNOWN or budget-truncated — the whole finite tree must close by certified deductions with no UNKNOWN/verifier-rejection/budget truncation anywhere.SOLVEDincludes a final verifier report; a structurally-solved-but-verifier-rejected leaf is a conflict/backtrack, never relabeled solved.Verification
python -m pytest tests/test_dsl/test_solver_controller.py tests/test_dsl/test_lattice_search.py -q(green; 94 passed across the full solver + compat suite) · full-reporuff check .clean ·python -m scripts.repo_policyok ·git diff --checkclean.test_solver_controller.py(13 tests) pins deductions-before-decision, solve after one/many decisions, rollback-to-alternate,CERTIFIED_UNSATvs UNKNOWN-prevents-unsat, terminal-verifier-failure backtrack, nogood-is-not-a-deduction, ranker permutation validation, adversarial-ranker membership safety, determinism, and budget stops.🤖 Generated with Claude Code
Generated by Claude Code
Summary by CodeRabbit
New Features
Documentation
Tests