Persist and replay solver deductions, decisions, and metrics (SLM-64)#341
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
VSS1-04 makes every verified-solver transition replayable and measured on the existing decode trace + telemetry owners — no second trace store, no new output root, no custom format. - dsl/solver/replay.py (new, Torch-free): typed event builders (solver_state, support_result, certified_deduction, decision, backtrack, nogood, solver_terminal), mode-gated certificate serialization (none/summary/full), and solver_replay_violations — the ten VSS1-04 invariants as human-readable strings: fingerprint lineage, live-only removals + full-mode certificate tamper detection (same canonical-JSON digest as SupportCertificate.digest), unknown-never-removes, single-live decisions, backtrack lineage, nogood-not-a-deduction, solved-has-report, certified-unsat purity, counter agreement, and truncation honesty. Closure never claims "solved". - harnesses/distill/trace_store.py: decode trace schema version 2 -> 3 (backward-compatible v1/v2 readers), DecodeTraceRecorder.record_solver sidecar, and replay_violations extended to run the solver invariants on any solver events present (decode-only traces unaffected). - models/decode_stats.py: solver work-metric counters + solver_ms (separated from denoiser/projection), zero on the default path, surfaced only under metrics["decode_stats"] via aggregate_stats. - models/twotower.py: _record_solver_metrics folds closure counters into DecodeStats and, when a DecodeTraceRecorder is attached, emits the closure-subset events + a bounded certificate/counter sidecar. No-op when neither stats nor a recorder is active; the disabled decode path is unchanged. Events and certificates store only token/path ids and SHA-256 digests — never raw region/user text. Tests: tests/test_dsl/test_solver_replay.py (validator + real-ClosureResult round-trip + tamper) and tests/test_harnesses/distill/test_solver_trace.py (recorder capture, clean replay, counters, historical compat). Docs: meta-model-traces.md, telemetry.md, verified-scope-solver.md, and a dated fixture-evidence note. Fixture-grade wiring only; no train/eval/benchmark/checkpoint ran, and this makes no solver-quality, correctness, speed, or ship claim. 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: 49 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 (10)
✨ 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 # src/slm_training/models/twotower.py
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-04 — replayable + measured solver transitions
Makes every verified-solver transition replayable and measured on the existing
decode trace + telemetry owners — no second trace store, no new output root, no
custom format. Stacked on #340 (SLM-63); base is
claude/slm-63-solver-decode-flag.What changed
dsl/solver/replay.py(new, Torch-free) — typed event builders(
solver_state,support_result,certified_deduction,decision,backtrack,nogood,solver_terminal), mode-gated certificate serialization(
none/summary/full), andsolver_replay_violations— the ten VSS1-04invariants returned as human-readable strings.
harnesses/distill/trace_store.py— decode trace schemaversion 2 → 3(backward-compatible v1/v2 readers),
DecodeTraceRecorder.record_solversidecar,and
replay_violationsextended to run the solver invariants on any solverevents present (decode-only traces unaffected).
models/decode_stats.py— solver work-metric counters +solver_ms(separated from denoiser/projection), zero on the default path, surfaced only
under
metrics["decode_stats"]viaaggregate_stats.models/twotower.py—_record_solver_metricsfolds closure counters intoDecodeStatsand, when aDecodeTraceRecorderis attached, emits theclosure-subset events + a bounded certificate/counter sidecar. No-op when neither
stats nor a recorder is active; the disabled decode path is unchanged.
meta-model-traces.md,telemetry.md,verified-scope-solver.md,and a dated fixture-evidence note.
Replay invariants (the centerpiece)
Fingerprint lineage · certified deductions remove only live values and — in
fullmode — cite a present, digest-consistent certificate (tamper detection, using
the same canonical-JSON digest as
SupportCertificate.digest) ·unknownneverremoves · decisions select one live value and record the rest · backtracks restore
a recorded state/level · a
nogoodis never a certified deduction ·solvedcarries a verifier report ·
certified_unsatis impossible once anyunknown/budget/truncation appears · event counts match the sidecar counters · atruncated snapshot is reported non-replayable. Closure never claims
solved.Privacy
Events and certificates store only token/path ids and SHA-256 digests — never raw
region/user text (the terminal report summarizer drops non-allowlisted strings).
Tests
tests/test_dsl/test_solver_replay.py— validator (each invariant), a realClosureResult→ events → clean replay, and certificate tamper detection.tests/test_harnesses/distill/test_solver_trace.py— recorder captures areplayable stream, solver counters land in
DecodeStats/aggregate_stats(zerowhen disabled), historical decode-only trace still replays.
Verified:
python -m pytest tests/test_harnesses/distill tests/test_models/test_decode_stats.py tests/test_models/test_trace_store.py tests/test_runtime_trace.py tests/test_dsl/test_solver_replay.py tests/test_dsl/test_solver_decode.py tests/test_dsl/test_solver_controller.py tests/test_models/test_solver_decode_integration.py tests/test_models/test_compiler_decode.py -q→ 100 passed;python -m scripts.repo_policyok;ruff+git diff --checkclean.Honesty
Fixture-grade wiring only. No train/eval/benchmark/checkpoint ran; this makes no
solver-quality, correctness, speed, or ship claim.
Pre-existing CI note
As on the rest of this stack, the changed-file hook also selects suites with
failures pre-existing on
main/ environmental (AgentV Node SDK absent,pack-verifier bridge unavailable, build/publish CLIs, the
test_dsl_tokenizervocab bound from #275). None touch the solver trace/replay path.
Closes SLM-64.
🤖 Generated with Claude Code
https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
Generated by Claude Code