lab: optimization phase — fingering optimality gap (CP-SAT oracle vs production DP and human tabs)

.gitignore

@@ -24,3 +24,6 @@ rustc-ice-*.txt
 # proptest regression files (generated by the test runner; not committed)
 **/*.proptest-regressions
 TestResults/
+
+# Constraint Lab run outputs derived from licensed tab corpora (ADR-0005).
+/lab/out/

docs/decisions.log.md

@@ -2835,6 +2835,32 @@ Architectural decisions go to [`adr/`](adr/) instead.
   the GP6 half. The crate defect is upstream's to fix; this adapter no
   longer depends on it.
 
+- 2026-09-16 — In the context of the Constraint Lab's optimization phase
+  (SLOTHY-style "how far from the best admissible realization is Griff?"),
+  facing a production fingering DP that is exact for its own objective, we
+  decided to **measure the optimality gap against two references — a
+  CP-SAT optimum verified in-repo and the tab authors of a Guitar Pro
+  corpus — and to keep the external solver offline**, to achieve evidence
+  about which component limits fingering quality, accepting hours of solver
+  time for what the DP answers in milliseconds. Result
+  (`docs/audit/2026-09-fingering-optimality-gap.md`): the solver gap is zero
+  on all 9,150 lines for both v1 weight sets; the model gap is large (34.0%
+  per-note agreement on holdout songs, 31.8% for a lowest-fret heuristic,
+  37.2% ceiling over all v1-optimal fingerings); fitted weights and a
+  hand-position model reach ~40%; and a repeat-consistency global
+  constraint that tab authors satisfy in 98% of repeats does not raise
+  agreement. The objective, not the search and not the constraint
+  vocabulary, is what to improve next. (Numbers are pre-#198: GP7 pitches
+  were wrong in the corpus import; re-measured after the fix, holdout
+  agreement is v1 35.8%, lowest-fret 33.5%, v1 ceiling 36.2%, fitted models
+  ~44%, with every conclusion unchanged — see the audit's Correction; after
+  the tuplet fix #202: v1 35.4%, lowest-fret 33.0%, v1 ceiling 35.8%, fitted
+  models ~44%, conclusions again unchanged.)
+  Solver: OR-Tools CP-SAT via a local
+  venv adapter (`lab/cpsat/`), never a dependency; idea-level prior art
+  only (TablaZinc is MPL-2.0, `guitar-tab-generator` GPL-3.0 — no code
+  copied).
+
 - 2026-09-17 — In the context of GPIF imports losing note techniques in
   `guitarpro` 0.4.2 (the `Tapped` property never read; `HopoOrigin` and
   `HopoDestination` merged into one hammer flag), we decided to **restore

lab/README.md

@@ -51,6 +51,44 @@ evidence on disk always belongs to the run that produced it. The committed
 manifests record both `griff-lab-exact` and `minizinc/chuffed` runs
 (frontend and backend versions separately).
 
+## Optimization phase — fingering gap
+
+The SAT/UNSAT IR answers "does an admissible realization exist?". The
+optimization IR (`src/optir.rs`) adds an objective — binary hard tables plus
+unary/pair cost tables and weighted `|a − b|` / `[a ≠ b]` terms — so an
+external solver can report the *best* admissible realization. The solver is
+untrusted: `optir::verify_record` accepts an optimum only when the solver
+proved it, the witness is admissible, and the in-repo re-score equals the
+claim.
+
+First subject (`src/fingering.rs`, `src/bin/fingering_gap.rs`): monophonic
+fingering, measured two ways —
+
+- **against an external optimum**: the production objective (`v1`, mirrored
+  independently of `infer_positions`) and an experimental hand-position
+  model are exported as IR and solved by OR-Tools CP-SAT
+  (`cpsat/solve_opt.py`); the in-repo DPs are compared with the verified
+  optima, and a lexicographic agreement pass gives the tie-insensitive
+  ceiling of each model's agreement with the tab author;
+- **against human tablature**: per-note agreement with Guitar Pro tabs,
+  how often the human fingering is itself optimal under a model, and by how
+  much it is not — with song-level holdout for fitted weights.
+
+```sh
+cd lab
+cargo build --release --bin fingering_gap
+T=path/to/gp/tabs; O=out            # out/ is git-ignored (ADR-0005)
+./target/release/fingering_gap fit    --tabs $T --out $O
+./target/release/fingering_gap export --tabs $T --out $O --v1 v1=1,1,2,1 --hand hand-fit=0,0,0,2,1,3
+python -m pip install ortools        # any venv
+python cpsat/solve_opt.py $O/v1.problems.jsonl $O/v1.cpsat.jsonl --agreement
+./target/release/fingering_gap report --tabs $T --out $O --v1 v1=1,1,2,1 --hand hand-fit=0,0,0,2,1,3
+```
+
+Everything written to `--out` is corpus-derived and stays local; `report`
+archives aggregates only (`report.json`). Results:
+[`../docs/audit/2026-09-fingering-optimality-gap.md`](../docs/audit/2026-09-fingering-optimality-gap.md).
+
 ## Known spike limits (deliberate)
 
 - The reference solver is leaf-checked backtracking with two sound band

lab/cpsat/solve_opt.py

@@ -0,0 +1,206 @@
+"""OR-Tools CP-SAT adapter for the Constraint Lab optimization IR.
+
+Reads `griff.constraint-lab-opt` v1 problem records (JSON lines), solves each
+to proven optimality, and writes one solve record per problem (JSON lines, in
+input order) in the shape `optir::SolveRecord` parses. The adapter is an
+*untrusted* oracle: the Rust side re-scores every witness and accepts an
+optimum only when the solver proved it (`optir::verify_record`).
+
+Optional agreement pass (`--agreement`): lexicographically, at the proven
+optimum, maximize how many of the record's reference `(var, value)`
+pairs hold — the tie-insensitive ceiling of a model's agreement with a
+reference (e.g. the human tab).
+
+Escalation: every problem is first solved in a process pool with `--threads`
+workers and `--time-limit`; a record without a proven optimum (or, with
+`--agreement`, without a proven agreement pass) is re-solved sequentially with
+`--retry-threads` and `--retry-limit`, and its solver identity says so. On the
+first corpus run a single-worker search left ~2% of lines unproven after 120 s,
+while the multi-worker portfolio proved the same lines in about a second.
+
+Usage:
+    python solve_opt.py IN.jsonl OUT.jsonl [--jobs N] [--threads T]
+                        [--time-limit SECONDS] [--agreement]
+                        [--retry-threads T] [--retry-limit SECONDS]
+"""
+
+import argparse
+import json
+import multiprocessing as mp
+import sys
+import time
+
+import ortools
+from ortools.sat.python import cp_model
+
+SCHEMA = "griff.constraint-lab-opt"
+SCHEMA_VERSION = 1
+
+STATUS = {
+    cp_model.OPTIMAL: "optimal",
+    cp_model.FEASIBLE: "feasible",
+    cp_model.INFEASIBLE: "infeasible",
+    cp_model.MODEL_INVALID: "model_invalid",
+    cp_model.UNKNOWN: "unknown",
+}
+
+
+def build(problem):
+    """Encodes the IR as a CP-SAT model; returns (model, vars, objective)."""
+    m = cp_model.CpModel()
+    domains = [v["domain"] for v in problem["vars"]]
+    xs = [
+        m.NewIntVarFromDomain(cp_model.Domain.FromValues(d), v["name"])
+        for v, d in zip(problem["vars"], domains)
+    ]
+    for h in problem["hard"]:
+        if h["kind"] != "allowed":
+            raise ValueError(f"unknown hard kind {h['kind']}")
+        m.AddAllowedAssignments([xs[h["a"]], xs[h["b"]]], [tuple(t) for t in h["tuples"]])
+
+    terms = []
+    for i, t in enumerate(problem["objective"]):
+        kind = t["kind"]
+        if kind == "unary":
+            table = {v: c for v, c in t["costs"]}
+            dom = domains[t["var"]]
+            rows = [(v, table.get(v, 0)) for v in dom]
+            c = m.NewIntVarFromDomain(
+                cp_model.Domain.FromValues(sorted({r[1] for r in rows})), f"u{i}"
+            )
+            m.AddAllowedAssignments([xs[t["var"]], c], rows)
+            terms.append(c)
+        elif kind == "pair":
+            table = {(a, b): c for a, b, c in t["costs"]}
+            rows = [
+                (a, b, table.get((a, b), 0))
+                for a in domains[t["a"]]
+                for b in domains[t["b"]]
+            ]
+            c = m.NewIntVarFromDomain(
+                cp_model.Domain.FromValues(sorted({r[2] for r in rows})), f"p{i}"
+            )
+            m.AddAllowedAssignments([xs[t["a"]], xs[t["b"]], c], rows)
+            terms.append(c)
+        elif kind == "abs_diff":
+            da, db = domains[t["a"]], domains[t["b"]]
+            span = max(abs(max(da) - min(db)), abs(max(db) - min(da)))
+            d = m.NewIntVar(0, span, f"d{i}")
+            m.AddAbsEquality(d, xs[t["a"]] - xs[t["b"]])
+            terms.append(t["weight"] * d)
+        elif kind == "not_equal":
+            b = m.NewBoolVar(f"n{i}")
+            m.Add(xs[t["a"]] != xs[t["b"]]).OnlyEnforceIf(b)
+            m.Add(xs[t["a"]] == xs[t["b"]]).OnlyEnforceIf(b.Not())
+            terms.append(t["weight"] * b)
+        else:
+            raise ValueError(f"unknown objective kind {kind}")
+    objective = sum(terms) if terms else 0
+    return m, xs, objective
+
+
+def solver_for(threads, time_limit):
+    s = cp_model.CpSolver()
+    s.parameters.num_workers = threads
+    s.parameters.max_time_in_seconds = time_limit
+    return s
+
+
+def solve_one(args):
+    line, threads, time_limit, agreement, tag = args
+    rec = json.loads(line)
+    if rec.get("schema") != SCHEMA or rec.get("version") != SCHEMA_VERSION:
+        raise ValueError(f"unsupported record schema {rec.get('schema')}/{rec.get('version')}")
+    problem = rec["problem"]
+    started = time.perf_counter()
+    m, xs, objective = build(problem)
+    m.Minimize(objective)
+    s = solver_for(threads, time_limit)
+    status = s.Solve(m)
+    out = {
+        "id": rec["id"],
+        "fingerprint_hex": rec["fingerprint_hex"],
+        "solver": {
+            "name": "ortools/cp-sat",
+            "version": f"{ortools.__version__} (num_workers={threads}, time_limit={time_limit}s{tag})",
+        },
+        "status": STATUS.get(status, "unknown"),
+        "objective": None,
+        "bound": None,
+        "witness": None,
+        "wall_us": 0,
+        "agreement": None,
+    }
+    if status in (cp_model.OPTIMAL, cp_model.FEASIBLE):
+        out["objective"] = int(round(s.ObjectiveValue()))
+        out["bound"] = int(round(s.BestObjectiveBound()))
+        out["witness"] = [int(s.Value(x)) for x in xs]
+    out["wall_us"] = int((time.perf_counter() - started) * 1e6)
+
+    if agreement and status == cp_model.OPTIMAL and rec.get("reference"):
+        # Lexicographic in one solve: with scale = len(reference) + 1, the
+        # minimum of scale*cost - matches has the minimum cost first and the
+        # most matches among cost-optimal assignments second. (Pinning
+        # `objective == optimum` as a constraint is far slower in CP-SAT.)
+        m2, xs2, objective2 = build(problem)
+        matches = []
+        for var, value in rec["reference"]:
+            b = m2.NewBoolVar(f"ref{var}")
+            m2.Add(xs2[var] == value).OnlyEnforceIf(b)
+            matches.append(b)
+        for x, v in zip(xs2, out["witness"]):
+            m2.AddHint(x, v)
+        scale = len(matches) + 1
+        m2.Minimize(scale * objective2 - sum(matches))
+        s2 = solver_for(threads, time_limit)
+        status2 = s2.Solve(m2)
+        ag = {"status": STATUS.get(status2, "unknown"), "matched": None, "witness": None}
+        if status2 in (cp_model.OPTIMAL, cp_model.FEASIBLE):
+            ag["witness"] = [int(s2.Value(x)) for x in xs2]
+            ag["matched"] = int(sum(s2.Value(b) for b in matches))
+        out["agreement"] = ag
+    return json.dumps(out, separators=(",", ":"))
+
+
+def main():
+    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    ap.add_argument("input")
+    ap.add_argument("output")
+    ap.add_argument("--jobs", type=int, default=mp.cpu_count())
+    ap.add_argument("--threads", type=int, default=1)
+    ap.add_argument("--time-limit", type=float, default=120.0)
+    ap.add_argument("--agreement", action="store_true")
+    ap.add_argument("--retry-threads", type=int, default=mp.cpu_count())
+    ap.add_argument("--retry-limit", type=float, default=300.0)
+    a = ap.parse_args()
+
+    with open(a.input, encoding="utf-8") as f:
+        lines = [l for l in f if l.strip()]
+    work = [(l, a.threads, a.time_limit, a.agreement, "") for l in lines]
+    started = time.perf_counter()
+    results = []
+    with mp.Pool(a.jobs) as pool:
+        for i, result in enumerate(pool.imap(solve_one, work, chunksize=1), 1):
+            results.append(result)
+            if i % 500 == 0 or i == len(work):
+                print(f"{i}/{len(work)} solved, {time.perf_counter() - started:.1f}s", file=sys.stderr)
+
+    def unproven(result):
+        r = json.loads(result)
+        if r["status"] != "optimal":
+            return True
+        return a.agreement and r["agreement"] is not None and r["agreement"]["status"] != "optimal"
+
+    retry = [i for i, r in enumerate(results) if unproven(r)]
+    print(f"escalating {len(retry)} unproven records", file=sys.stderr)
+    for n, i in enumerate(retry, 1):
+        results[i] = solve_one((lines[i], a.retry_threads, a.retry_limit, a.agreement, ", escalated"))
+        print(f"  escalated {n}/{len(retry)}, {time.perf_counter() - started:.1f}s", file=sys.stderr)
+
+    with open(a.output, "w", encoding="utf-8", newline="\n") as out:
+        for result in results:
+            out.write(result + "\n")
+
+
+if __name__ == "__main__":
+    main()