Add exhaustive tri-state support oracle and replayable certificates (SLM-60)#332
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
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
|
Warning Review limit reached
Next review available in: 23 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 (6)
✨ 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
Summary
Implements the deterministic tri-state support oracle for the Verified Scope Solving project (SLM-60 / VSS0-04): the first component allowed to produce
UNSUPPORTED. It decides whether a candidate at one hole of aFiniteDomainStateparticipates in at least one bounded, verifier-accepted completion, and distinguishes a proven absence from incomplete search.Changes
dsl/solver/support.py—SupportQuery,SupportCertificate,SupportResult,SearchCounters; theSupportOracle/ProblemExpander/Verifierprotocols; andEnumerativeSupportOracle. The search is iterative (no Python recursion), explores values in the canonicalHoleDomainorder (logit-independent), deduplicates byFiniteDomainState.fingerprint, and enforces everySolverBoundsbudget. Verdicts:SUPPORTED(verifier-accepted witness; a witness wins even if other branches stay partial),UNSUPPORTED(whole finite space exhausted with onlycompletecoverage and no witness →exhausted=True),UNKNOWN(anypartial/nonecoverage, unavailable capability, or budget stop — never from a timeout).replay_support_certificate(...)re-derives identity, reruns the deterministic search, and returns structured violations.dsl/solver/openui_support.py— the OpenUI wiring:OpenUIForestExpanderadvances a token prefix throughbuild_completion_forest+ the VSS0-03completion_forest_stateadapter (eos→terminal,none→dead,partial→incomplete);OpenUIWellFormedVerifierruns lang-corevalidatewhere a genuineParseErroris a hardREJECTbut a missing bridge / timeout /RuntimeErrorisUNAVAILABLE→UNKNOWN(the timeout-vs-UNSAT distinction the contract requires).dsl/solver/__init__.py— exports the new public API.verified-scope-solver.mdgains an implemented-oracle section (tri-state table, search ordercanonical-domain-value-v1, certificate schema v1, verifier profile, replay rules) + a dated status note;lattice-recursive-search.mdgains a prefix-global extendability vs. verifier-backed support subsection.Honesty
UNSUPPORTEDrequires an exhausted, fully-complete-coverage search; replay rejects a non-exhausted, incomplete-coverage, or budget-stoppedUNSUPPORTED, and rejects aSUPPORTEDwhose witness digest doesn't match a re-verified witness.UNKNOWNis accepted as honest but never as pruning authority.Verification
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 ·ruffclean ·python -m scripts.repo_policyok ·git diff --checkclean.tests/test_dsl/test_solver_support.py(18 tests) pins all three verdicts, witness-before-partial, duplicate-state suppression, determinism, stale-query/candidate rejection, JSON round-trip, torch-free, every replay rule, and an OpenUI wiring smoke.Honest caveat:
.githooks/check-changed --stagedsurfaces 13 failures in unrelated DSL/pack/tokenizer suites (vocab_size 500 != 480, bridge-unavailable QUARANTINE) — these are pre-existing environmental failures on the base branch, not introduced here; alldsl/solver/*tests pass.🤖 Generated with Claude Code
Generated by Claude Code