diff --git a/.gitignore b/.gitignore index 5b830d10..8310be96 100644 --- a/.gitignore +++ b/.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/ diff --git a/docs/audit/2026-09-fingering-optimality-gap.md b/docs/audit/2026-09-fingering-optimality-gap.md new file mode 100644 index 00000000..1efbea7d --- /dev/null +++ b/docs/audit/2026-09-fingering-optimality-gap.md @@ -0,0 +1,382 @@ +# 2026-09 — Fingering optimality gap (Constraint Lab optimization phase) + +The July oracle spike ([`2026-07-constraint-oracle-spike.md`](2026-07-constraint-oracle-spike.md)) +gave the Constraint Lab a SAT/UNSAT phase: *does an admissible realization +exist?* This increment adds the next question, borrowed from SLOTHY +(assembly superoptimization with CP-SAT, ): +*what does the **best** admissible realization cost, and how far from it is +what Griff produces?* — measured on monophonic fretboard fingering, against +two references: an external proven optimum and the tab authors of a real +Guitar Pro corpus. + +Research tooling only. `lab/` stays outside the workspace; no production +code, dependency, or `deny.toml` changed; OR-Tools lives in a local venv. + +## Correction (2026-09-17) — GP7 pitches were wrong in the data + +Chasing this audit's side finding exposed a larger import defect, fixed in +PhysShell/griff#198: GP7 (`.gp`) tracks imported a fallback Standard E +tuning while their notes stayed numbered from the low string, so **nearly +every GP7 note in the corpus had the wrong pitch** (0.2% matched the GPIF +`Midi` property). Positions stayed consistent with the wrong tuning, which is +why no check in this audit caught it. Every number in Results 1–4 below was +measured *before* that fix. + +Re-measured on the fixed importer (same corpus and protocol; 1,149 guitar +tracks, 9,045 lines, 326,130 notes; 7,091 train / 1,954 holdout lines; weights +refitted on train songs): + +| model | agreement, holdout (before → after) | human fingering optimal, holdout (after) | +|---|---|---| +| lowest fret | 31.8% → 33.5% | — | +| v1 production | 34.0% → 35.8% | 19.2% | +| v1-fit (after: fret 0, open +3 penalty, shift 1, string 0) | 40.1% → 44.1% | 30.9% | +| hand-fit (after: height 0, open 1, stretch 2, shift 0, shift_distance 2, string_distance 2) | 40.6% → 44.3% | 37.7% | + +CP-SAT on the holdout lines, fixed importer (every record verified): + +| model | proven | DP gap = 0 | DP agreement | ceiling at the optimum | +|---|---|---|---|---| +| v1 | 1,954 / 1,954 | 1,954 | 35.8% | **36.2%** | +| v1-fit | 1,954 / 1,954 | 1,954 | 44.1% | **55.5%** | + +What changes and what does not: + +- **Unchanged:** the solver gap is zero; the production weights barely beat + a lowest-fret heuristic; v1's optimal set caps agreement near its DP value + (36.2% vs 35.8%), so the objective is the limit. +- **Stronger:** the flat-objective reading of v1-fit — its optimal set + contains 55.5% agreement against the DP's 44.1%, an 11.4-point tie-break + loss. +- **Shifted:** fitted weights and absolute agreement (+2 to +4 points on + every model). The fitted hand model no longer beats fitted v1 on holdout + agreement (44.3% vs 44.1%); its advantage remains the human-optimal rate. +- **Not re-run:** the repeat-consistency experiment (Result 3) and the + hand-model oracle (Results 1 and 4). Neither conclusion depends on pitch + correctness in an obvious way, but their numbers are pre-fix. + +## Re-measured after #202 (2026-09-17) — tuplet durations + +PhysShell/griff#202 fixed a second import defect. The Guitar Pro importer +applied the tuplet ratio upside down, so every tuplet came out 9/4 too long, +and it ignored double dots. Bars with tuplets overflowed into the next bar, +and tab lines, which order notes by onset, interleaved notes from neighbouring +bars. The tables in the Correction above were measured before this fix. + +Re-measured on this branch merged with `main` at `e871a44`, with the same +corpus, protocol and weights. The weights were not refitted. + +- **Corpus.** 9,045 → 8,966 lines (holdout 1,954 → 1,945); 326,130 → 329,095 + notes. +- **Oracle.** The CP-SAT oracle was not rerun in full. For each model: + - 1,831 of the 1,945 holdout problems have unchanged fingerprints and keep + their verified records; + - the other 114 (46 with changed fingerprints, 68 new lines) were solved + again, agreement pass included. +- **Solver gap.** All 1,945 are proven optimal, and the DP gap is 0 on every + line for both models. + +| model | DP agreement, holdout | ceiling at the optimum | human fingering optimal | +|---|---|---|---| +| lowest fret | 33.5% → 33.0% | — | — | +| v1 production | 35.8% → 35.4% | 36.2% → 35.8% | 19.2% → 19.0% | +| v1-fit | 44.1% → 44.2% | 55.5% → 55.4% | 30.9% → 30.7% | +| hand-fit (DP only) | 44.3% → 44.7% | — | 37.7% → 37.3% | + +No conclusion above changes: + +- the solver gap is still zero; +- v1's optimum set still caps agreement near its DP value; +- v1-fit still loses about 11 points to ties (44.2% against a 55.4% ceiling). + +Results 1–4 stay as first measured, before both fixes. + +## What was built + +`lab/` (`griff-constraint-lab`), TDD red → green per commit: + +- **Optimization IR** (`src/optir.rs`) — finite integer variables, binary + hard tables, and an integer objective of unary/pair cost tables and + weighted `|a − b|` / `[a ≠ b]` terms; canonical tables and fingerprints. + The external solver is untrusted: `verify_record` accepts an optimum only + when the solver proved it, the witness is admissible, the in-repo re-score + equals the claim, and the bound equals the objective; `verify_agreement` + recounts the agreement pass and pins it to the optimum. +- **Fingering subject** (`src/fingering.rs`): + - `tab_lines` — monophonic runs of a GP track with the tab author's + `(string, fret)`; every refused note counted by cause; tracks always + emitted with string 1 = highest (see *Side finding*); + - `v1_cost` / `v1_problem` — the production `infer_positions` objective, + re-implemented independently and pinned against the production DP by + exhaustive brute force; + - `HandModel` — the finger-span layer ADR-0019 §7 defers: a hidden + index-finger position with a four-fret box, one-fret stretches, shift + event + shift distance, string distance, neck height, open strings. + `best_hands` scores fixed positions (a human tab) exactly; `solve_hand` + is the exact joint DP with a factored `O(K²H + KH²)` step; both pinned + against brute force; + - `repeat_pairs` / `with_repeat_consistency` / `with_string_tiebreak` — + the global constraint experiment below. +- **Runner** (`src/bin/fingering_gap.rs`): `fit`, `export`, `report`, + `repeat-export`, `repeat-report`. `report` rebuilds every problem from the + tabs and verifies every solver record before counting it. +- **CP-SAT adapter** (`cpsat/solve_opt.py`, OR-Tools 9.15.6755): proven + optimum, bound, witness; a lexicographic agreement pass + (`min scale·cost − matches`); two-tier solving (pool of single-worker + solves with a 5 s limit, then a 16-worker portfolio with 300 s for anything + unproven — the tier is recorded in the solver identity). + +## Corpus and protocol + +- 410 Guitar Pro files (GP3/4/5/6/7, swancore-first), 407 imported, 1,177 + guitar tracks (`select_ingest_tracks`). Content fingerprint + `9e53e55a19cddf29`; tabs are licensed material and never enter git — + problems, solver records and per-line data stay in the git-ignored + `lab/out/` (ADR-0005). Only aggregates are recorded here. +- Line cut (`LineCut::v1`): single-note onsets with explicit positions, + ≥ 4 notes; chords, unpositioned notes, positions above fret 24, + pitch/position mismatches and rests ≥ 4 quarters end a line. Of 1,216,035 + note atoms, **331,670 (27%) sit in 9,150 kept lines**; the rest are chord + onsets (292,992 onsets), frets above 24 (11,453 notes, mostly 35/36/99 + placeholders in non-guitar parts), short runs (17,376 notes), unpositioned + (64). Pitch/position mismatches: 0. 156 tracks were mirrored. +- **Song-level holdout**: `holdout_bucket(song_key, 5) == 0` is test — + 208 train / 51 test songs, 7,196 / 1,954 lines, 260,737 / 70,933 notes; + arrangements of one song (`(ver 2 by …)`) share a key. +- Machine-generated tabs would inflate agreement (prior art warns about + DadaGP): files with ≥ 50 kept notes that agree ≥ 99% with a lowest-fret + baseline — **1 of 385**. + +## Result 1 — the production DP has no optimality gap + +`infer_positions` is an exact Viterbi for its own objective, so the +SLOTHY-style gap was expected to be zero; the Lab now proves it at corpus +scale instead of assuming it. + +| model | lines | proven by CP-SAT | verified | gap = 0 | gap > 0 | gap < 0 | escalated | +|---|---|---|---|---|---|---|---| +| v1 (production weights) | 9,150 | 9,150 | 9,150 | **9,150** | 0 | 0 | 519 | +| v1-fit | 9,150 | 9,150 | 9,150 | **9,150** | 0 | 0 | 748 | +| hand-fit (in-repo `solve_hand`) | 1,954 (holdout) | 1,930 | 1,930 | **1,930** | 0 | 0 | 350 | + +For the hand model, 24 holdout lines (1.2%) stayed unproven after the +16-worker, 60 s escalation; no claim is made for them. + +`gap < 0` would mean the IR encoding and the in-repo evaluator disagree; it +is a defect detector and stayed empty. Every optimum above was re-scored in +the repo before it counted. For the hand model the oracle comparison is a +differential test of the new DP against an independent declarative model; +the DP is additionally pinned against brute force in the contract suite. + +## Result 2 — the model gap to human tablature is large + +Per-note agreement with the tab author (string and fret), holdout songs: + +| model | weights | agreement (test) | all | exact lines (test) | human fingering optimal (test) | human excess p50 / p90 (test) | +|---|---|---|---|---|---|---| +| lowest fret (baseline) | — | 31.8% | 35.5% | 20.7% | — | — | +| v1 production | fret 1, open bonus 1, shift 2, string 1 | 34.0% | 36.7% | 18.9% | 19.0% | 45 / 489 | +| v1-fit | fret 0, open +4 penalty, shift 1, string 0 | 40.1% | 42.4% | 11.5% | 22.1% | 10 / 76 | +| hand-fit | height 0, open 0, stretch 0, shift 2, shift_distance 1, string_distance 3 | **40.6%** | 46.2% | 22.3% | 35.4% | 6 / 69 | + +(v1 fields: cost = `fret·w − [open]·open_string`; `open_string = −4` is a +penalty of 4 per open string. v1-fit: exhaustive grid of 2,205 integer +weight sets on train songs; hand-fit: coordinate descent from three starts, +366 weight sets evaluated.) + +**Reading the last two columns across models.** Only the agreement columns +compare models on a common scale. + +- *Human excess* is in each model's own cost units and is **not comparable + across rows**: v1 charges every note its fret number, so a tab author + playing at the 12th fret pays 12 per note before any movement, while the + fitted models have no per-note term at all. The drop from 45 to 6 mostly + reflects weight scale, not a better account of human choices. +- *Human fingering optimal* is scale-free but inflated by flat objectives: + the more fingerings tie at the optimum, the easier it is for the human one + to be among them. +- Neither is a training target: all-zero weights make every fingering + optimal (excess 0, 100% optimal). A scale-free diagnostic — the human + path's rank among candidates, or `(human − optimum) / (baseline − + optimum)` — is follow-up work; agreement on holdout songs remains the only + unbiased target used here. + +- The production weights barely beat "always the lowest fret" (34.0% vs + 31.8%) and make the human fingering optimal in only 19% of lines. +- Fitted on train songs only, both families gain ~6 points on unseen songs. + The fit is a local optimum over small integer grids, not a claim about the + best achievable weights. +- The hand model makes the human fingering optimal in 35% of test lines + (v1: 19%, v1-fit: 22%) while agreement moves only to 40.6%. Part of that + rise is the flatness caveat above, so it is a hint that the hand terms + describe human choices better, not a measurement of how much better. +- Tab authors avoid open strings: every fit turned the open-string bonus + into a penalty or zero. The hand model charges a crossed string three + times a fret of hand travel; the v1 family, which sees only whether the + string *changed*, set that weight to 0 — the distance, not the change, + carries the signal. + +**Tie-breaking is not the problem.** The agreement pass maximizes agreement +over *all* cost-optimal fingerings, so it is the ceiling any tie-break could +reach: + +| model | DP agreement (all lines) | ceiling at the optimum | +|---|---|---| +| v1 | 36.7% | 37.2% | +| v1-fit | 42.4% | **52.3%** | + +(The ceiling uses the human tab to break ties, so it is an upper bound, not +a predictor.) + +- **v1: the objective is the limit.** Even the most human-like of all + v1-optimal fingerings agrees on only 37.2% of notes; no tie-break or + search improvement can recover the rest. The weights have to change. +- **v1-fit: the objective is too flat.** With zero fret and string-change + weights, many fingerings tie, and the DP's tie-break loses 10 points + against what the optimal set contains. The fitted weights moved toward + humans but stopped distinguishing choices a guitarist does distinguish — + the missing terms, not the search, are the next gain. +- The hand model's agreement pass is the same lexicographic problem shape + and was not tractable in the session's budget (Result 4). + +## Result 3 — a global constraint the chain DP cannot hold + +Tab authors finger a repeated 6-note figure identically in **98.5%** of +23,635 repeat pairs (2,468 lines; single-pitch ostinati excluded); the +chain DPs do so in 84.8% (v1-fit) and 88.7% (hand-fit), because entry and +exit context pull repeats apart. Equality between distant notes is out of +reach of a first-order DP state, but it is a handful of equal-value tables in +the IR. Both variants use a deterministic string tie-break +(`with_string_tiebreak`) so the witnesses are comparable; the tie-broken +solver reproduced the DP's choices exactly (identical agreement and +consistency counts), so the constrained column differs from the DP by the +constraint alone. + +v1-fit, holdout songs, lines with a repeated figure (510 lines, 56,455 notes, +5,433 repeat pairs; every record verified): + +| | tab author | chain DP | solver (tie-break) | solver + repeat consistency | +|---|---|---|---|---| +| repeat pairs fingered identically | 98.2% | 82.2% | 82.2% | **100%** (enforced) | +| per-note agreement with the tab author | — | 41.3% | 41.3% | **40.2%** | + +- The constraint is cheap: it raised the model cost in 177 of 510 lines, + by a median of 0 and p90 of 3 cost units (max 108). +- **It does not move the model toward the tab author** — agreement drops by + 1.1 points. The human fingering satisfies the constraint in 460 of 510 + lines, but the cheapest *consistent* fingering under v1-fit is usually + not the human one. Consistency is a property humans have, not a cause of + their choices; with an objective this far from human preference, pinning + a human-true invariant does not import the preference. +- This is the SLOTHY lesson in its honest form: the solver can hold global + structure a DP cannot, but it optimizes whatever objective it is given. + The experiment isolates the objective — not the search, and not the + constraint vocabulary — as the component that limits Griff's fingering. + +The same experiment on the hand model was stopped: under the tie-break +scaling, 354 of 510 holdout lines were still unproven after the 5 s +first tier (Result 4). + +## Result 4 — what the oracle costs + +- In-repo DPs over all 331,670 notes: v1 in single-digit milliseconds, the + hand model in ~120 ms (16 threads). +- CP-SAT per line (recorded wall time of the optimality solve, model build + included, agreement pass excluded; for escalated lines the accepted + multi-worker re-solve): + + | problem | lines | first tier unproven (5 s, 1 worker) | p50 | p99 | max | total | + |---|---|---|---|---|---|---| + | v1 | 9,150 | 519 (5.7%) | 19 ms | 2.8 s | 19 s | 1,507 s | + | v1-fit | 9,150 | 748 (8.2%) | 10 ms | 1.4 s | 142 s | 939 s | + | v1-fit + tie-break (repeat lines) | 510 | 60 (12%) | | | | 400 s | + | v1-fit + tie-break + repeat consistency | 510 | 33 (6.5%) | | | | 342 s | + | hand-fit + tie-break (repeat lines) | 510 | **354 (69%)** | | | | stopped | + | hand-fit (holdout, no agreement pass) | 1,954 | 350 (18%) | 61 ms | 60 s (limit) | 61 s | 3,676 s | + +- With one worker and a 120 s limit, ~2% of v1 lines (80–357 notes) stayed + unproven; a 16-worker portfolio proved the same lines in 0.2–1.1 s, while + a tighter local-marginal encoding with one worker still timed out on one + of five — search strategy, not formulation, was the bottleneck. +- The hidden hand position (21 values per note) and any lexicographic + scaling (tie-break, agreement pass) push CP-SAT from milliseconds to + tens of seconds per line; the in-repo DP is unaffected by either. The + repeat constraint, by contrast, made proofs *easier* (it prunes). +- The first full-corpus hand-model run with the agreement pass was stopped + after 1.5 h in its escalation tier; the holdout run without it took about + an hour of wall time for what `solve_hand` does over the whole corpus in + ~120 ms, and still left 24 lines unproven. + +The contract's standing decision holds with evidence: an external solver in +the production path would cost four to five orders of magnitude of latency +for problems a DP solves exactly, and its cost is sensitive to modelling +details a DP does not see. As an offline oracle over a sample it is cheap +enough and it found what it was asked to find. + +## Side finding — GPIF imports mirror string numbering (and GP7 pitches) + +156 guitar tracks — nearly all `.gpx` (GP6/GPIF) — import with a strictly +ascending tuning: string 1 is the *lowest* string, against the glossary's +string 1 = highest. Pitches stay consistent (tuning and positions are +mirrored together, which is why 9073de1's index fix did not surface it), but +anything orientation-sensitive — the DP's "lowest string first" tie-break, +tab rendering, `Tuning` equality — flips with the file format. The Lab +normalizes lines (`CutStats::mirrored_tracks`). + +Following it up against the GPIF `Midi` note property found the GP7 half: +the `guitarpro` crate never reads a staff-level tuning, so GP7 tracks got a +high-first Standard E and wrong pitches (see *Correction* above). Both are +fixed at the import boundary in PhysShell/griff#198. + +## Limitations (recorded, not hidden) + +- Monophonic lines only: 73% of corpus notes are in chords or cut away. + Chord voicing (inventory rule 2) remains the next oracle target. +- Agreement treats one human tab as ground truth; real alternatives exist, + and GP authoring (copy-paste) inflates repeat consistency. +- Techniques are ignored: tapping, slides, legato and harmonics change what + "hand position" means, and swancore uses them heavily. +- Weights were fitted by agreement with small integer grids and coordinate + descent; a structured-perceptron / path-difference learner is the obvious + next step. +- CP-SAT witnesses are not deterministic across worker counts; every claim + above rests on verified optima and recounts, not on witness identity. +- The hand model's `h` domain spans frets 1–21 with a fixed four-fret box + and no per-finger assignment (ADR-0019 §7 remains open). + +## Prior art (surveyed before the experiment) + +- Human-tab agreement: MIDI-to-Tab (ISMIR 2024) reports Guitar Pro 8 at + 62.3%, MuseScore 62.5%, a transformer 73.6% string agreement on 8,451 + held-out jazz notes (); + Fretting-Transformer (2025) reports a lowest-fret heuristic at 58.1% on + Leduc and 79.2% on DadaGP (). Neither + evaluates a DP of Griff's shape; swancore position playing is harder for + every heuristic. +- Hand-position costs: Hori & Sagayama (ISMIR 2016, index-finger state), + Radicioni & Lombardo (2005, neck height, string crossing, shift at phrase + boundaries), Heijink & Meulenbroek (2002, motion capture: shifts and + spans are costly). +- Learned weights: path difference learning (ICMC 2004). +- Solvers for fingering: TablaZinc (MiniZinc/Gecode, MPL-2.0), CPLEX in + Bontempi et al. (2024) and Tahon (2017); no CP-SAT use found. Idea reuse + only; no code copied. + +## Follow-ups proposed + +1. A `FingeringWeights` v2 decision (ADR or decisions log): the production + weights are the weakest calibrated component measured here — they barely + beat a lowest-fret heuristic and their optimal set caps agreement at 37%. + The fitted v1 weights are a better starting point but too flat; the hand + model's terms (shift event vs distance, string distance) belong in the + candidate v2 cost. +2. Replace grid/descent fitting with path-difference learning (a structured + perceptron over the same features), still scored on holdout songs, with + the agreement ceiling as the target to close. +3. Keep global constraints (repeat consistency) as Lab instruments, not + production rules: they are cheap for the solver and true of humans, but + they do not substitute for a better objective. Revisit once the + objective's ceiling rises. +4. Fix GP6 string orientation in `core/src/gp.rs` (separate change). +5. Chord voicing feasibility and optimization as the next Lab subject — + 73% of the corpus notes are outside monophonic lines. diff --git a/docs/decisions.log.md b/docs/decisions.log.md index bc56ac0c..3093053b 100644 --- a/docs/decisions.log.md +++ b/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 diff --git a/lab/README.md b/lab/README.md index 8fd52e10..f740e4fe 100644 --- a/lab/README.md +++ b/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 diff --git a/lab/cpsat/solve_opt.py b/lab/cpsat/solve_opt.py new file mode 100644 index 00000000..1c128ca2 --- /dev/null +++ b/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() diff --git a/lab/src/bin/fingering_gap.rs b/lab/src/bin/fingering_gap.rs new file mode 100644 index 00000000..60b51801 --- /dev/null +++ b/lab/src/bin/fingering_gap.rs @@ -0,0 +1,1278 @@ +//! Fingering optimality-gap runner — the Constraint Lab's optimization phase. +//! +//! Measures fingering models against two different references: +//! +//! 1. **An external optimum** (SLOTHY-style oracle): each model's objective is +//! exported as solver-neutral IR, solved by OR-Tools CP-SAT +//! (`cpsat/solve_opt.py`), and every returned optimum is re-verified here +//! (`optir::verify_record`) before it is compared with the in-repo DP. +//! 2. **Human tablature**: the `(string, fret)` choices of the tab authors in a +//! Guitar Pro corpus — per-note agreement, how often the human fingering is +//! itself optimal under the model, and by how much it is not. +//! +//! ```text +//! cargo run --release --bin fingering_gap -- fit --tabs DIR --out DIR +//! cargo run --release --bin fingering_gap -- export --tabs DIR --out DIR [MODELS] +//! python cpsat/solve_opt.py OUT/NAME.problems.jsonl OUT/NAME.cpsat.jsonl --agreement +//! cargo run --release --bin fingering_gap -- report --tabs DIR --out DIR [MODELS] +//! ``` +//! +//! Repeat consistency (a global constraint no chain DP state holds): +//! +//! ```text +//! cargo run --release --bin fingering_gap -- repeat-export --tabs DIR --out DIR [MODELS] +//! python cpsat/solve_opt.py OUT/NAME.tie.problems.jsonl OUT/NAME.tie.cpsat.jsonl +//! python cpsat/solve_opt.py OUT/NAME.tie-repeat.problems.jsonl OUT/NAME.tie-repeat.cpsat.jsonl +//! cargo run --release --bin fingering_gap -- repeat-report --tabs DIR --out DIR [MODELS] +//! ``` +//! +//! `MODELS`: `--v1 NAME=fret,open_string,position_shift,string_change` and +//! `--hand NAME=height,open_string,stretch,shift,shift_distance,string_distance`, +//! repeatable; default `--v1 v1=1,1,2,1` (the production weights). +//! +//! Corpus-derived files (problems, solver records, per-line records) stay in +//! `--out`, which is never committed — tab content is licensed material +//! (ADR-0005). `report` prints and archives aggregates only. + +use std::collections::{BTreeMap, HashMap}; +use std::fs; +use std::io::{BufRead, BufReader, BufWriter, Write}; +use std::path::{Path, PathBuf}; +use std::process::ExitCode; +use std::time::Instant; + +use griff_constraint_lab::fingering::{ + best_hands, decode_positions, hand_problem, holdout_bucket, repeat_pairs, solve_hand, song_key, + tab_lines, v1_cost, v1_problem, with_repeat_consistency, with_string_tiebreak, CutStats, + HandModel, HandWeights, LineCut, TabLine, HAND_VARS_PER_NOTE, V1_VARS_PER_NOTE, +}; +use griff_constraint_lab::ir::VarId; +use griff_constraint_lab::optir::{ + verify_agreement, verify_record, OptProblem, ProblemRecord, SolveRecord, Verdict, +}; +use griff_core::event::FretboardPosition; +use griff_core::fretboard::{infer_positions, FingeringWeights, STANDARD_MAX_FRET}; +use griff_core::gp::import_gp_score; +use griff_core::ingest::select_ingest_tracks; +use serde::Serialize; + +/// Song-level holdout: `holdout_bucket(song_key, 5) == 0` is the test split. +const HOLDOUT_BUCKETS: u64 = 5; + +// ── corpus ──────────────────────────────────────────────────────────────────── + +struct Line { + id: String, + file: usize, + test: bool, + tab: TabLine, +} + +#[derive(Serialize)] +struct CorpusFacts { + files: usize, + import_failures: usize, + guitar_tracks: usize, + songs_train: usize, + songs_test: usize, + lines_train: usize, + lines_test: usize, + notes_train: u64, + notes_test: u64, + /// FNV-1a 64 over the per-file content hashes, in file-name order. + corpus_fingerprint_hex: String, + cut: LineCut, + cut_stats: CutStats, +} + +struct Corpus { + names: Vec, + lines: Vec, + facts: CorpusFacts, +} + +fn fnv1a64(bytes: &[u8]) -> u64 { + bytes.iter().fold(0xcbf2_9ce4_8422_2325, |acc, &b| { + (acc ^ u64::from(b)).wrapping_mul(0x0000_0100_0000_01b3) + }) +} + +fn load(tabs: &Path, cut: &LineCut) -> std::io::Result { + let mut paths: Vec = fs::read_dir(tabs)? + .filter_map(Result::ok) + .map(|e| e.path()) + .filter(|p| p.is_file()) + .collect(); + paths.sort(); + let mut names = Vec::with_capacity(paths.len()); + let mut lines = Vec::new(); + let mut stats = CutStats::default(); + let (mut import_failures, mut guitar_tracks) = (0, 0); + let mut corpus_hash = Vec::with_capacity(paths.len() * 8); + let mut songs: BTreeMap = BTreeMap::new(); + for (file, path) in paths.iter().enumerate() { + let name = path + .file_name() + .map(|n| n.to_string_lossy().into_owned()) + .unwrap_or_default(); + let bytes = fs::read(path)?; + corpus_hash.extend_from_slice(&fnv1a64(&bytes).to_le_bytes()); + let key = song_key(&name); + let test = holdout_bucket(&key, HOLDOUT_BUCKETS) == 0; + names.push(name); + let Ok(score) = import_gp_score(&bytes) else { + import_failures += 1; + continue; + }; + songs.insert(key, test); + for track in select_ingest_tracks(&score, false) { + guitar_tracks += 1; + let Ok((track_lines, track_stats)) = tab_lines(&score, track, cut) else { + continue; + }; + stats.absorb(&track_stats); + lines.extend(track_lines.into_iter().map(|tab| Line { + id: format!( + "f{file:03}.t{}.v{}.at{}", + tab.track, tab.voice, tab.start_tick + ), + file, + test, + tab, + })); + } + } + let notes = |test: bool| { + lines + .iter() + .filter(|l| l.test == test) + .map(|l| l.tab.pitches.len() as u64) + .sum() + }; + let facts = CorpusFacts { + files: paths.len(), + import_failures, + guitar_tracks, + songs_train: songs.values().filter(|t| !**t).count(), + songs_test: songs.values().filter(|t| **t).count(), + lines_train: lines.iter().filter(|l| !l.test).count(), + lines_test: lines.iter().filter(|l| l.test).count(), + notes_train: notes(false), + notes_test: notes(true), + corpus_fingerprint_hex: format!("{:016x}", fnv1a64(&corpus_hash)), + cut: *cut, + cut_stats: stats, + }; + Ok(Corpus { + names, + lines, + facts, + }) +} + +fn par_map(items: &[T], f: impl Fn(&T) -> R + Sync) -> Vec { + let threads = std::thread::available_parallelism().map_or(1, std::num::NonZero::get); + let chunk = items.len().div_ceil(threads * 4).max(1); + let f = &f; + std::thread::scope(|scope| { + let handles: Vec<_> = items + .chunks(chunk) + .map(|c| scope.spawn(move || c.iter().map(f).collect::>())) + .collect(); + handles + .into_iter() + .flat_map(|h| h.join().expect("worker thread panicked")) + .collect() + }) +} + +// ── models ──────────────────────────────────────────────────────────────────── + +#[derive(Clone)] +enum Model { + /// Per note the lowest-fret candidate (prior-art baseline); no objective. + LowestFret, + /// The production DP (`infer_positions`) under the given weights. + V1 { + name: String, + weights: FingeringWeights, + }, + /// The hand-position model's exact DP. + Hand { name: String, model: HandModel }, +} + +struct Prediction { + positions: Vec, + /// The model's own cost of its prediction (`None` for the baseline). + cost: Option, +} + +impl Model { + fn name(&self) -> &str { + match self { + Self::LowestFret => "lowest-fret", + Self::V1 { name, .. } | Self::Hand { name, .. } => name, + } + } + + fn describe(&self) -> String { + match self { + Self::LowestFret => "lowest fret per note".into(), + Self::V1 { weights: w, .. } => format!( + "production DP, fret={} open_string={} position_shift={} string_change={}", + w.fret, w.open_string, w.position_shift, w.string_change + ), + Self::Hand { model, .. } => { + let w = model.weights(); + format!( + "hand DP, height={} open_string={} stretch={} shift={} shift_distance={} string_distance={}", + w.height, w.open_string, w.stretch, w.shift, w.shift_distance, w.string_distance + ) + } + } + } + + fn predict(&self, line: &TabLine) -> Prediction { + match self { + Self::LowestFret => Prediction { + positions: line + .pitches + .iter() + .map(|&p| { + line.tuning + .candidates(p, STANDARD_MAX_FRET) + .into_iter() + .min_by_key(|c| c.fret) + .expect("tab lines only hold positionable pitches") + }) + .collect(), + cost: None, + }, + Self::V1 { weights, .. } => { + let positions: Vec = + infer_positions(&line.pitches, &line.tuning, weights, STANDARD_MAX_FRET) + .into_iter() + .map(|p| p.expect("tab lines only hold positionable pitches")) + .collect(); + let cost = v1_cost(&positions, weights); + Prediction { + positions, + cost: Some(cost), + } + } + Self::Hand { model, .. } => { + let sol = solve_hand(&line.pitches, &line.tuning, model) + .expect("tab lines only hold positionable pitches"); + Prediction { + positions: sol.positions, + cost: Some(sol.cost), + } + } + } + } + + fn human_cost(&self, line: &TabLine) -> Option { + match self { + Self::LowestFret => None, + Self::V1 { weights, .. } => Some(v1_cost(&line.human, weights)), + Self::Hand { model, .. } => best_hands(&line.human, model).map(|b| b.0), + } + } + + fn problem(&self, line: &TabLine) -> Option<(OptProblem, usize)> { + match self { + Self::LowestFret => None, + Self::V1 { weights, .. } => { + v1_problem(&line.pitches, &line.tuning, weights, STANDARD_MAX_FRET) + .ok() + .map(|p| (p, V1_VARS_PER_NOTE)) + } + Self::Hand { model, .. } => hand_problem(&line.pitches, &line.tuning, model) + .ok() + .map(|p| (p, HAND_VARS_PER_NOTE)), + } + } +} + +fn human_reference(line: &TabLine, vars_per_note: usize) -> Vec<(VarId, i64)> { + line.human + .iter() + .enumerate() + .map(|(i, p)| (VarId(i * vars_per_note), i64::from(p.string))) + .collect() +} + +fn parse_list(raw: &str) -> Result, String> { + raw.split(',') + .map(|x| x.trim().parse::().map_err(|e| format!("{x:?}: {e}"))) + .collect() +} + +fn parse_model(flag: &str, spec: &str) -> Result { + let (name, weights) = spec + .split_once('=') + .ok_or_else(|| format!("{flag} expects NAME=w1,w2,…, got {spec:?}"))?; + let w = parse_list(weights)?; + match (flag, w.as_slice()) { + ("--v1", &[fret, open_string, position_shift, string_change]) => Ok(Model::V1 { + name: name.into(), + weights: FingeringWeights { + fret, + open_string, + position_shift, + string_change, + }, + }), + ("--hand", &[height, open_string, stretch, shift, shift_distance, string_distance]) => { + let weights = HandWeights { + height, + open_string, + stretch, + shift, + shift_distance, + string_distance, + }; + HandModel::new(weights, STANDARD_MAX_FRET) + .map(|model| Model::Hand { + name: name.into(), + model, + }) + .map_err(|e| e.to_string()) + } + _ => Err(format!("{flag} {spec:?}: wrong weight count")), + } +} + +// ── metrics ─────────────────────────────────────────────────────────────────── + +#[derive(Debug, Clone, Copy, Default, Serialize)] +struct Agreement { + notes: u64, + agree: u64, + lines: u64, + exact_lines: u64, +} + +impl Agreement { + fn of(human: &[FretboardPosition], predicted: &[FretboardPosition]) -> Self { + let agree = human.iter().zip(predicted).filter(|(a, b)| a == b).count() as u64; + let notes = human.len() as u64; + Self { + notes, + agree, + lines: 1, + exact_lines: u64::from(agree == notes), + } + } + + fn add(&mut self, other: Self) { + self.notes += other.notes; + self.agree += other.agree; + self.lines += other.lines; + self.exact_lines += other.exact_lines; + } + + #[allow(clippy::cast_precision_loss)] + fn rate(&self) -> f64 { + if self.notes == 0 { + 0.0 + } else { + self.agree as f64 / self.notes as f64 + } + } +} + +#[derive(Debug, Clone, Default, Serialize)] +struct Quantiles { + count: usize, + p50: i64, + p75: i64, + p90: i64, + p99: i64, + max: i64, +} + +#[allow( + clippy::cast_possible_truncation, + clippy::cast_sign_loss, + clippy::cast_precision_loss +)] +fn quantiles(mut values: Vec) -> Quantiles { + values.sort_unstable(); + let at = |q: f64| { + values + .get(((values.len().saturating_sub(1)) as f64 * q).round() as usize) + .copied() + .unwrap_or(0) + }; + Quantiles { + count: values.len(), + p50: at(0.5), + p75: at(0.75), + p90: at(0.9), + p99: at(0.99), + max: values.last().copied().unwrap_or(0), + } +} + +#[derive(Debug, Clone, Default, Serialize)] +struct SplitEval { + agreement: Agreement, + agreement_rate: f64, + /// Lines whose human fingering is optimal under the model. + human_optimal_lines: Option, + /// `cost(human) − cost(model optimum)` per line. + human_excess: Option, +} + +struct LineEval { + test: bool, + agreement: Agreement, + excess: Option, +} + +fn eval_line(model: &Model, line: &Line) -> LineEval { + let prediction = model.predict(&line.tab); + let excess = match (model.human_cost(&line.tab), prediction.cost) { + (Some(human), Some(best)) => Some(human - best), + _ => None, + }; + LineEval { + test: line.test, + agreement: Agreement::of(&line.tab.human, &prediction.positions), + excess, + } +} + +fn split_eval<'a>(evals: impl Iterator) -> SplitEval { + let mut agreement = Agreement::default(); + let mut excess = Vec::new(); + let mut has_cost = false; + for e in evals { + agreement.add(e.agreement); + if let Some(x) = e.excess { + has_cost = true; + excess.push(x); + } + } + SplitEval { + agreement, + agreement_rate: agreement.rate(), + human_optimal_lines: has_cost.then(|| excess.iter().filter(|&&x| x == 0).count() as u64), + human_excess: has_cost.then(|| quantiles(excess)), + } +} + +#[derive(Debug, Clone, Serialize)] +struct ModelEval { + name: String, + description: String, + all: SplitEval, + train: SplitEval, + test: SplitEval, + in_repo_ms: u128, +} + +fn evaluate(model: &Model, lines: &[Line]) -> ModelEval { + let started = Instant::now(); + let evals = par_map(lines, |l| eval_line(model, l)); + let in_repo_ms = started.elapsed().as_millis(); + ModelEval { + name: model.name().into(), + description: model.describe(), + all: split_eval(evals.iter()), + train: split_eval(evals.iter().filter(|e| !e.test)), + test: split_eval(evals.iter().filter(|e| e.test)), + in_repo_ms, + } +} + +fn train_agreement(model: &Model, train: &[&Line]) -> u64 { + par_map(train, |l| { + Agreement::of(&l.tab.human, &model.predict(&l.tab).positions).agree + }) + .into_iter() + .sum() +} + +// ── commands ────────────────────────────────────────────────────────────────── + +#[derive(Serialize)] +struct FitResult { + corpus: CorpusFacts, + v1_grid_evaluated: usize, + v1_best: [i64; 4], + hand_evaluated: usize, + hand_best: [i64; 6], + evaluations: Vec, +} + +fn fit(corpus: Corpus, out: &Path) -> std::io::Result<()> { + let train: Vec<&Line> = corpus.lines.iter().filter(|l| !l.test).collect(); + + // v1 family: exhaustive integer grid. + let started = Instant::now(); + let mut grid = Vec::new(); + for fret in 0..=4 { + for open_string in -4..=4 { + for position_shift in 0..=6 { + for string_change in 0..=6 { + grid.push([fret, open_string, position_shift, string_change]); + } + } + } + } + let mut v1_best = ([1, 1, 2, 1], 0_u64); + for w in &grid { + let model = Model::V1 { + name: String::new(), + weights: FingeringWeights { + fret: w[0], + open_string: w[1], + position_shift: w[2], + string_change: w[3], + }, + }; + let score = train_agreement(&model, &train); + if score > v1_best.1 { + v1_best = (*w, score); + } + } + eprintln!( + "v1 grid: {} weight sets in {:.1}s, best {:?}", + grid.len(), + started.elapsed().as_secs_f64(), + v1_best.0 + ); + + // Hand family: coordinate descent from several starts. + let ranges: [(i64, i64); 6] = [(-2, 3), (-6, 6), (0, 10), (0, 12), (0, 6), (0, 6)]; + let starts: [[i64; 6]; 3] = [[1, 0, 2, 4, 1, 1], [0, 0, 0, 0, 0, 0], [0, -2, 4, 8, 0, 2]]; + let hand = |w: [i64; 6]| Model::Hand { + name: String::new(), + model: HandModel::new( + HandWeights { + height: w[0], + open_string: w[1], + stretch: w[2], + shift: w[3], + shift_distance: w[4], + string_distance: w[5], + }, + STANDARD_MAX_FRET, + ) + .expect("ranges keep weights valid"), + }; + let mut cache: HashMap<[i64; 6], u64> = HashMap::new(); + let mut score_of = |w: [i64; 6]| { + *cache + .entry(w) + .or_insert_with(|| train_agreement(&hand(w), &train)) + }; + let mut hand_best = ([0_i64; 6], 0_u64); + for start in starts { + let mut current = (start, score_of(start)); + for pass in 0..8 { + let before = current.1; + for (coord, &(lo, hi)) in ranges.iter().enumerate() { + for value in lo..=hi { + let mut w = current.0; + w[coord] = value; + let s = score_of(w); + if s > current.1 { + current = (w, s); + } + } + } + eprintln!( + "hand descent from {start:?}, pass {pass}: {:?} agree {} ({:.1}s)", + current.0, + current.1, + started.elapsed().as_secs_f64() + ); + if current.1 == before { + break; + } + } + if current.1 > hand_best.1 { + hand_best = current; + } + } + let hand_evaluated = cache.len(); + + let models = [ + Model::LowestFret, + parse_model("--v1", "v1=1,1,2,1").expect("production weights"), + Model::V1 { + name: "v1-fit".into(), + weights: FingeringWeights { + fret: v1_best.0[0], + open_string: v1_best.0[1], + position_shift: v1_best.0[2], + string_change: v1_best.0[3], + }, + }, + match hand(hand_best.0) { + Model::Hand { model, .. } => Model::Hand { + name: "hand-fit".into(), + model, + }, + other => other, + }, + ]; + let evaluations: Vec = models.iter().map(|m| evaluate(m, &corpus.lines)).collect(); + print_table(&evaluations); + let result = FitResult { + corpus: corpus.facts, + v1_grid_evaluated: grid.len(), + v1_best: v1_best.0, + hand_evaluated, + hand_best: hand_best.0, + evaluations, + }; + write_json(&out.join("fit.json"), &result)?; + println!( + "\nsuggested models: --v1 v1-fit={} --hand hand-fit={}", + join(&v1_best.0), + join(&hand_best.0) + ); + Ok(()) +} + +fn join(values: &[i64]) -> String { + values + .iter() + .map(ToString::to_string) + .collect::>() + .join(",") +} + +fn export(corpus: &Corpus, models: &[Model], out: &Path) -> std::io::Result<()> { + { + let mut w = BufWriter::new(fs::File::create(out.join("lines.jsonl"))?); + for line in &corpus.lines { + let record = serde_json::json!({ + "id": line.id, + "file": corpus.names.get(line.file), + "test": line.test, + "notes": line.tab.pitches.len(), + "human": line.tab.human.iter().map(|p| [p.string, p.fret]).collect::>(), + }); + serde_json::to_writer(&mut w, &record).map_err(std::io::Error::other)?; + w.write_all(b"\n")?; + } + } + for model in models { + let path = out.join(format!("{}.problems.jsonl", model.name())); + let records = par_map(&corpus.lines, |line| { + model.problem(&line.tab).map(|(problem, vpn)| { + let record = + ProblemRecord::new(line.id.clone(), problem, human_reference(&line.tab, vpn)); + serde_json::to_string(&record).expect("problem records serialize") + }) + }); + let mut w = BufWriter::new(fs::File::create(&path)?); + let mut written = 0; + for record in records.into_iter().flatten() { + w.write_all(record.as_bytes())?; + w.write_all(b"\n")?; + written += 1; + } + eprintln!("{}: {written} problems → {}", model.name(), path.display()); + } + Ok(()) +} + +#[derive(Debug, Clone, Default, Serialize)] +struct OracleEval { + records: usize, + /// Records re-solved by the adapter's multi-worker escalation tier. + escalated: usize, + missing: usize, + proven: usize, + not_proven: usize, + fingerprint_mismatch: usize, + witness_invalid: usize, + objective_mismatch: usize, + /// In-repo DP cost equals the verified optimum. + gap_zero: usize, + /// In-repo DP cost above the verified optimum (the heuristic is suboptimal). + gap_positive: usize, + /// In-repo DP cost *below* the verified optimum — impossible unless the + /// encoding and the evaluator disagree; any count here is a defect. + gap_negative: usize, + max_gap: i64, + /// Agreement passes verified (recounted, pinned to the optimum). + agreement_verified: usize, + agreement_refused: usize, + /// Over lines with a verified agreement pass: notes, DP agreement, and the + /// tie-insensitive ceiling at the optimum. + ceiling_notes: u64, + ceiling_dp_agree: u64, + ceiling_best_agree: u64, + solver: Option, + solver_wall_us: Quantiles, + solver_total_s: f64, +} + +#[allow(clippy::cast_precision_loss)] +fn oracle_eval( + model: &Model, + lines: &[Line], + records: &HashMap, +) -> OracleEval { + struct One { + verdict: Option, + in_repo: Option, + agreement: Option>, + notes: u64, + dp_agree: u64, + wall_us: Option, + } + let ones = par_map(lines, |line| { + let Some(record) = records.get(&line.id) else { + return One { + verdict: None, + in_repo: None, + agreement: None, + notes: 0, + dp_agree: 0, + wall_us: None, + }; + }; + let (problem, vpn) = model.problem(&line.tab).expect("exported models build"); + let verdict = verify_record(&problem, record); + let prediction = model.predict(&line.tab); + let agreement = match (&verdict, &record.agreement) { + (Verdict::Proven { optimum }, Some(pass)) => Some( + verify_agreement(&problem, &human_reference(&line.tab, vpn), *optimum, pass) + .map_err(|_| ()), + ), + _ => None, + }; + One { + verdict: Some(verdict), + in_repo: prediction.cost, + agreement, + notes: line.tab.human.len() as u64, + dp_agree: Agreement::of(&line.tab.human, &prediction.positions).agree, + wall_us: Some(record.wall_us), + } + }); + let mut e = OracleEval { + records: records.len(), + escalated: records + .values() + .filter(|r| r.solver.version.contains("escalated")) + .count(), + ..OracleEval::default() + }; + let mut walls = Vec::new(); + for one in ones { + let Some(verdict) = one.verdict else { + e.missing += 1; + continue; + }; + if let Some(w) = one.wall_us { + walls.push(i64::try_from(w).unwrap_or(i64::MAX)); + } + match verdict { + Verdict::Proven { optimum } => { + e.proven += 1; + let gap = one.in_repo.unwrap_or(optimum) - optimum; + match gap.cmp(&0) { + std::cmp::Ordering::Equal => e.gap_zero += 1, + std::cmp::Ordering::Greater => e.gap_positive += 1, + std::cmp::Ordering::Less => e.gap_negative += 1, + } + e.max_gap = e.max_gap.max(gap); + } + Verdict::NotProven { .. } | Verdict::MissingWitness => e.not_proven += 1, + Verdict::FingerprintMismatch => e.fingerprint_mismatch += 1, + Verdict::WitnessInvalid(_) => e.witness_invalid += 1, + Verdict::ObjectiveMismatch { .. } => e.objective_mismatch += 1, + } + match one.agreement { + Some(Ok(best)) => { + e.agreement_verified += 1; + e.ceiling_notes += one.notes; + e.ceiling_dp_agree += one.dp_agree; + e.ceiling_best_agree += best; + } + Some(Err(())) => e.agreement_refused += 1, + None => {} + } + } + e.solver = records + .values() + .find(|r| !r.solver.version.contains("escalated")) + .map(|r| format!("{} {}", r.solver.name, r.solver.version)); + e.solver_total_s = walls.iter().sum::() as f64 / 1e6; + e.solver_wall_us = quantiles(walls); + e +} + +#[derive(Serialize)] +struct Report { + schema: &'static str, + version: u32, + corpus: CorpusFacts, + /// Files (≥ 50 kept notes) whose tab agrees ≥ 99% with the lowest-fret + /// baseline — candidates for machine-generated fingering. + lowest_fret_lookalike_files: usize, + files_with_50_notes: usize, + models: Vec, + oracle: BTreeMap, +} + +fn report(corpus: Corpus, models: &[Model], out: &Path) -> std::io::Result<()> { + let mut all_models = vec![Model::LowestFret]; + all_models.extend(models.iter().cloned()); + let evaluations: Vec = all_models + .iter() + .map(|m| evaluate(m, &corpus.lines)) + .collect(); + + let mut per_file: BTreeMap = BTreeMap::new(); + for (line, agreement) in corpus.lines.iter().zip(par_map(&corpus.lines, |l| { + Agreement::of(&l.tab.human, &Model::LowestFret.predict(&l.tab).positions) + })) { + per_file.entry(line.file).or_default().add(agreement); + } + let big: Vec<&Agreement> = per_file.values().filter(|a| a.notes >= 50).collect(); + let lookalikes = big.iter().filter(|a| a.rate() >= 0.99).count(); + + let mut oracle = BTreeMap::new(); + for model in models { + let path = out.join(format!("{}.cpsat.jsonl", model.name())); + let Ok(file) = fs::File::open(&path) else { + continue; + }; + let mut records = HashMap::new(); + for line in BufReader::new(file).lines() { + let line = line?; + if line.trim().is_empty() { + continue; + } + let record: SolveRecord = serde_json::from_str(&line).map_err(std::io::Error::other)?; + records.insert(record.id.clone(), record); + } + oracle.insert( + model.name().to_string(), + oracle_eval(model, &corpus.lines, &records), + ); + } + + print_table(&evaluations); + println!( + "\nlowest-fret look-alike files (≥50 notes, ≥99% agreement): {lookalikes} of {}", + big.len() + ); + print_oracle(&oracle); + let report = Report { + schema: "griff.constraint-lab-fingering-gap", + version: 1, + corpus: corpus.facts, + lowest_fret_lookalike_files: lookalikes, + files_with_50_notes: big.len(), + models: evaluations, + oracle, + }; + write_json(&out.join("report.json"), &report) +} + +#[allow(clippy::cast_precision_loss)] +fn print_table(evaluations: &[ModelEval]) { + println!("\n| model | agreement all | train | test (holdout songs) | exact lines (test) | human optimal (test) | human excess p50 / p90 (test) | in-repo ms |"); + println!("|---|---|---|---|---|---|---|---|"); + for e in evaluations { + let optimal = e.test.human_optimal_lines.map_or("—".into(), |n| { + format!( + "{:.1}%", + 100.0 * n as f64 / e.test.agreement.lines.max(1) as f64 + ) + }); + let excess = e + .test + .human_excess + .as_ref() + .map_or("—".into(), |q| format!("{} / {}", q.p50, q.p90)); + println!( + "| {} | {:.1}% | {:.1}% | {:.1}% | {:.1}% | {optimal} | {excess} | {} |", + e.name, + 100.0 * e.all.agreement_rate, + 100.0 * e.train.agreement_rate, + 100.0 * e.test.agreement_rate, + 100.0 * e.test.agreement.exact_lines as f64 / e.test.agreement.lines.max(1) as f64, + e.in_repo_ms + ); + } + for e in evaluations { + println!(" {}: {}", e.name, e.description); + } +} + +#[allow(clippy::cast_precision_loss)] +fn print_oracle(oracle: &BTreeMap) { + if oracle.is_empty() { + return; + } + println!("\n| model | records | not run | proven | not proven | invalid | gap = 0 | gap > 0 | gap < 0 | max gap | DP agreement | ceiling at optimum | solver p50 / p99 / max ms | solver total s |"); + println!("|---|---|---|---|---|---|---|---|---|---|---|---|---|---|"); + for (name, e) in oracle { + // No agreement pass verified: say so rather than print 0%. + let rate = |x: u64| { + if e.ceiling_notes == 0 { + "—".to_string() + } else { + format!("{:.1}%", 100.0 * x as f64 / e.ceiling_notes as f64) + } + }; + println!( + "| {name} | {} | {} | {} | {} | {} | {} | {} | {} | {} | {} | {} | {:.1} / {:.1} / {:.1} | {:.1} |", + e.records, + e.missing, + e.proven, + e.not_proven, + e.witness_invalid + e.objective_mismatch + e.fingerprint_mismatch, + e.gap_zero, + e.gap_positive, + e.gap_negative, + e.max_gap, + rate(e.ceiling_dp_agree), + rate(e.ceiling_best_agree), + e.solver_wall_us.p50 as f64 / 1e3, + e.solver_wall_us.p99 as f64 / 1e3, + e.solver_wall_us.max as f64 / 1e3, + e.solver_total_s + ); + } + for (name, e) in oracle { + if let Some(s) = &e.solver { + println!( + " {name}: {s}; escalated {}; agreement passes verified {} refused {}", + e.escalated, e.agreement_verified, e.agreement_refused + ); + } + } +} + +// ── repeat consistency ──────────────────────────────────────────────────────── + +/// Window of a repeated figure, in notes. +const REPEAT_WINDOW: usize = 6; + +/// The two solver variants of a line with repeats: the model under a +/// deterministic string tie-break (`tie`), and the same plus the +/// repeat-consistency constraint (`tie-repeat`). +fn repeat_variants(model: &Model, line: &TabLine) -> Option { + let pairs = repeat_pairs(&line.pitches, REPEAT_WINDOW); + if pairs.is_empty() { + return None; + } + let (base, vpn) = model.problem(line)?; + let (tie, scale) = with_string_tiebreak(&base, vpn).ok()?; + let constrained = with_repeat_consistency(&tie, vpn, &pairs, REPEAT_WINDOW).ok()?; + Some(RepeatVariants { + tie, + constrained, + scale, + vpn, + pairs, + }) +} + +struct RepeatVariants { + tie: OptProblem, + constrained: OptProblem, + scale: i64, + vpn: usize, + pairs: Vec<(usize, usize)>, +} + +fn repeat_export(corpus: &Corpus, models: &[Model], out: &Path) -> std::io::Result<()> { + for model in models { + let records = par_map(&corpus.lines, |line| { + repeat_variants(model, &line.tab).map(|v| { + let a = ProblemRecord::new(line.id.clone(), v.tie, Vec::new()); + let b = ProblemRecord::new(line.id.clone(), v.constrained, Vec::new()); + ( + serde_json::to_string(&a).expect("problem records serialize"), + serde_json::to_string(&b).expect("problem records serialize"), + ) + }) + }); + let tie_path = out.join(format!("{}.tie.problems.jsonl", model.name())); + let rep_path = out.join(format!("{}.tie-repeat.problems.jsonl", model.name())); + let mut tie_w = BufWriter::new(fs::File::create(&tie_path)?); + let mut rep_w = BufWriter::new(fs::File::create(&rep_path)?); + let mut written = 0; + for (a, b) in records.into_iter().flatten() { + tie_w.write_all(a.as_bytes())?; + tie_w.write_all(b"\n")?; + rep_w.write_all(b.as_bytes())?; + rep_w.write_all(b"\n")?; + written += 1; + } + eprintln!( + "{}: {written} lines with repeats → {}, {}", + model.name(), + tie_path.display(), + rep_path.display() + ); + } + Ok(()) +} + +fn read_records(path: &Path) -> std::io::Result> { + let mut records = HashMap::new(); + for line in BufReader::new(fs::File::open(path)?).lines() { + let line = line?; + if line.trim().is_empty() { + continue; + } + let record: SolveRecord = serde_json::from_str(&line).map_err(std::io::Error::other)?; + records.insert(record.id.clone(), record); + } + Ok(records) +} + +#[derive(Debug, Clone, Default, Serialize)] +struct RepeatEval { + lines: usize, + notes: u64, + pairs: u64, + /// Both variants proven and verified. + verified_lines: usize, + refused_lines: usize, + consistent_pairs_human: u64, + consistent_pairs_dp: u64, + consistent_pairs_tie: u64, + consistent_pairs_repeat: u64, + agree_dp: u64, + agree_tie: u64, + agree_repeat: u64, + agree_rate_dp: f64, + agree_rate_tie: f64, + agree_rate_repeat: f64, + /// Lines where the constraint raised the model cost, and by how much. + lines_cost_raised: usize, + cost_raise: Quantiles, + /// Lines where the human fingering satisfies the constraint. + human_consistent_lines: usize, + solver_total_s_tie: f64, + solver_total_s_repeat: f64, +} + +#[allow(clippy::cast_precision_loss, clippy::too_many_lines)] +fn repeat_report(corpus: &Corpus, models: &[Model], out: &Path) -> std::io::Result<()> { + let consistent = |positions: &[FretboardPosition], pairs: &[(usize, usize)]| { + pairs + .iter() + .filter(|&&(i, j)| { + positions.get(i..i + REPEAT_WINDOW) == positions.get(j..j + REPEAT_WINDOW) + }) + .count() as u64 + }; + let mut evals = BTreeMap::new(); + for model in models { + let tie = read_records(&out.join(format!("{}.tie.cpsat.jsonl", model.name())))?; + let repeat = read_records(&out.join(format!("{}.tie-repeat.cpsat.jsonl", model.name())))?; + struct One { + notes: u64, + pairs: u64, + verified: Option<[u64; 7]>, + raise: Option, + human_consistent: bool, + wall: (u64, u64), + } + let ones = par_map(&corpus.lines, |line| { + let RepeatVariants { + tie: tie_p, + constrained: rep_p, + scale, + vpn, + pairs, + } = repeat_variants(model, &line.tab)?; + // Lines the solver was not run on (e.g. a holdout-only run) are + // outside the sample, not refusals. + let (Some(a), Some(b)) = (tie.get(&line.id), repeat.get(&line.id)) else { + return None; + }; + let human = &line.tab.human; + let human_consistent = consistent(human, &pairs) == pairs.len() as u64; + let wall = (a.wall_us, b.wall_us); + let (Verdict::Proven { optimum: oa }, Verdict::Proven { optimum: ob }) = + (verify_record(&tie_p, a), verify_record(&rep_p, b)) + else { + return Some(One { + notes: human.len() as u64, + pairs: pairs.len() as u64, + verified: None, + raise: None, + human_consistent, + wall, + }); + }; + let pa = decode_positions(a.witness.as_deref()?, vpn)?; + let pb = decode_positions(b.witness.as_deref()?, vpn)?; + let dp = model.predict(&line.tab).positions; + let agree = |p: &[FretboardPosition]| Agreement::of(human, p).agree; + Some(One { + notes: human.len() as u64, + pairs: pairs.len() as u64, + verified: Some([ + consistent(human, &pairs), + consistent(&dp, &pairs), + consistent(&pa, &pairs), + consistent(&pb, &pairs), + agree(&dp), + agree(&pa), + agree(&pb), + ]), + raise: Some(ob.div_euclid(scale) - oa.div_euclid(scale)), + human_consistent, + wall, + }) + }); + let mut e = RepeatEval::default(); + let mut raises = Vec::new(); + let mut verified_notes = 0_u64; + for one in ones.into_iter().flatten() { + e.lines += 1; + e.notes += one.notes; + e.pairs += one.pairs; + e.human_consistent_lines += usize::from(one.human_consistent); + e.solver_total_s_tie += one.wall.0 as f64 / 1e6; + e.solver_total_s_repeat += one.wall.1 as f64 / 1e6; + let Some(v) = one.verified else { + e.refused_lines += 1; + continue; + }; + e.verified_lines += 1; + verified_notes += one.notes; + e.consistent_pairs_human += v[0]; + e.consistent_pairs_dp += v[1]; + e.consistent_pairs_tie += v[2]; + e.consistent_pairs_repeat += v[3]; + e.agree_dp += v[4]; + e.agree_tie += v[5]; + e.agree_repeat += v[6]; + if let Some(r) = one.raise { + e.lines_cost_raised += usize::from(r > 0); + raises.push(r); + } + } + let rate = |x: u64| x as f64 / verified_notes.max(1) as f64; + e.agree_rate_dp = rate(e.agree_dp); + e.agree_rate_tie = rate(e.agree_tie); + e.agree_rate_repeat = rate(e.agree_repeat); + e.cost_raise = quantiles(raises); + evals.insert(model.name().to_string(), e); + } + + println!("\n| model | lines (verified / refused) | pairs | consistent pairs: human / DP / solver / solver+constraint | agreement: DP / solver / solver+constraint | cost raised (lines, p50 / p90 / max) | solver s (tie / +constraint) |"); + println!("|---|---|---|---|---|---|---|"); + for (name, e) in &evals { + let pct = |x: u64| 100.0 * x as f64 / e.pairs.max(1) as f64; + println!( + "| {name} | {} ({} / {}) | {} | {:.1}% / {:.1}% / {:.1}% / {:.1}% | {:.1}% / {:.1}% / {:.1}% | {} ({} / {} / {}) | {:.0} / {:.0} |", + e.lines, + e.verified_lines, + e.refused_lines, + e.pairs, + pct(e.consistent_pairs_human), + pct(e.consistent_pairs_dp), + pct(e.consistent_pairs_tie), + pct(e.consistent_pairs_repeat), + 100.0 * e.agree_rate_dp, + 100.0 * e.agree_rate_tie, + 100.0 * e.agree_rate_repeat, + e.lines_cost_raised, + e.cost_raise.p50, + e.cost_raise.p90, + e.cost_raise.max, + e.solver_total_s_tie, + e.solver_total_s_repeat + ); + } + write_json(&out.join("repeat-report.json"), &evals) +} + +fn write_json(path: &Path, value: &impl Serialize) -> std::io::Result<()> { + let mut text = serde_json::to_string_pretty(value).map_err(std::io::Error::other)?; + text.push('\n'); + fs::write(path, text)?; + eprintln!("wrote {}", path.display()); + Ok(()) +} + +// ── entry ───────────────────────────────────────────────────────────────────── + +struct Args { + command: String, + tabs: PathBuf, + out: PathBuf, + models: Vec, +} + +fn parse_args() -> Result { + let mut it = std::env::args().skip(1); + let command = it.next().ok_or("missing command (fit | export | report)")?; + let (mut tabs, mut out, mut models) = (None, None, Vec::new()); + while let Some(flag) = it.next() { + let value = it.next().ok_or_else(|| format!("{flag} needs a value"))?; + match flag.as_str() { + "--tabs" => tabs = Some(PathBuf::from(value)), + "--out" => out = Some(PathBuf::from(value)), + "--v1" | "--hand" => models.push(parse_model(&flag, &value)?), + _ => return Err(format!("unknown flag {flag}")), + } + } + if models.is_empty() { + models.push(parse_model("--v1", "v1=1,1,2,1")?); + } + Ok(Args { + command, + tabs: tabs.ok_or("--tabs DIR is required")?, + out: out.ok_or("--out DIR is required")?, + models, + }) +} + +fn run() -> Result<(), String> { + let args = parse_args()?; + fs::create_dir_all(&args.out).map_err(|e| e.to_string())?; + let started = Instant::now(); + let corpus = load(&args.tabs, &LineCut::v1()).map_err(|e| e.to_string())?; + eprintln!( + "corpus: {} files ({} failed), {} guitar tracks, {} + {} lines, {} + {} notes (train + test), {:.1}s", + corpus.facts.files, + corpus.facts.import_failures, + corpus.facts.guitar_tracks, + corpus.facts.lines_train, + corpus.facts.lines_test, + corpus.facts.notes_train, + corpus.facts.notes_test, + started.elapsed().as_secs_f64() + ); + let result = match args.command.as_str() { + "fit" => fit(corpus, &args.out), + "export" => export(&corpus, &args.models, &args.out), + "report" => report(corpus, &args.models, &args.out), + "repeat-export" => repeat_export(&corpus, &args.models, &args.out), + "repeat-report" => repeat_report(&corpus, &args.models, &args.out), + other => return Err(format!("unknown command {other}")), + }; + result.map_err(|e| e.to_string()) +} + +fn main() -> ExitCode { + match run() { + Ok(()) => ExitCode::SUCCESS, + Err(e) => { + eprintln!("fingering_gap: {e}"); + ExitCode::FAILURE + } + } +} diff --git a/lab/src/fingering.rs b/lab/src/fingering.rs new file mode 100644 index 00000000..8177ec74 --- /dev/null +++ b/lab/src/fingering.rs @@ -0,0 +1,1232 @@ +//! Fingering optimality experiments — the first optimization-phase subject. +//! +//! Three pieces, all pure and deterministic: +//! +//! - **Tablature lines** ([`tab_lines`]): monophonic runs of a Guitar Pro +//! track that carry the tab author's own `(string, fret)` choices — the +//! human reference a fingering model is measured against. +//! - **The production objective, mirrored** ([`v1_cost`], [`v1_problem`]): +//! the exact cost `griff_core::fretboard::infer_positions` minimizes, +//! re-implemented independently so an external solver's optimum can be +//! compared with the production DP's path. +//! - **A hand-position model** ([`HandModel`], [`solve_hand`], +//! [`hand_problem`]): a hidden index-finger position with a four-fret box, +//! stretch, shift events and distances, and string distance — the +//! finger-span layer ADR-0019 §7 defers. Experimental: calibration +//! evidence only, no authority over production. + +use std::ops::RangeInclusive; + +use griff_core::event::{FretboardPosition, Pitch, Tuning}; +use griff_core::fretboard::{FingeringWeights, STANDARD_MAX_FRET}; +use griff_core::score::{AtomEvent, AtomNote, Score}; +use serde::{Deserialize, Serialize}; +use thiserror::Error; + +use crate::ir::{fnv1a64, IntVar, VarId}; +use crate::optir::{Hard, OptIrError, OptProblem, Term}; +use crate::problems::LabError; + +/// Variables per note in a [`v1_problem`]: `s{i}` (string), `f{i}` (fret). +pub const V1_VARS_PER_NOTE: usize = 2; +/// Variables per note in a [`hand_problem`]: `s{i}`, `f{i}`, `h{i}` (hand). +pub const HAND_VARS_PER_NOTE: usize = 3; + +/// How a track is cut into tablature lines. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub struct LineCut { + /// Lines shorter than this are dropped (and counted). + pub min_notes: usize, + /// A silence of at least this many quarters between a note's end and the + /// next onset cuts the line; `0` disables rest cuts. + pub max_rest_quarters: u32, + /// Positions above this fret cut the line (and are counted). + pub max_fret: u8, +} + +impl LineCut { + /// The experiment's baseline cut: ≥ 4 notes, a whole-bar-in-4/4 rest + /// cuts, [`STANDARD_MAX_FRET`]. + #[must_use] + pub const fn v1() -> Self { + Self { + min_notes: 4, + max_rest_quarters: 4, + max_fret: STANDARD_MAX_FRET, + } + } +} + +/// Where the notes of a track went when it was cut into lines. +#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Serialize)] +pub struct CutStats { + /// Note atoms read. + pub notes_seen: u64, + /// Onsets carrying more than one note (each cuts the line). + pub chord_onsets: u64, + /// Single notes without a position (each cuts the line). + pub unpositioned: u64, + /// Single notes positioned above `max_fret` (each cuts the line). + pub beyond_max_fret: u64, + /// Single notes whose position does not sound their pitch under the + /// track tuning (each cuts the line). + pub pitch_mismatch: u64, + /// Rests long enough to cut a non-empty line. + pub rest_cuts: u64, + /// Non-empty lines dropped as shorter than `min_notes`. + pub short_lines: u64, + /// Notes inside those dropped lines. + pub short_line_notes: u64, + /// Lines kept. + pub kept_lines: u64, + /// Notes inside kept lines. + pub kept_notes: u64, + /// Tracks whose tuning was strictly ascending (string 1 = lowest, the GP6 + /// import orientation) and was mirrored to string 1 = highest. + pub mirrored_tracks: u64, +} + +impl CutStats { + /// Adds another track's counts into this one. + pub fn absorb(&mut self, other: &Self) { + let Self { + notes_seen, + chord_onsets, + unpositioned, + beyond_max_fret, + pitch_mismatch, + rest_cuts, + short_lines, + short_line_notes, + kept_lines, + kept_notes, + mirrored_tracks, + } = *other; + self.notes_seen = self.notes_seen.saturating_add(notes_seen); + self.chord_onsets = self.chord_onsets.saturating_add(chord_onsets); + self.unpositioned = self.unpositioned.saturating_add(unpositioned); + self.beyond_max_fret = self.beyond_max_fret.saturating_add(beyond_max_fret); + self.pitch_mismatch = self.pitch_mismatch.saturating_add(pitch_mismatch); + self.rest_cuts = self.rest_cuts.saturating_add(rest_cuts); + self.short_lines = self.short_lines.saturating_add(short_lines); + self.short_line_notes = self.short_line_notes.saturating_add(short_line_notes); + self.kept_lines = self.kept_lines.saturating_add(kept_lines); + self.kept_notes = self.kept_notes.saturating_add(kept_notes); + self.mirrored_tracks = self.mirrored_tracks.saturating_add(mirrored_tracks); + } +} + +/// One monophonic tablature line with the tab author's positions. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct TabLine { + /// Track index in the score. + pub track: usize, + /// Voice id within the track. + pub voice: u8, + /// Onset tick of the first note. + pub start_tick: u32, + /// The track tuning. + pub tuning: Tuning, + /// Pitches, in onset order. + pub pitches: Vec, + /// The tab author's positions — one per pitch, each sounding it. + pub human: Vec, +} + +/// Cuts one track into monophonic tablature lines, per voice. +/// +/// A line is a maximal run of single-note onsets whose explicit positions +/// sound their pitch under the track tuning. A chord onset, an unpositioned +/// note, a position above `cut.max_fret`, a pitch/position mismatch, or a +/// long enough rest ends the current line; each cause is counted. +/// +/// Lines always use griff's string orientation (string 1 = highest): a track +/// whose tuning is strictly ascending is mirrored — tuning reversed and every +/// position renumbered — and counted in [`CutStats::mirrored_tracks`]. +/// +/// # Errors +/// +/// [`LabError::NoSuchTrack`] when `track_index` is out of range. +pub fn tab_lines( + score: &Score, + track_index: usize, + cut: &LineCut, +) -> Result<(Vec, CutStats), LabError> { + let track = score + .tracks + .get(track_index) + .ok_or(LabError::NoSuchTrack { index: track_index })?; + let rest_ticks = u64::from(cut.max_rest_quarters) * u64::from(score.ticks_per_quarter); + let mut lines = Vec::new(); + let mut stats = CutStats::default(); + + // Positions are checked against the imported tuning as-is, then emitted + // in griff's orientation (string 1 = highest). + let open = track.tuning.open_strings(); + let mirrored = open.len() >= 2 && open.windows(2).all(|w| matches!(w, [a, b] if a.0 < b.0)); + let tuning = if mirrored { + stats.mirrored_tracks = 1; + Tuning::new(open.iter().rev().copied().collect()) + } else { + track.tuning.clone() + }; + let string_count = u8::try_from(open.len()).unwrap_or(u8::MAX); + let orient = |p: FretboardPosition| { + if mirrored { + FretboardPosition { + string: string_count.saturating_add(1).saturating_sub(p.string), + fret: p.fret, + } + } else { + p + } + }; + + for voice in &track.voices { + let mut notes: Vec<&AtomNote> = voice + .event_groups + .iter() + .flat_map(|g| &g.atoms) + .filter_map(|a| match a { + AtomEvent::Note(n) => Some(n), + AtomEvent::Rest(_) => None, + }) + .collect(); + notes.sort_by_key(|n| n.absolute_start.0); + + let mut line = LineBuilder::new(track_index, voice.id, &tuning); + let mut sounding_until: Option = None; + let mut rest = notes.as_slice(); + while let Some(first) = rest.first() { + let onset = first.absolute_start.0; + let width = rest + .iter() + .position(|n| n.absolute_start.0 != onset) + .unwrap_or(rest.len()); + let (group, tail) = rest.split_at(width); + rest = tail; + stats.notes_seen = stats.notes_seen.saturating_add(count(group.len())); + + let onset_ticks = u64::from(onset); + let rest_cut = cut.max_rest_quarters > 0 + && sounding_until.is_some_and(|end| onset_ticks >= end.saturating_add(rest_ticks)); + let group_end = group + .iter() + .map(|n| onset_ticks.saturating_add(u64::from(n.duration.0))) + .max() + .unwrap_or(onset_ticks); + sounding_until = Some(sounding_until.map_or(group_end, |end| end.max(group_end))); + if rest_cut && !line.is_empty() { + stats.rest_cuts = stats.rest_cuts.saturating_add(1); + line.flush(cut, &mut lines, &mut stats); + } + + let [note] = group else { + stats.chord_onsets = stats.chord_onsets.saturating_add(1); + line.flush(cut, &mut lines, &mut stats); + continue; + }; + let Some(position) = note.position.map(|p| p.position) else { + stats.unpositioned = stats.unpositioned.saturating_add(1); + line.flush(cut, &mut lines, &mut stats); + continue; + }; + if position.fret > cut.max_fret { + stats.beyond_max_fret = stats.beyond_max_fret.saturating_add(1); + line.flush(cut, &mut lines, &mut stats); + continue; + } + if track.tuning.pitch_at(position) != Some(note.pitch) { + stats.pitch_mismatch = stats.pitch_mismatch.saturating_add(1); + line.flush(cut, &mut lines, &mut stats); + continue; + } + line.push(onset, note.pitch, orient(position)); + } + line.flush(cut, &mut lines, &mut stats); + } + Ok((lines, stats)) +} + +/// The production fingering objective (ADR-0019 `v1`), re-implemented +/// independently of `infer_positions`: per note `fret·w.fret − [open]·w.open_string`, +/// per step `|Δfret|·w.position_shift + [string changed]·w.string_change`. +#[must_use] +pub fn v1_cost(line: &[FretboardPosition], weights: &FingeringWeights) -> i64 { + let unary = line + .iter() + .map(|&p| v1_unary(p.fret, weights)) + .fold(0_i64, i64::saturating_add); + let steps = line + .windows(2) + .map(|pair| match pair { + [a, b] => weights + .position_shift + .saturating_mul(i64::from(a.fret.abs_diff(b.fret))) + .saturating_add(if a.string == b.string { + 0 + } else { + weights.string_change + }), + _ => 0, + }) + .fold(0_i64, i64::saturating_add); + unary.saturating_add(steps) +} + +/// The production objective as an [`OptProblem`]: per note `s{i}` and +/// `f{i}` tied by the candidate table, unary fret costs, `AbsDiff` fret +/// travel and `NotEqual` string change between neighbours. Zero-weight terms +/// and zero-cost table entries are omitted. +/// +/// # Errors +/// +/// [`LabError::EmptyLine`] for no pitches; [`LabError::UnpositionablePitch`] +/// when a pitch has no candidate at or below `max_fret`. +pub fn v1_problem( + pitches: &[Pitch], + tuning: &Tuning, + weights: &FingeringWeights, + max_fret: u8, +) -> Result { + if pitches.is_empty() { + return Err(LabError::EmptyLine); + } + let mut vars = Vec::with_capacity(pitches.len().saturating_mul(V1_VARS_PER_NOTE)); + let mut hard = Vec::with_capacity(pitches.len()); + let mut objective = Vec::new(); + for (index, &pitch) in pitches.iter().enumerate() { + let candidates = candidates_or_refuse(index, pitch, tuning, max_fret)?; + let (s, f) = push_position_vars(&mut vars, &mut hard, index, &candidates); + let costs: Vec<(i64, i64)> = distinct_frets(&candidates) + .into_iter() + .map(|fret| (i64::from(fret), v1_unary(fret, weights))) + .filter(|&(_, cost)| cost != 0) + .collect(); + if !costs.is_empty() { + objective.push(Term::Unary { var: f, costs }); + } + if index > 0 { + let (prev_s, prev_f) = (VarId(s.0 - V1_VARS_PER_NOTE), VarId(f.0 - V1_VARS_PER_NOTE)); + if weights.position_shift != 0 { + objective.push(Term::AbsDiff { + a: prev_f, + b: f, + weight: weights.position_shift, + }); + } + if weights.string_change != 0 { + objective.push(Term::NotEqual { + a: prev_s, + b: s, + weight: weights.string_change, + }); + } + } + } + Ok(build("fingering-v1", vars, hard, objective)) +} + +/// Encodes positions as a [`v1_problem`] witness (`s0, f0, s1, f1, …`). +#[must_use] +pub fn encode_v1_witness(line: &[FretboardPosition]) -> Vec { + line.iter() + .flat_map(|p| [i64::from(p.string), i64::from(p.fret)]) + .collect() +} + +/// Encodes positions and hands as a [`hand_problem`] witness +/// (`s0, f0, h0, s1, …`); `None` when the lengths differ. +#[must_use] +pub fn encode_hand_witness(line: &[FretboardPosition], hands: &[u8]) -> Option> { + if line.len() != hands.len() { + return None; + } + Some( + line.iter() + .zip(hands) + .flat_map(|(p, &h)| [i64::from(p.string), i64::from(p.fret), i64::from(h)]) + .collect(), + ) +} + +/// Decodes the per-note positions of a witness laid out with +/// `vars_per_note` variables per note, string then fret first; `None` for a +/// ragged length or out-of-range values. +#[must_use] +pub fn decode_positions(witness: &[i64], vars_per_note: usize) -> Option> { + if vars_per_note < 2 || !witness.len().is_multiple_of(vars_per_note) { + return None; + } + witness + .chunks(vars_per_note) + .map(|chunk| match chunk { + [string, fret, ..] => Some(FretboardPosition { + string: u8::try_from(*string).ok()?, + fret: u8::try_from(*fret).ok()?, + }), + _ => None, + }) + .collect() +} + +/// Weights of the hand-position model. Transition weights and `stretch` are +/// non-negative; `height` and `open_string` may be negative (a preference +/// for high positions, a bonus for open strings). +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub struct HandWeights { + /// Per fret of hand height above the first position, per note. + pub height: i64, + /// Per open-string note. + pub open_string: i64, + /// Per note played one fret outside the four-fret box. + pub stretch: i64, + /// Per hand shift (the position changes at all). + pub shift: i64, + /// Per fret of hand travel. + pub shift_distance: i64, + /// Per string crossed between consecutive notes. + pub string_distance: i64, +} + +/// How a fret is reached from a hand position. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Reach { + /// An open string — reachable from any hand position. + Open, + /// Inside the four-fret box `[hand, hand + 3]`. + InBox, + /// One fret outside the box: `hand − 1` (≥ 1) or `hand + 4`. + Stretch, +} + +/// Typed refusals for a hand model. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Error)] +pub enum HandModelError { + /// A weight that must be non-negative is negative. + #[error("weight {name} must be non-negative, got {value}")] + NegativeWeight { + /// The weight's field name. + name: &'static str, + /// Its value. + value: i64, + }, + /// The neck is too short for a four-fret box. + #[error("max_fret {max_fret} leaves no room for a four-fret box")] + NoRoom { + /// The refused fret range. + max_fret: u8, + }, +} + +/// A validated hand-position model over frets `0..=max_fret`; hand +/// positions are `1..=max_fret − 3`, so the box stays on the neck. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct HandModel { + weights: HandWeights, + max_fret: u8, +} + +impl HandModel { + /// Frets covered by the hand without a stretch. + pub const BOX_FRETS: u8 = 4; + + /// Validates the weights and the neck range. + /// + /// # Errors + /// + /// [`HandModelError::NegativeWeight`] for a negative `stretch`, `shift`, + /// `shift_distance`, or `string_distance`; [`HandModelError::NoRoom`] + /// when `max_fret < 4`. + pub fn new(weights: HandWeights, max_fret: u8) -> Result { + for (name, value) in [ + ("stretch", weights.stretch), + ("shift", weights.shift), + ("shift_distance", weights.shift_distance), + ("string_distance", weights.string_distance), + ] { + if value < 0 { + return Err(HandModelError::NegativeWeight { name, value }); + } + } + if max_fret < Self::BOX_FRETS { + return Err(HandModelError::NoRoom { max_fret }); + } + Ok(Self { weights, max_fret }) + } + + /// The weights. + #[must_use] + pub const fn weights(&self) -> HandWeights { + self.weights + } + + /// The highest fret. + #[must_use] + pub const fn max_fret(&self) -> u8 { + self.max_fret + } + + /// Admissible hand positions, ascending. + #[must_use] + pub fn hands(&self) -> RangeInclusive { + 1..=self.max_fret.saturating_sub(Self::BOX_FRETS - 1) + } + + /// How `fret` is reached from `hand`; `None` when it is not reachable + /// (or `hand` is not an admissible position). + #[must_use] + pub fn reach(&self, fret: u8, hand: u8) -> Option { + if !self.hands().contains(&hand) || fret > self.max_fret { + return None; + } + if fret == 0 { + return Some(Reach::Open); + } + let top = hand.saturating_add(Self::BOX_FRETS - 1); + if (hand..=top).contains(&fret) { + Some(Reach::InBox) + } else if fret == top.saturating_add(1) || fret.saturating_add(1) == hand { + Some(Reach::Stretch) + } else { + None + } + } +} + +/// Why a `(positions, hands)` pair cannot be scored. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Error)] +pub enum HandError { + /// Positions and hands differ in length. + #[error("{positions} positions but {hands} hands")] + Length { + /// Positions supplied. + positions: usize, + /// Hands supplied. + hands: usize, + }, + /// A note is not reachable from its hand position. + #[error("note {index} is not reachable from its hand position")] + Unreachable { + /// Index of the note. + index: usize, + }, +} + +/// Scores a complete `(positions, hands)` realization under the model: +/// per note `height·(hand − 1) + [open]·open_string + [stretch]·stretch`, +/// per step `[hand changed]·shift + |Δhand|·shift_distance + |Δstring|·string_distance`. +/// +/// # Errors +/// +/// See [`HandError`]. +pub fn hand_cost( + line: &[FretboardPosition], + hands: &[u8], + model: &HandModel, +) -> Result { + if line.len() != hands.len() { + return Err(HandError::Length { + positions: line.len(), + hands: hands.len(), + }); + } + let mut total = 0_i64; + for (index, (p, &hand)) in line.iter().zip(hands).enumerate() { + let unary = hand_unary(model, p.fret, hand).ok_or(HandError::Unreachable { index })?; + total = total.saturating_add(unary); + } + for (pair, hand_pair) in line.windows(2).zip(hands.windows(2)) { + if let ([a, b], [ha, hb]) = (pair, hand_pair) { + total = total.saturating_add(hand_transition(&model.weights, *a, *ha, *b, *hb)); + } + } + Ok(total) +} + +/// The cheapest hand sequence for **fixed** positions (e.g. a human tab): +/// the model's score of that fingering. `None` when some position is +/// unreachable from every hand position. +#[must_use] +pub fn best_hands(line: &[FretboardPosition], model: &HandModel) -> Option<(i64, Vec)> { + let hands: Vec = model.hands().collect(); + let mut layers: Vec>> = Vec::with_capacity(line.len()); + for (index, p) in line.iter().enumerate() { + let layer: Vec> = hands + .iter() + .map(|&h| { + let unary = hand_unary(model, p.fret, h)?; + let Some(prev_layer) = index.checked_sub(1).and_then(|i| layers.get(i)) else { + return Some((unary, usize::MAX)); + }; + let prev = line.get(index - 1).copied()?; + let mut best: Scored = None; + for (j, cell) in prev_layer.iter().enumerate() { + let (Some((cost, _)), Some(&ph)) = (cell, hands.get(j)) else { + continue; + }; + let total = cost + .saturating_add(hand_transition(&model.weights, prev, ph, *p, h)) + .saturating_add(unary); + if best.is_none_or(|(b, _)| total < b) { + best = Some((total, j)); + } + } + best + }) + .collect(); + if layer.iter().all(Option::is_none) { + return None; + } + layers.push(layer); + } + let Some(last) = layers.last() else { + return Some((0, Vec::new())); + }; + let mut best: Scored = None; + for (j, cell) in last.iter().enumerate() { + if let Some((cost, _)) = cell { + if best.is_none_or(|(b, _)| *cost < b) { + best = Some((*cost, j)); + } + } + } + let (cost, mut j) = best?; + let mut out = vec![0_u8; line.len()]; + for (layer, slot) in layers.iter().zip(out.iter_mut()).rev() { + let (_, parent) = (*layer.get(j)?)?; + *slot = *hands.get(j)?; + j = parent; + } + Some((cost, out)) +} + +/// An optimal realization under a [`HandModel`]. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct HandSolution { + /// The optimal cost. + pub cost: i64, + /// One position per pitch. + pub positions: Vec, + /// One hand position per pitch. + pub hands: Vec, +} + +/// Exact joint DP over `(candidate, hand)` states — the in-repo reference +/// optimum of the hand model. Deterministic. `None` when some pitch has no +/// candidate at or below the model's `max_fret`; an empty line costs `0`. +#[must_use] +pub fn solve_hand(pitches: &[Pitch], tuning: &Tuning, model: &HandModel) -> Option { + let hands: Vec = model.hands().collect(); + let weights = model.weights; + let mut layers: Vec = Vec::with_capacity(pitches.len()); + for &pitch in pitches { + let candidates = tuning.candidates(pitch, model.max_fret); + if candidates.is_empty() { + return None; + } + let unary: Vec>> = candidates + .iter() + .map(|c| { + hands + .iter() + .map(|&h| hand_unary(model, c.fret, h)) + .collect() + }) + .collect(); + let cells = match layers.last() { + None => unary + .iter() + .map(|row| row.iter().map(|u| u.map(|u| (u, (0, 0)))).collect()) + .collect(), + Some(prev) => hand_step(prev, &candidates, &unary, &hands, &weights), + }; + let layer = HandLayer { candidates, cells }; + if layer.cells.iter().flatten().all(Option::is_none) { + return None; + } + layers.push(layer); + } + + let Some(last) = layers.last() else { + return Some(HandSolution { + cost: 0, + positions: Vec::new(), + hands: Vec::new(), + }); + }; + let mut best: Scored<(usize, usize)> = None; + for (ci, row) in last.cells.iter().enumerate() { + for (hi, cell) in row.iter().enumerate() { + if let Some((cost, _)) = cell { + if best.is_none_or(|(b, _)| *cost < b) { + best = Some((*cost, (ci, hi))); + } + } + } + } + let (cost, (mut ci, mut hi)) = best?; + let mut positions = vec![FretboardPosition { string: 0, fret: 0 }; layers.len()]; + let mut chosen = vec![0_u8; layers.len()]; + for ((layer, position), hand) in layers + .iter() + .zip(positions.iter_mut()) + .zip(chosen.iter_mut()) + .rev() + { + let (_, parent) = (*layer.cells.get(ci)?.get(hi)?)?; + *position = *layer.candidates.get(ci)?; + *hand = *hands.get(hi)?; + (ci, hi) = parent; + } + Some(HandSolution { + cost, + positions, + hands: chosen, + }) +} + +/// The hand model as an [`OptProblem`]: per note `s{i}`, `f{i}`, `h{i}`; +/// the candidate table ties string to fret, a reach table ties fret to hand; +/// unary height and open-string costs, a fret×hand stretch table, and +/// `NotEqual` / `AbsDiff` hand shifts plus `AbsDiff` string distance between +/// neighbours. Zero-weight terms and zero-cost entries are omitted. +/// +/// # Errors +/// +/// [`LabError::EmptyLine`] for no pitches; [`LabError::UnpositionablePitch`] +/// when a pitch has no candidate at or below the model's `max_fret`. +pub fn hand_problem( + pitches: &[Pitch], + tuning: &Tuning, + model: &HandModel, +) -> Result { + if pitches.is_empty() { + return Err(LabError::EmptyLine); + } + let hands: Vec = model.hands().collect(); + let weights = model.weights; + let mut vars = Vec::with_capacity(pitches.len().saturating_mul(HAND_VARS_PER_NOTE)); + let mut hard = Vec::with_capacity(pitches.len().saturating_mul(2)); + let mut objective = Vec::new(); + for (index, &pitch) in pitches.iter().enumerate() { + let candidates = candidates_or_refuse(index, pitch, tuning, model.max_fret)?; + let (s, f) = push_position_vars(&mut vars, &mut hard, index, &candidates); + let h = VarId(vars.len()); + vars.push(IntVar::new( + format!("h{index}"), + hands.iter().map(|&x| i64::from(x)).collect(), + )); + let frets = distinct_frets(&candidates); + let mut reach_tuples = Vec::new(); + let mut stretch_costs = Vec::new(); + for &fret in &frets { + for &hand in &hands { + match model.reach(fret, hand) { + None => {} + Some(reach) => { + reach_tuples.push((i64::from(fret), i64::from(hand))); + if reach == Reach::Stretch && weights.stretch != 0 { + stretch_costs.push((i64::from(fret), i64::from(hand), weights.stretch)); + } + } + } + } + } + hard.push(Hard::Allowed { + a: f, + b: h, + tuples: reach_tuples, + }); + if weights.height != 0 { + objective.push(Term::Unary { + var: h, + costs: hands + .iter() + .map(|&x| { + ( + i64::from(x), + weights.height.saturating_mul(i64::from(x) - 1), + ) + }) + .filter(|&(_, cost)| cost != 0) + .collect(), + }); + } + if weights.open_string != 0 && frets.contains(&0) { + objective.push(Term::Unary { + var: f, + costs: vec![(0, weights.open_string)], + }); + } + if !stretch_costs.is_empty() { + objective.push(Term::Pair { + a: f, + b: h, + costs: stretch_costs, + }); + } + if index > 0 { + let (prev_s, prev_h) = ( + VarId(s.0 - HAND_VARS_PER_NOTE), + VarId(h.0 - HAND_VARS_PER_NOTE), + ); + if weights.shift != 0 { + objective.push(Term::NotEqual { + a: prev_h, + b: h, + weight: weights.shift, + }); + } + if weights.shift_distance != 0 { + objective.push(Term::AbsDiff { + a: prev_h, + b: h, + weight: weights.shift_distance, + }); + } + if weights.string_distance != 0 { + objective.push(Term::AbsDiff { + a: prev_s, + b: s, + weight: weights.string_distance, + }); + } + } + } + Ok(build("fingering-hand", vars, hard, objective)) +} + +/// A song identity for holdout splits: the file stem, lowercased, with +/// trailing parenthesized groups (e.g. `(ver 2 by …)`) and the extension +/// removed, so arrangements of one song share a key. +#[must_use] +pub fn song_key(file_name: &str) -> String { + let name = file_name.rsplit(['/', '\\']).next().unwrap_or(file_name); + let stem = match name.rfind('.') { + Some(dot) if dot > 0 && !name[dot..].contains(' ') => &name[..dot], + _ => name, + }; + let mut key = stem.trim(); + while key.ends_with(')') { + match key.rfind('(') { + Some(open) => key = key[..open].trim_end(), + None => break, + } + } + key.to_lowercase() +} + +/// A deterministic holdout bucket in `0..buckets` for a [`song_key`] +/// (FNV-1a 64 modulo `buckets`); `0` when `buckets` is `0`. +#[must_use] +pub fn holdout_bucket(key: &str, buckets: u64) -> u64 { + if buckets == 0 { + return 0; + } + fnv1a64(key.as_bytes()) % buckets +} + +/// Repeated figures inside one line: start indices `(i, j)` with +/// `i + window <= j` of identical pitch windows, scanning left to right — +/// for each start `i` the first later non-overlapping occurrence `j`, after +/// which the scan resumes at `i + window`. Single-pitch windows (ostinato on +/// one note) are skipped: they carry no fingering shape. Empty for +/// `window == 0`. +#[must_use] +pub fn repeat_pairs(pitches: &[Pitch], window: usize) -> Vec<(usize, usize)> { + let n = pitches.len(); + let mut pairs = Vec::new(); + if window == 0 { + return pairs; + } + let mut i = 0; + while i + 2 * window <= n { + let Some(figure) = pitches.get(i..i + window) else { + break; + }; + if figure.windows(2).all(|w| matches!(w, [a, b] if a == b)) { + i += 1; + continue; + } + let next = (i + window..=n - window).find(|&j| pitches.get(j..j + window) == Some(figure)); + match next { + Some(j) => { + pairs.push((i, j)); + i += window; + } + None => i += 1, + } + } + pairs +} + +/// Adds the **repeat-consistency** global constraint to a fingering problem +/// laid out with `vars_per_note` variables per note (string first): for each +/// pair from [`repeat_pairs`] and each offset `k < window`, notes `i + k` and +/// `j + k` must use the same string. Not expressible in a chain DP's local +/// state; expressed in the IR as equal-value hard tables. +/// +/// # Errors +/// +/// [`OptIrError`] when a pair indexes past the problem (dangling variable) or +/// two aligned notes share no string. +pub fn with_repeat_consistency( + problem: &OptProblem, + vars_per_note: usize, + pairs: &[(usize, usize)], + window: usize, +) -> Result { + let vars = problem.vars(); + let mut hard = problem.hard().to_vec(); + for &(i, j) in pairs { + for k in 0..window { + let (a, b) = ((i + k) * vars_per_note, (j + k) * vars_per_note); + let tuples = match (vars.get(a), vars.get(b)) { + (Some(x), Some(y)) => x + .domain + .iter() + .filter(|v| y.domain.binary_search(v).is_ok()) + .map(|&v| (v, v)) + .collect(), + // Let validation name the dangling id. + _ => vec![(0, 0)], + }; + hard.push(Hard::Allowed { + a: VarId(a), + b: VarId(b), + tuples, + }); + } + } + OptProblem::try_new( + problem.name(), + vars.to_vec(), + hard, + problem.objective().to_vec(), + ) +} + +/// A deterministic tie-break for comparing solver witnesses: every objective +/// weight is multiplied by `scale = notes · max_string + 1` and each note's +/// string value is added, so `evaluate' = scale · evaluate + Σ string` — the +/// cost-optimal set is unchanged and ties resolve toward lower string numbers. +/// Returns the new problem and `scale`. +/// +/// # Errors +/// +/// [`OptIrError`] if the rebuilt problem is refused. +pub fn with_string_tiebreak( + problem: &OptProblem, + vars_per_note: usize, +) -> Result<(OptProblem, i64), OptIrError> { + let vars = problem.vars(); + let step = vars_per_note.max(1); + let strings: Vec = (0..vars.len()).step_by(step).map(VarId).collect(); + let max_string = strings + .iter() + .filter_map(|id| vars.get(id.0)) + .filter_map(|v| v.domain.last().copied()) + .max() + .unwrap_or(0); + let notes = i64::try_from(strings.len()).unwrap_or(i64::MAX); + let scale = notes.saturating_mul(max_string).saturating_add(1); + let mut objective: Vec = problem + .objective() + .iter() + .map(|term| match term { + Term::Unary { var, costs } => Term::Unary { + var: *var, + costs: costs + .iter() + .map(|&(v, c)| (v, c.saturating_mul(scale))) + .collect(), + }, + Term::Pair { a, b, costs } => Term::Pair { + a: *a, + b: *b, + costs: costs + .iter() + .map(|&(x, y, c)| (x, y, c.saturating_mul(scale))) + .collect(), + }, + Term::AbsDiff { a, b, weight } => Term::AbsDiff { + a: *a, + b: *b, + weight: weight.saturating_mul(scale), + }, + Term::NotEqual { a, b, weight } => Term::NotEqual { + a: *a, + b: *b, + weight: weight.saturating_mul(scale), + }, + }) + .collect(); + for id in strings { + if let Some(var) = vars.get(id.0) { + objective.push(Term::Unary { + var: id, + costs: var.domain.iter().map(|&v| (v, v)).collect(), + }); + } + } + let rebuilt = OptProblem::try_new( + problem.name(), + vars.to_vec(), + problem.hard().to_vec(), + objective, + )?; + Ok((rebuilt, scale)) +} + +// ── private helpers ─────────────────────────────────────────────────────────── + +/// Accumulates one tablature line while a voice is scanned. +struct LineBuilder<'a> { + track: usize, + voice: u8, + tuning: &'a Tuning, + start_tick: u32, + pitches: Vec, + human: Vec, +} + +impl<'a> LineBuilder<'a> { + const fn new(track: usize, voice: u8, tuning: &'a Tuning) -> Self { + Self { + track, + voice, + tuning, + start_tick: 0, + pitches: Vec::new(), + human: Vec::new(), + } + } + + fn is_empty(&self) -> bool { + self.pitches.is_empty() + } + + fn push(&mut self, onset: u32, pitch: Pitch, position: FretboardPosition) { + if self.pitches.is_empty() { + self.start_tick = onset; + } + self.pitches.push(pitch); + self.human.push(position); + } + + /// Ends the current line: kept when long enough, otherwise counted as + /// dropped. An empty line is a no-op. + fn flush(&mut self, cut: &LineCut, lines: &mut Vec, stats: &mut CutStats) { + let len = self.pitches.len(); + if len == 0 { + return; + } + let pitches = std::mem::take(&mut self.pitches); + let human = std::mem::take(&mut self.human); + if len < cut.min_notes { + stats.short_lines = stats.short_lines.saturating_add(1); + stats.short_line_notes = stats.short_line_notes.saturating_add(count(len)); + return; + } + stats.kept_lines = stats.kept_lines.saturating_add(1); + stats.kept_notes = stats.kept_notes.saturating_add(count(len)); + lines.push(TabLine { + track: self.track, + voice: self.voice, + start_tick: self.start_tick, + tuning: self.tuning.clone(), + pitches, + human, + }); + } +} + +fn count(n: usize) -> u64 { + u64::try_from(n).unwrap_or(u64::MAX) +} + +/// The `v1` per-note cost (mirrors production `candidate_cost`). +fn v1_unary(fret: u8, weights: &FingeringWeights) -> i64 { + let base = weights.fret.saturating_mul(i64::from(fret)); + if fret == 0 { + base.saturating_sub(weights.open_string) + } else { + base + } +} + +fn candidates_or_refuse( + index: usize, + pitch: Pitch, + tuning: &Tuning, + max_fret: u8, +) -> Result, LabError> { + let candidates = tuning.candidates(pitch, max_fret); + if candidates.is_empty() { + return Err(LabError::UnpositionablePitch { + index, + pitch: pitch.0, + }); + } + Ok(candidates) +} + +/// Declares `s{index}` and `f{index}` and the candidate table tying them. +fn push_position_vars( + vars: &mut Vec, + hard: &mut Vec, + index: usize, + candidates: &[FretboardPosition], +) -> (VarId, VarId) { + let s = VarId(vars.len()); + vars.push(IntVar::new( + format!("s{index}"), + candidates.iter().map(|c| i64::from(c.string)).collect(), + )); + let f = VarId(vars.len()); + vars.push(IntVar::new( + format!("f{index}"), + candidates.iter().map(|c| i64::from(c.fret)).collect(), + )); + hard.push(Hard::Allowed { + a: s, + b: f, + tuples: candidates + .iter() + .map(|c| (i64::from(c.string), i64::from(c.fret))) + .collect(), + }); + (s, f) +} + +fn distinct_frets(candidates: &[FretboardPosition]) -> Vec { + let mut frets: Vec = candidates.iter().map(|c| c.fret).collect(); + frets.sort_unstable(); + frets.dedup(); + frets +} + +/// Builds an IR problem the builders above make valid by construction: +/// unique safe names, validated ids, non-empty domains and tables, and +/// duplicate-free cost tables. +#[allow(clippy::panic)] // documented invariant, exercised by the contract suite +fn build(name: &str, vars: Vec, hard: Vec, objective: Vec) -> OptProblem { + match OptProblem::try_new(name, vars, hard, objective) { + Ok(problem) => problem, + Err(e) => panic!("fingering problem builder produced invalid IR: {e}"), + } +} + +/// Per-note hand-model cost, or `None` when unreachable. +fn hand_unary(model: &HandModel, fret: u8, hand: u8) -> Option { + let reach = model.reach(fret, hand)?; + let w = model.weights; + let mut cost = w.height.saturating_mul(i64::from(hand) - 1); + match reach { + Reach::Open => cost = cost.saturating_add(w.open_string), + Reach::Stretch => cost = cost.saturating_add(w.stretch), + Reach::InBox => {} + } + Some(cost) +} + +fn hand_shift(w: &HandWeights, from: u8, to: u8) -> i64 { + if from == to { + 0 + } else { + w.shift.saturating_add( + w.shift_distance + .saturating_mul(i64::from(from.abs_diff(to))), + ) + } +} + +fn hand_transition( + w: &HandWeights, + a: FretboardPosition, + ha: u8, + b: FretboardPosition, + hb: u8, +) -> i64 { + hand_shift(w, ha, hb).saturating_add( + w.string_distance + .saturating_mul(i64::from(a.string.abs_diff(b.string))), + ) +} + +/// A DP cell: the best cost reaching a state and its parent, or `None` when +/// the state is unreachable. +type Scored

= Option<(i64, P)>; + +/// Per candidate, per hand: a [`solve_hand`] layer's cells. +type HandCells = Vec>>; + +/// One [`solve_hand`] layer transition, factored: the string term depends +/// only on the candidates and the hand term only on the hands, so +/// `min over (c, h) of D[c][h] + σ|s_c − s_c'| + τ(h, h')` equals +/// `min over h of (min over c of D[c][h] + σ|s_c − s_c'|) + τ(h, h')` — +/// `O(K²·H + K·H²)` instead of `O(K²·H²)` per step. Ties keep the lowest +/// candidate, then the lowest hand. +fn hand_step( + prev: &HandLayer, + candidates: &[FretboardPosition], + unary: &[Vec>], + hands: &[u8], + weights: &HandWeights, +) -> HandCells { + candidates + .iter() + .zip(unary) + .map(|(next, row)| { + let via_string: Vec> = (0..hands.len()) + .map(|hi| { + let mut best: Scored = None; + for (ci, (cand, prev_row)) in + prev.candidates.iter().zip(&prev.cells).enumerate() + { + let Some(Some((cost, _))) = prev_row.get(hi) else { + continue; + }; + let total = cost.saturating_add( + weights + .string_distance + .saturating_mul(i64::from(cand.string.abs_diff(next.string))), + ); + if best.is_none_or(|(b, _)| total < b) { + best = Some((total, ci)); + } + } + best + }) + .collect(); + row.iter() + .enumerate() + .map(|(hj, u)| { + let u = (*u)?; + let to = *hands.get(hj)?; + let mut best: Scored<(usize, usize)> = None; + for (hi, cell) in via_string.iter().enumerate() { + let (Some((cost, ci)), Some(&from)) = (cell, hands.get(hi)) else { + continue; + }; + let total = cost + .saturating_add(hand_shift(weights, from, to)) + .saturating_add(u); + if best.is_none_or(|(b, _)| total < b) { + best = Some((total, (*ci, hi))); + } + } + best + }) + .collect() + }) + .collect() +} + +/// One DP layer of [`solve_hand`]: per candidate, per hand, the best cost and +/// its parent `(candidate, hand)` in the previous layer. +struct HandLayer { + candidates: Vec, + cells: HandCells, +} diff --git a/lab/src/ir.rs b/lab/src/ir.rs index 032e2291..85e1d44b 100644 --- a/lab/src/ir.rs +++ b/lab/src/ir.rs @@ -248,7 +248,7 @@ impl OracleProblem { } /// FNV-1a 64-bit. -fn fnv1a64(bytes: &[u8]) -> u64 { +pub(crate) fn fnv1a64(bytes: &[u8]) -> u64 { const OFFSET: u64 = 0xcbf2_9ce4_8422_2325; const PRIME: u64 = 0x0000_0100_0000_01b3; bytes @@ -257,7 +257,7 @@ fn fnv1a64(bytes: &[u8]) -> u64 { } /// `[A-Za-z_][A-Za-z0-9_]*` — safe as a `MiniZinc` identifier. -fn minizinc_safe(name: &str) -> bool { +pub(crate) fn minizinc_safe(name: &str) -> bool { let mut chars = name.chars(); let Some(first) = chars.next() else { return false; diff --git a/lab/src/lib.rs b/lab/src/lib.rs index 607c0667..72eb86eb 100644 --- a/lab/src/lib.rs +++ b/lab/src/lib.rs @@ -8,12 +8,18 @@ //! - **Problem B** — complement pair cleanliness (the existing //! `PairValidation` rule set, pinned to production semantics). //! +//! The optimization phase ([`optir`], [`fingering`]) adds an objective to +//! the IR and measures the production fingering DP and a hand-position model +//! against an external optimum and against human tablature. +//! //! Shape: typed problem → solver-neutral IR → `MiniZinc` emission + an exact //! in-repo reference solver → archived manifests. Research tooling only: //! nothing here is a production dependency, and no production path calls it. pub mod emit; +pub mod fingering; pub mod ir; pub mod manifest; +pub mod optir; pub mod problems; pub mod solve; diff --git a/lab/src/optir.rs b/lab/src/optir.rs new file mode 100644 index 00000000..c2a931c5 --- /dev/null +++ b/lab/src/optir.rs @@ -0,0 +1,564 @@ +//! Solver-neutral **optimization** IR — the Constraint Lab's second phase. +//! +//! The SAT/UNSAT IR ([`crate::ir`]) answers "does an admissible realization +//! exist?". This IR adds an objective: finite integer variables, binary hard +//! tables, and an integer-weighted sum of cost terms, so an external solver +//! can answer "what does the *best* admissible realization cost?". +//! +//! Authority stays in-repo: every witness — from any solver — is re-scored by +//! [`OptProblem::evaluate`], and [`verify_record`] accepts an optimality claim +//! only when the solver proved it, the witness is admissible, and the +//! re-scored objective equals the claimed one. Research tooling only: nothing +//! here is a production dependency. + +use serde::{Deserialize, Serialize}; +use thiserror::Error; + +use crate::ir::{fnv1a64, minizinc_safe, IntVar, IrError, VarId}; +use crate::manifest::SolverIdentity; + +/// Wire schema identity of an exported optimization problem. +pub const OPT_SCHEMA: &str = "griff.constraint-lab-opt"; +/// Wire schema version of an exported optimization problem. +pub const OPT_SCHEMA_VERSION: u32 = 1; + +/// A hard (admissibility) constraint. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +#[serde(tag = "kind", rename_all = "snake_case")] +pub enum Hard { + /// `(a, b)` must equal one of `tuples` (canonical: sorted, deduplicated). + Allowed { + /// First variable. + a: VarId, + /// Second variable. + b: VarId, + /// The admissible value pairs. + tuples: Vec<(i64, i64)>, + }, +} + +/// One integer-weighted objective term; the objective is their sum. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +#[serde(tag = "kind", rename_all = "snake_case")] +pub enum Term { + /// `cost(var)` from a table; a value absent from the table costs `0`. + Unary { + /// The scored variable. + var: VarId, + /// `(value, cost)` entries (canonical: sorted by value, unique keys). + costs: Vec<(i64, i64)>, + }, + /// `cost(a, b)` from a table; an absent pair costs `0`. + Pair { + /// First variable. + a: VarId, + /// Second variable. + b: VarId, + /// `(value_a, value_b, cost)` entries (canonical: sorted, unique keys). + costs: Vec<(i64, i64, i64)>, + }, + /// `weight · |a − b|`. + AbsDiff { + /// First variable. + a: VarId, + /// Second variable. + b: VarId, + /// Integer weight. + weight: i64, + }, + /// `weight · [a ≠ b]`. + NotEqual { + /// First variable. + a: VarId, + /// Second variable. + b: VarId, + /// Integer weight. + weight: i64, + }, +} + +/// Typed refusals at problem construction. +#[derive(Debug, Clone, PartialEq, Eq, Error)] +pub enum OptIrError { + /// A shared IR invariant (domains, names, variable ids) is violated. + #[error(transparent)] + Ir(#[from] IrError), + /// A cost table maps one key to two costs — ambiguous, refused. + #[error("cost table of objective term {term} repeats a key")] + DuplicateCostKey { + /// Index of the offending term. + term: usize, + }, + /// A hard table admits nothing — an unconditional UNSAT is refused at + /// construction rather than smuggled to a solver. + #[error("hard constraint {index} admits no tuple")] + EmptyAllowedTable { + /// Index of the offending hard constraint. + index: usize, + }, +} + +/// Why a witness is not an admissible, scorable assignment. +#[derive(Debug, Clone, PartialEq, Eq, Error)] +pub enum WitnessError { + /// Wrong number of values. + #[error("witness has {got} values, the problem has {expected} variables")] + Length { + /// Variables in the problem. + expected: usize, + /// Values in the witness. + got: usize, + }, + /// A value lies outside its variable's domain. + #[error("value {value} of \"{name}\" lies outside its domain")] + OutOfDomain { + /// The variable name. + name: String, + /// The offending value. + value: i64, + }, + /// A hard constraint is violated. + #[error("hard constraint {index} is violated")] + HardViolated { + /// Index of the violated hard constraint. + index: usize, + }, + /// The objective does not fit `i64`. + #[error("the objective overflows i64")] + Overflow, +} + +/// A complete optimization problem: named, finite, canonical, **opaque** — +/// construction validates every invariant and canonicalizes every table, so +/// equal problems have equal fingerprints. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +pub struct OptProblem { + name: String, + vars: Vec, + hard: Vec, + objective: Vec, +} + +impl OptProblem { + /// Builds a problem after validating every invariant and canonicalizing + /// every table (sorted; hard tables deduplicated). + /// + /// # Errors + /// + /// [`OptIrError::Ir`] for dangling variable ids, empty domains, duplicate + /// or MiniZinc-unsafe names; [`OptIrError::DuplicateCostKey`] for an + /// ambiguous cost table; [`OptIrError::EmptyAllowedTable`] for a hard + /// table that admits nothing. + pub fn try_new( + name: impl Into, + vars: Vec, + hard: Vec, + objective: Vec, + ) -> Result { + let mut vars = vars; + for var in &mut vars { + // IntVar fields are public: re-canonicalize so evaluation can + // binary-search every domain. + var.domain.sort_unstable(); + var.domain.dedup(); + if var.domain.is_empty() { + return Err(IrError::EmptyDomain { + name: var.name.clone(), + } + .into()); + } + if !minizinc_safe(&var.name) { + return Err(IrError::UnsafeName { + name: var.name.clone(), + } + .into()); + } + } + for (i, var) in vars.iter().enumerate() { + if vars.iter().skip(i + 1).any(|other| other.name == var.name) { + return Err(IrError::DuplicateName { + name: var.name.clone(), + } + .into()); + } + } + let count = vars.len(); + let check = |id: VarId| -> Result<(), IrError> { + if id.0 >= count { + return Err(IrError::DanglingVarId { + id: id.0, + vars: count, + }); + } + Ok(()) + }; + + let mut hard = hard; + for (index, constraint) in hard.iter_mut().enumerate() { + match constraint { + Hard::Allowed { a, b, tuples } => { + check(*a)?; + check(*b)?; + tuples.sort_unstable(); + tuples.dedup(); + if tuples.is_empty() { + return Err(OptIrError::EmptyAllowedTable { index }); + } + } + } + } + + let mut objective = objective; + for (index, term) in objective.iter_mut().enumerate() { + let duplicate = match term { + Term::Unary { var, costs } => { + check(*var)?; + costs.sort_unstable(); + costs.windows(2).any(|w| matches!(w, [x, y] if x.0 == y.0)) + } + Term::Pair { a, b, costs } => { + check(*a)?; + check(*b)?; + costs.sort_unstable(); + costs + .windows(2) + .any(|w| matches!(w, [x, y] if (x.0, x.1) == (y.0, y.1))) + } + Term::AbsDiff { a, b, .. } | Term::NotEqual { a, b, .. } => { + check(*a)?; + check(*b)?; + false + } + }; + if duplicate { + return Err(OptIrError::DuplicateCostKey { term: index }); + } + } + + Ok(Self { + name: name.into(), + vars, + hard, + objective, + }) + } + + /// Problem name. + #[must_use] + pub fn name(&self) -> &str { + &self.name + } + + /// Variables, in declaration order. + #[must_use] + pub fn vars(&self) -> &[IntVar] { + &self.vars + } + + /// Hard constraints. + #[must_use] + pub fn hard(&self) -> &[Hard] { + &self.hard + } + + /// Objective terms. + #[must_use] + pub fn objective(&self) -> &[Term] { + &self.objective + } + + /// FNV-1a 64 over the canonical serialization — the same within-context + /// identity discipline as [`crate::ir::OracleProblem::fingerprint`]. + #[must_use] + pub fn fingerprint(&self) -> u64 { + let canonical = + serde_json::to_string(self).unwrap_or_else(|_| format!("unserializable:{}", self.name)); + fnv1a64(canonical.as_bytes()) + } + + /// Re-scores a complete assignment: full length, every value inside its + /// domain, every hard constraint satisfied, then the exact objective. + /// + /// # Errors + /// + /// See [`WitnessError`]. + pub fn evaluate(&self, witness: &[i64]) -> Result { + if witness.len() != self.vars.len() { + return Err(WitnessError::Length { + expected: self.vars.len(), + got: witness.len(), + }); + } + for (var, &value) in self.vars.iter().zip(witness) { + if var.domain.binary_search(&value).is_err() { + return Err(WitnessError::OutOfDomain { + name: var.name.clone(), + value, + }); + } + } + // Ids are validated at construction, so every lookup below succeeds. + let value = |id: &VarId| witness.get(id.0).copied().unwrap_or_default(); + for (index, constraint) in self.hard.iter().enumerate() { + match constraint { + Hard::Allowed { a, b, tuples } => { + if tuples.binary_search(&(value(a), value(b))).is_err() { + return Err(WitnessError::HardViolated { index }); + } + } + } + } + let mut total: i128 = 0; + for term in &self.objective { + let cost: i128 = match term { + Term::Unary { var, costs } => { + let x = value(var); + costs + .binary_search_by_key(&x, |&(v, _)| v) + .ok() + .and_then(|i| costs.get(i)) + .map_or(0, |&(_, c)| i128::from(c)) + } + Term::Pair { a, b, costs } => { + let key = (value(a), value(b)); + costs + .binary_search_by_key(&key, |&(u, v, _)| (u, v)) + .ok() + .and_then(|i| costs.get(i)) + .map_or(0, |&(_, _, c)| i128::from(c)) + } + Term::AbsDiff { a, b, weight } => { + let diff = (i128::from(value(a)) - i128::from(value(b))).abs(); + i128::from(*weight) + .checked_mul(diff) + .ok_or(WitnessError::Overflow)? + } + Term::NotEqual { a, b, weight } => { + if value(a) == value(b) { + 0 + } else { + i128::from(*weight) + } + } + }; + total = total.checked_add(cost).ok_or(WitnessError::Overflow)?; + } + i64::try_from(total).map_err(|_| WitnessError::Overflow) + } +} + +/// One exported problem on the wire (one JSON line), consumed by external +/// solver adapters. +#[derive(Debug, Clone, Serialize)] +pub struct ProblemRecord { + /// Schema identity: [`OPT_SCHEMA`]. + pub schema: &'static str, + /// Schema version: [`OPT_SCHEMA_VERSION`]. + pub version: u32, + /// Caller-assigned identity, unique within one export. + pub id: String, + /// The problem fingerprint, zero-padded hex. + pub fingerprint_hex: String, + /// The problem. + pub problem: OptProblem, + /// Optional reference values for the agreement pass: among optimal + /// assignments, maximize how many of these `(variable, value)` pairs hold. + /// Never part of the objective. + pub reference: Vec<(VarId, i64)>, +} + +impl ProblemRecord { + /// Wraps a problem with its identity and fingerprint. + #[must_use] + pub fn new(id: impl Into, problem: OptProblem, reference: Vec<(VarId, i64)>) -> Self { + Self { + schema: OPT_SCHEMA, + version: OPT_SCHEMA_VERSION, + id: id.into(), + fingerprint_hex: format!("{:016x}", problem.fingerprint()), + problem, + reference, + } + } +} + +/// A solver's status for one solve, on the wire. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum SolveStatus { + /// Optimum proven. + Optimal, + /// A feasible assignment without an optimality proof. + Feasible, + /// Proven to admit no assignment. + Infeasible, + /// No conclusion (limit reached). + Unknown, + /// The solver rejected the model. + ModelInvalid, +} + +/// The lexicographic agreement pass: among assignments at the proven +/// optimum, the maximum number of reference pairs that can hold. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct AgreementRecord { + /// Status of the agreement maximization. + pub status: SolveStatus, + /// Claimed number of matched reference pairs. + pub matched: Option, + /// The witness achieving it. + pub witness: Option>, +} + +/// One solver result on the wire (one JSON line). +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct SolveRecord { + /// The problem id it answers. + pub id: String, + /// The fingerprint the solver read. + pub fingerprint_hex: String, + /// Solver identity. + pub solver: SolverIdentity, + /// Solve status. + pub status: SolveStatus, + /// Claimed objective of the witness. + pub objective: Option, + /// Best proven lower bound. + pub bound: Option, + /// The witness, one value per variable. + pub witness: Option>, + /// Wall time in microseconds. + pub wall_us: u64, + /// Optional agreement pass. + pub agreement: Option, +} + +/// The in-repo judgement of a [`SolveRecord`]. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Verdict { + /// Optimality proven by the solver, witness admissible, objective + /// re-scored exactly. + Proven { + /// The verified optimum. + optimum: i64, + }, + /// The record answers a different problem. + FingerprintMismatch, + /// The solver did not prove optimality. + NotProven { + /// The reported status. + status: SolveStatus, + }, + /// The solver claims optimality but supplied no witness or objective. + MissingWitness, + /// The witness is not admissible. + WitnessInvalid(WitnessError), + /// The claimed objective differs from the re-scored one, or the proven + /// bound differs from the objective. + ObjectiveMismatch { + /// Solver-claimed objective. + claimed: i64, + /// In-repo re-scored objective. + rescored: i64, + /// Solver-claimed bound. + bound: Option, + }, +} + +/// Judges a solver record against the problem it claims to answer. +#[must_use] +pub fn verify_record(problem: &OptProblem, record: &SolveRecord) -> Verdict { + if record.fingerprint_hex != format!("{:016x}", problem.fingerprint()) { + return Verdict::FingerprintMismatch; + } + if record.status != SolveStatus::Optimal { + return Verdict::NotProven { + status: record.status, + }; + } + let (Some(witness), Some(claimed)) = (&record.witness, record.objective) else { + return Verdict::MissingWitness; + }; + let rescored = match problem.evaluate(witness) { + Ok(cost) => cost, + Err(e) => return Verdict::WitnessInvalid(e), + }; + if rescored != claimed || record.bound.is_some_and(|bound| bound != claimed) { + return Verdict::ObjectiveMismatch { + claimed, + rescored, + bound: record.bound, + }; + } + Verdict::Proven { optimum: rescored } +} + +/// Why an agreement-pass claim is refused. +#[derive(Debug, Clone, PartialEq, Eq, Error)] +pub enum AgreementError { + /// The pass was not solved to optimality. + #[error("agreement pass not proven: {status:?}")] + NotProven { + /// Reported status. + status: SolveStatus, + }, + /// No witness or count supplied. + #[error("agreement pass has no witness or count")] + MissingWitness, + /// The witness is not admissible. + #[error("agreement witness invalid: {0}")] + WitnessInvalid(WitnessError), + /// The witness does not sit at the proven optimum. + #[error("agreement witness costs {rescored}, optimum is {optimum}")] + OffOptimum { + /// Verified optimum. + optimum: i64, + /// Re-scored cost of the agreement witness. + rescored: i64, + }, + /// The claimed match count differs from the recount. + #[error("agreement claims {claimed} matches, recount is {recounted}")] + CountMismatch { + /// Claimed matches. + claimed: u64, + /// In-repo recount. + recounted: u64, + }, +} + +/// Verifies an agreement pass against a verified optimum and the reference +/// pairs; returns the recounted number of matches. +/// +/// # Errors +/// +/// See [`AgreementError`]. +pub fn verify_agreement( + problem: &OptProblem, + reference: &[(VarId, i64)], + optimum: i64, + record: &AgreementRecord, +) -> Result { + if record.status != SolveStatus::Optimal { + return Err(AgreementError::NotProven { + status: record.status, + }); + } + let (Some(witness), Some(claimed)) = (&record.witness, record.matched) else { + return Err(AgreementError::MissingWitness); + }; + let rescored = problem + .evaluate(witness) + .map_err(AgreementError::WitnessInvalid)?; + if rescored != optimum { + return Err(AgreementError::OffOptimum { optimum, rescored }); + } + let recounted = reference + .iter() + .filter(|(var, value)| witness.get(var.0) == Some(value)) + .count(); + let recounted = u64::try_from(recounted).unwrap_or(u64::MAX); + if recounted != claimed { + return Err(AgreementError::CountMismatch { claimed, recounted }); + } + Ok(recounted) +} diff --git a/lab/tests/fingering.rs b/lab/tests/fingering.rs new file mode 100644 index 00000000..5004bbb3 --- /dev/null +++ b/lab/tests/fingering.rs @@ -0,0 +1,941 @@ +//! Red → contract tests for the fingering optimality experiment (`fingering`). +//! +//! Pins: how a Guitar Pro track becomes human-fingered tablature lines (and +//! where every refused note is counted); that the mirrored `v1` objective is +//! the one the production DP minimizes; that the `v1` and hand-model IR +//! encodings score exactly like the domain evaluators; and that the in-repo +//! hand DP is optimal — all against brute force on exhaustive small families. + +#![allow( + clippy::expect_used, + clippy::unwrap_used, + clippy::panic, + clippy::missing_assert_message, + clippy::indexing_slicing, + clippy::arithmetic_side_effects, + clippy::cast_possible_truncation, + clippy::cast_possible_wrap, + clippy::cast_sign_loss, + clippy::type_complexity +)] + +use griff_constraint_lab::{ + fingering::{ + best_hands, decode_positions, encode_hand_witness, encode_v1_witness, hand_cost, + hand_problem, holdout_bucket, repeat_pairs, solve_hand, song_key, tab_lines, v1_cost, + v1_problem, with_repeat_consistency, with_string_tiebreak, CutStats, HandError, HandModel, + HandModelError, HandWeights, LineCut, Reach, HAND_VARS_PER_NOTE, V1_VARS_PER_NOTE, + }, + optir::{OptIrError, Term, WitnessError}, + problems::LabError, +}; +use griff_core::{ + event::{ + FretboardPosition, NoteMarks, NotePosition, Pitch, Tempo, Ticks, TimeSignature, Tuning, + Velocity, + }, + fretboard::{infer_positions, FingeringWeights, STANDARD_MAX_FRET}, + score::{ + AtomEvent, AtomNote, EventGroup, EventGroupKind, LossReport, MasterBar, RepeatMarker, + Score, Track, Voice, + }, + slice::TickRange, +}; + +const Q: u32 = 480; + +fn pitch(p: u8) -> Pitch { + Pitch::new(p).expect("valid pitch") +} + +fn pos(string: u8, fret: u8) -> FretboardPosition { + FretboardPosition { string, fret } +} + +fn note(onset: u32, p: u8, position: Option<(u8, u8)>) -> AtomEvent { + AtomEvent::Note(AtomNote { + absolute_start: Ticks(onset), + duration: Ticks(Q), + pitch: pitch(p), + velocity: Velocity::new(90).expect("velocity"), + marks: NoteMarks::empty(), + position: position.map(|(s, f)| NotePosition::explicit(pos(s, f))), + }) +} + +fn group(atoms: Vec) -> EventGroup { + EventGroup { + kind: if atoms.len() > 1 { + EventGroupKind::Chord + } else { + EventGroupKind::Single + }, + atoms, + technique_spans: Vec::new(), + } +} + +fn score(voices: Vec>) -> Score { + score_with_tuning(voices, Tuning::standard_e()) +} + +fn score_with_tuning(voices: Vec>, tuning: Tuning) -> Score { + Score { + ticks_per_quarter: 480, + master_bars: vec![MasterBar { + index: 0, + tick_range: TickRange::new(Ticks(0), Ticks(64 * Q)).expect("ordered"), + time_signature: TimeSignature { + numerator: 4, + denominator: 4, + }, + tempo: Tempo::from_bpm_integer(120).expect("tempo"), + repeat: RepeatMarker::default(), + }], + tracks: vec![Track { + name: Some("Guitar".into()), + channel: 0, + voices: voices + .into_iter() + .enumerate() + .map(|(i, event_groups)| Voice { + id: i as u8, + event_groups, + }) + .collect(), + tuning, + }], + source_meta: None, + loss: LossReport::new(), + } +} + +fn single(onset: u32, p: u8, position: Option<(u8, u8)>) -> EventGroup { + group(vec![note(onset, p, position)]) +} + +// ── tablature lines ─────────────────────────────────────────────────────────── + +/// Voice 0 exercises every cut cause once; voice 1 is one clean line sharing +/// voice 0's onsets (chords are per voice, not per track). +fn cut_fixture() -> Score { + let voice0 = vec![ + single(0, 40, Some((6, 0))), + single(Q, 45, Some((5, 0))), + single(2 * Q, 47, Some((5, 2))), + single(3 * Q, 50, Some((4, 0))), + group(vec![ + note(4 * Q, 52, Some((4, 2))), + note(4 * Q, 55, Some((3, 0))), + ]), + single(5 * Q, 57, Some((3, 2))), + single(6 * Q, 59, Some((2, 0))), + single(7 * Q, 60, None), + single(8 * Q, 62, Some((2, 3))), + single(9 * Q, 64, Some((1, 0))), + single(10 * Q, 65, Some((1, 1))), + single(11 * Q, 67, Some((1, 3))), + // 4-quarter rest after the note ending at 12Q. + single(16 * Q, 89, Some((1, 25))), + single(17 * Q, 60, Some((2, 0))), + single(18 * Q, 64, Some((2, 5))), + single(19 * Q, 66, Some((2, 7))), + single(20 * Q, 67, Some((2, 8))), + single(21 * Q, 69, Some((2, 10))), + ]; + let voice1 = vec![ + single(0, 52, Some((5, 7))), + single(Q, 55, Some((5, 10))), + single(2 * Q, 57, Some((4, 7))), + single(3 * Q, 59, Some((4, 9))), + ]; + score(vec![voice0, voice1]) +} + +#[test] +fn tab_lines_cut_at_every_cause_and_count_it() { + let (lines, stats) = tab_lines(&cut_fixture(), 0, &LineCut::v1()).expect("track 0"); + let summary: Vec<(u8, u32, Vec)> = lines + .iter() + .map(|l| { + ( + l.voice, + l.start_tick, + l.pitches.iter().map(|p| p.0).collect(), + ) + }) + .collect(); + assert_eq!( + summary, + vec![ + (0, 0, vec![40, 45, 47, 50]), + (0, 8 * Q, vec![62, 64, 65, 67]), + (0, 18 * Q, vec![64, 66, 67, 69]), + (1, 0, vec![52, 55, 57, 59]), + ] + ); + assert_eq!( + lines[1].human, + vec![pos(2, 3), pos(1, 0), pos(1, 1), pos(1, 3)] + ); + assert!(lines + .iter() + .all(|l| l.track == 0 && l.tuning == Tuning::standard_e())); + assert!(lines.iter().all(|l| l.human.len() == l.pitches.len())); + assert_eq!( + stats, + CutStats { + notes_seen: 23, + chord_onsets: 1, + unpositioned: 1, + beyond_max_fret: 1, + pitch_mismatch: 1, + rest_cuts: 1, + short_lines: 1, + short_line_notes: 2, + kept_lines: 4, + kept_notes: 16, + mirrored_tracks: 0, + } + ); +} + +#[test] +fn rest_cut_threshold_is_inclusive_and_can_be_disabled() { + let line = |gap_onset: u32| { + score(vec![vec![ + single(0, 40, Some((6, 0))), + single(Q, 45, Some((5, 0))), + single(gap_onset, 50, Some((4, 0))), + single(gap_onset + Q, 55, Some((3, 0))), + ]]) + }; + let cut = LineCut { + min_notes: 2, + max_rest_quarters: 4, + max_fret: STANDARD_MAX_FRET, + }; + // The second note ends at 2Q; a rest of exactly 4Q cuts, one tick less does not. + let (lines, stats) = tab_lines(&line(6 * Q), 0, &cut).unwrap(); + assert_eq!((lines.len(), stats.rest_cuts), (2, 1)); + let (lines, stats) = tab_lines(&line(6 * Q - 1), 0, &cut).unwrap(); + assert_eq!((lines.len(), stats.rest_cuts), (1, 0)); + let no_rests = LineCut { + max_rest_quarters: 0, + ..cut + }; + let (lines, _) = tab_lines(&line(40 * Q), 0, &no_rests).unwrap(); + assert_eq!(lines.len(), 1); +} + +#[test] +fn tab_lines_sort_onsets_within_a_voice() { + let s = score(vec![vec![ + single(2 * Q, 47, Some((5, 2))), + single(0, 40, Some((6, 0))), + single(3 * Q, 50, Some((4, 0))), + single(Q, 45, Some((5, 0))), + ]]); + let (lines, _) = tab_lines(&s, 0, &LineCut::v1()).unwrap(); + assert_eq!( + lines[0].pitches, + vec![pitch(40), pitch(45), pitch(47), pitch(50)] + ); +} + +/// GP6 imports number strings low-first (string 1 = lowest); lines come out +/// in griff's orientation (string 1 = highest), pitches untouched. +#[test] +fn tab_lines_mirror_low_first_tunings() { + let low_first = Tuning::new(pitches_of(&[40, 45, 50, 55, 59, 64])); + let s = score_with_tuning( + vec![vec![ + single(0, 40, Some((1, 0))), + single(Q, 45, Some((1, 5))), + single(2 * Q, 59, Some((5, 0))), + single(3 * Q, 64, Some((6, 0))), + ]], + low_first, + ); + let (lines, stats) = tab_lines(&s, 0, &LineCut::v1()).unwrap(); + assert_eq!(stats.mirrored_tracks, 1); + assert_eq!(lines[0].tuning, Tuning::standard_e()); + assert_eq!( + lines[0].human, + vec![pos(6, 0), pos(6, 5), pos(2, 0), pos(1, 0)] + ); + for (p, q) in lines[0].human.iter().zip(&lines[0].pitches) { + assert_eq!(lines[0].tuning.pitch_at(*p), Some(*q)); + } +} + +#[test] +fn tab_lines_keep_non_monotonic_tunings_as_they_are() { + // Descending except one crossed pair: not a mirrored tuning, left alone. + let odd = Tuning::new(pitches_of(&[64, 59, 55, 57, 45, 40])); + let s = score_with_tuning( + vec![vec![ + single(0, 40, Some((6, 0))), + single(Q, 57, Some((4, 0))), + single(2 * Q, 59, Some((2, 0))), + single(3 * Q, 64, Some((1, 0))), + ]], + odd.clone(), + ); + let (lines, stats) = tab_lines(&s, 0, &LineCut::v1()).unwrap(); + assert_eq!(stats.mirrored_tracks, 0); + assert_eq!(lines[0].tuning, odd); + assert_eq!(lines[0].human[1], pos(4, 0)); +} + +#[test] +fn tab_lines_refuse_a_missing_track() { + assert_eq!( + tab_lines(&cut_fixture(), 1, &LineCut::v1()), + Err(LabError::NoSuchTrack { index: 1 }) + ); +} + +#[test] +fn cut_stats_absorb_adds_fieldwise() { + let (_, a) = tab_lines(&cut_fixture(), 0, &LineCut::v1()).unwrap(); + let mut total = CutStats::default(); + total.absorb(&a); + total.absorb(&a); + assert_eq!(total.notes_seen, 2 * a.notes_seen); + assert_eq!(total.kept_notes, 2 * a.kept_notes); + assert_eq!(total.rest_cuts, 2 * a.rest_cuts); + assert_eq!(total.short_line_notes, 2 * a.short_line_notes); + let (_, mirrored) = tab_lines( + &score_with_tuning(vec![vec![]], Tuning::new(pitches_of(&[40, 45, 50]))), + 0, + &LineCut::v1(), + ) + .unwrap(); + total.absorb(&mirrored); + total.absorb(&mirrored); + assert_eq!(total.mirrored_tracks, 2); +} + +// ── brute force helpers ─────────────────────────────────────────────────────── + +fn candidate_lines( + pitches: &[Pitch], + tuning: &Tuning, + max_fret: u8, +) -> Vec> { + let mut out = vec![Vec::new()]; + for &p in pitches { + let cands = tuning.candidates(p, max_fret); + out = out + .into_iter() + .flat_map(|prefix| { + cands.iter().map(move |&c| { + let mut next = prefix.clone(); + next.push(c); + next + }) + }) + .collect(); + } + out +} + +fn sequences(alphabet: &[u8], len: usize) -> Vec> { + let mut out = vec![Vec::new()]; + for _ in 0..len { + out = out + .into_iter() + .flat_map(|prefix| { + alphabet.iter().map(move |&a| { + let mut next = prefix.clone(); + next.push(a); + next + }) + }) + .collect(); + } + out +} + +fn pitches_of(raw: &[u8]) -> Vec { + raw.iter().map(|&p| pitch(p)).collect() +} + +/// Deterministic pseudo-random lines (xorshift) over the guitar range. +fn lcg_lines(count: usize, len: usize, lo: u8, hi: u8) -> Vec> { + let mut state: u64 = 0x9e37_79b9_7f4a_7c15; + let span = u64::from(hi - lo + 1); + (0..count) + .map(|_| { + (0..len) + .map(|_| { + state ^= state << 13; + state ^= state >> 7; + state ^= state << 17; + pitch(lo + (state % span) as u8) + }) + .collect() + }) + .collect() +} + +const V1_PITCHES: [u8; 8] = [40, 45, 47, 52, 55, 59, 64, 71]; + +fn v1_weight_sets() -> Vec { + vec![ + FingeringWeights::v1(), + FingeringWeights { + fret: 0, + open_string: 0, + position_shift: 0, + string_change: 0, + }, + FingeringWeights { + fret: 0, + open_string: 3, + position_shift: 1, + string_change: 4, + }, + FingeringWeights { + fret: 2, + open_string: -2, + position_shift: 5, + string_change: 0, + }, + ] +} + +// ── v1 objective ────────────────────────────────────────────────────────────── + +#[test] +fn v1_cost_scores_a_hand_computed_line() { + // unary: (0 − 1) + 2 + 5 = 6; steps: (2·2 + 1) + (3·2 + 0) = 11. + let line = [pos(6, 0), pos(5, 2), pos(5, 5)]; + assert_eq!(v1_cost(&line, &FingeringWeights::v1()), 17); + assert_eq!(v1_cost(&[], &FingeringWeights::v1()), 0); +} + +/// The production DP's path is `v1_cost`-optimal: the mirrored objective is +/// the one `infer_positions` minimizes. +#[test] +fn production_dp_path_is_v1_optimal_on_exhaustive_small_lines() { + let tuning = Tuning::standard_e(); + for weights in v1_weight_sets() { + for len in 1..=3 { + for raw in sequences(&V1_PITCHES, len) { + let pitches = pitches_of(&raw); + let dp: Vec = + infer_positions(&pitches, &tuning, &weights, STANDARD_MAX_FRET) + .into_iter() + .map(Option::unwrap) + .collect(); + let brute = candidate_lines(&pitches, &tuning, STANDARD_MAX_FRET) + .iter() + .map(|l| v1_cost(l, &weights)) + .min() + .unwrap(); + assert_eq!(v1_cost(&dp, &weights), brute, "{raw:?} {weights:?}"); + } + } + } +} + +#[test] +fn production_dp_path_is_v1_optimal_on_longer_lines() { + let tuning = Tuning::standard_e(); + for weights in v1_weight_sets() { + for pitches in lcg_lines(24, 6, 40, 76) { + let dp: Vec = + infer_positions(&pitches, &tuning, &weights, STANDARD_MAX_FRET) + .into_iter() + .map(Option::unwrap) + .collect(); + let brute = candidate_lines(&pitches, &tuning, STANDARD_MAX_FRET) + .iter() + .map(|l| v1_cost(l, &weights)) + .min() + .unwrap(); + assert_eq!(v1_cost(&dp, &weights), brute); + } + } +} + +#[test] +fn v1_problem_scores_every_candidate_line_like_v1_cost() { + let tuning = Tuning::standard_e(); + for weights in v1_weight_sets() { + for raw in sequences(&V1_PITCHES, 3) { + let pitches = pitches_of(&raw); + let problem = v1_problem(&pitches, &tuning, &weights, STANDARD_MAX_FRET).unwrap(); + assert_eq!(problem.vars().len(), V1_VARS_PER_NOTE * pitches.len()); + for line in candidate_lines(&pitches, &tuning, STANDARD_MAX_FRET) { + assert_eq!( + problem.evaluate(&encode_v1_witness(&line)), + Ok(v1_cost(&line, &weights)) + ); + } + } + } +} + +#[test] +fn v1_problem_admits_only_candidate_positions() { + let tuning = Tuning::standard_e(); + let pitches = pitches_of(&[40, 45]); + let problem = v1_problem( + &pitches, + &tuning, + &FingeringWeights::v1(), + STANDARD_MAX_FRET, + ) + .unwrap(); + let names: Vec<&str> = problem.vars().iter().map(|v| v.name.as_str()).collect(); + assert_eq!(names, ["s0", "f0", "s1", "f1"]); + // E2 has one candidate (6, 0); A2 has (6, 5) and (5, 0). + assert_eq!(problem.vars()[0].domain, vec![6]); + assert_eq!(problem.vars()[3].domain, vec![0, 5]); + // (5, 5) is in both domains but does not sound A2. + assert_eq!( + problem.evaluate(&[6, 0, 5, 5]), + Err(WitnessError::HardViolated { index: 1 }) + ); +} + +#[test] +fn v1_problem_omits_zero_weight_terms() { + let tuning = Tuning::standard_e(); + let pitches = pitches_of(&[40, 45, 47]); + let weights = FingeringWeights { + fret: 1, + open_string: 0, + position_shift: 0, + string_change: 3, + }; + let problem = v1_problem(&pitches, &tuning, &weights, STANDARD_MAX_FRET).unwrap(); + let abs = problem + .objective() + .iter() + .filter(|t| matches!(t, Term::AbsDiff { .. })) + .count(); + let neq = problem + .objective() + .iter() + .filter(|t| matches!(t, Term::NotEqual { .. })) + .count(); + assert_eq!((abs, neq), (0, 2)); + for term in problem.objective() { + if let Term::Unary { costs, .. } = term { + assert!(costs.iter().all(|&(_, c)| c != 0)); + } + } +} + +#[test] +fn v1_problem_refuses_empty_and_unpositionable_lines() { + let tuning = Tuning::standard_e(); + let w = FingeringWeights::v1(); + assert_eq!( + v1_problem(&[], &tuning, &w, STANDARD_MAX_FRET), + Err(LabError::EmptyLine) + ); + assert_eq!( + v1_problem(&pitches_of(&[40, 30]), &tuning, &w, STANDARD_MAX_FRET), + Err(LabError::UnpositionablePitch { + index: 1, + pitch: 30 + }) + ); +} + +#[test] +fn witness_encoding_round_trips() { + let line = vec![pos(6, 0), pos(5, 12), pos(1, 24)]; + assert_eq!(encode_v1_witness(&line), vec![6, 0, 5, 12, 1, 24]); + assert_eq!( + decode_positions(&encode_v1_witness(&line), V1_VARS_PER_NOTE), + Some(line.clone()) + ); + let hands = vec![1, 12, 21]; + let hw = encode_hand_witness(&line, &hands).unwrap(); + assert_eq!(hw, vec![6, 0, 1, 5, 12, 12, 1, 24, 21]); + assert_eq!( + decode_positions(&hw, HAND_VARS_PER_NOTE), + Some(line.clone()) + ); + assert_eq!(encode_hand_witness(&line, &hands[..2]), None); + assert_eq!(decode_positions(&[6, 0, 5], V1_VARS_PER_NOTE), None); + assert_eq!(decode_positions(&[6, -1], V1_VARS_PER_NOTE), None); + assert_eq!(decode_positions(&[256, 0], V1_VARS_PER_NOTE), None); + assert_eq!(decode_positions(&[6, 0], 0), None); +} + +// ── hand model ──────────────────────────────────────────────────────────────── + +fn hand_weight_sets() -> Vec { + vec![ + HandWeights { + height: 1, + open_string: 2, + stretch: 3, + shift: 5, + shift_distance: 1, + string_distance: 2, + }, + HandWeights { + height: -1, + open_string: -4, + stretch: 0, + shift: 0, + shift_distance: 2, + string_distance: 0, + }, + HandWeights { + height: 0, + open_string: 0, + stretch: 0, + shift: 0, + shift_distance: 0, + string_distance: 0, + }, + HandWeights { + height: 0, + open_string: 0, + stretch: 7, + shift: 3, + shift_distance: 0, + string_distance: 1, + }, + ] +} + +fn model(weights: HandWeights, max_fret: u8) -> HandModel { + HandModel::new(weights, max_fret).expect("valid model") +} + +#[test] +fn hand_model_refuses_negative_transition_and_stretch_weights() { + let base = hand_weight_sets()[0]; + for (name, weights) in [ + ( + "stretch", + HandWeights { + stretch: -1, + ..base + }, + ), + ("shift", HandWeights { shift: -1, ..base }), + ( + "shift_distance", + HandWeights { + shift_distance: -1, + ..base + }, + ), + ( + "string_distance", + HandWeights { + string_distance: -1, + ..base + }, + ), + ] { + assert_eq!( + HandModel::new(weights, 24), + Err(HandModelError::NegativeWeight { name, value: -1 }) + ); + } + assert!(HandModel::new(hand_weight_sets()[1], 24).is_ok()); + assert_eq!( + HandModel::new(base, 3), + Err(HandModelError::NoRoom { max_fret: 3 }) + ); + assert_eq!(model(base, 4).hands(), 1..=1); + assert_eq!(model(base, 24).hands(), 1..=21); +} + +#[test] +fn reach_follows_the_four_fret_box() { + let m = model(hand_weight_sets()[0], 24); + assert_eq!(m.reach(0, 9), Some(Reach::Open)); + assert_eq!(m.reach(5, 5), Some(Reach::InBox)); + assert_eq!(m.reach(8, 5), Some(Reach::InBox)); + assert_eq!(m.reach(9, 5), Some(Reach::Stretch)); + assert_eq!(m.reach(4, 5), Some(Reach::Stretch)); + assert_eq!(m.reach(3, 5), None); + assert_eq!(m.reach(10, 5), None); + assert_eq!(m.reach(1, 2), Some(Reach::Stretch)); + assert_eq!(m.reach(24, 21), Some(Reach::InBox)); + assert_eq!(m.reach(0, 22), None); + assert_eq!(m.reach(0, 0), None); +} + +#[test] +fn hand_cost_scores_a_hand_computed_realization() { + let m = model(hand_weight_sets()[0], 24); + let line = [pos(6, 3), pos(6, 7), pos(5, 0), pos(4, 12)]; + // unary: 2 + 3 + (3 + 2) + 9 = 19; steps: 6 + 2 + 13 = 21. + assert_eq!(hand_cost(&line, &[3, 4, 4, 10], &m), Ok(40)); + // A stretch: fret 7 from hand 3 costs stretch 3 on top of height 2. + assert_eq!(hand_cost(&[pos(6, 7)], &[3], &m), Ok(5)); + assert_eq!( + hand_cost(&line, &[3, 1, 4, 10], &m), + Err(HandError::Unreachable { index: 1 }) + ); + assert_eq!( + hand_cost(&line, &[3, 4], &m), + Err(HandError::Length { + positions: 4, + hands: 2 + }) + ); +} + +fn brute_best_hands(line: &[FretboardPosition], m: &HandModel) -> Option { + let hands: Vec = m.hands().collect(); + sequences(&hands, line.len()) + .iter() + .filter_map(|hs| hand_cost(line, hs, m).ok()) + .min() +} + +#[test] +fn best_hands_is_optimal_for_fixed_positions() { + let tuning = Tuning::standard_e(); + for weights in hand_weight_sets() { + let m = model(weights, 7); + for raw in sequences(&[40, 45, 47, 50, 52, 57, 59, 64], 3) { + for line in candidate_lines(&pitches_of(&raw), &tuning, 7) { + let got = best_hands(&line, &m); + assert_eq!(got.as_ref().map(|g| g.0), brute_best_hands(&line, &m)); + if let Some((cost, hands)) = got { + assert_eq!(hand_cost(&line, &hands, &m), Ok(cost)); + } + } + } + } +} + +#[test] +fn solve_hand_is_optimal_on_exhaustive_small_lines() { + let tuning = Tuning::standard_e(); + for weights in hand_weight_sets() { + let m = model(weights, 7); + for len in 1..=3 { + for raw in sequences(&[40, 45, 47, 50, 52, 57, 59, 64], len) { + let pitches = pitches_of(&raw); + let brute = candidate_lines(&pitches, &tuning, 7) + .iter() + .filter_map(|l| brute_best_hands(l, &m)) + .min(); + let sol = solve_hand(&pitches, &tuning, &m); + assert_eq!(sol.as_ref().map(|s| s.cost), brute, "{raw:?} {weights:?}"); + let sol = sol.unwrap(); + for (p, q) in sol.positions.iter().zip(&pitches) { + assert_eq!(tuning.pitch_at(*p), Some(*q)); + } + assert_eq!(hand_cost(&sol.positions, &sol.hands, &m), Ok(sol.cost)); + } + } + } +} + +#[test] +fn solve_hand_is_optimal_on_longer_full_neck_lines() { + let tuning = Tuning::standard_e(); + for weights in hand_weight_sets() { + let m = model(weights, STANDARD_MAX_FRET); + for pitches in lcg_lines(12, 5, 40, 80) { + let brute = candidate_lines(&pitches, &tuning, STANDARD_MAX_FRET) + .iter() + .filter_map(|l| best_hands(l, &m).map(|b| b.0)) + .min(); + let sol = solve_hand(&pitches, &tuning, &m).unwrap(); + assert_eq!(Some(sol.cost), brute); + assert_eq!(hand_cost(&sol.positions, &sol.hands, &m), Ok(sol.cost)); + assert_eq!(solve_hand(&pitches, &tuning, &m), Some(sol)); + } + } +} + +#[test] +fn solve_hand_edges() { + let m = model(hand_weight_sets()[0], STANDARD_MAX_FRET); + let tuning = Tuning::standard_e(); + let empty = solve_hand(&[], &tuning, &m).unwrap(); + assert_eq!((empty.cost, empty.positions.len()), (0, 0)); + assert_eq!(solve_hand(&pitches_of(&[40, 30]), &tuning, &m), None); +} + +#[test] +fn hand_problem_scores_like_hand_cost_and_shares_the_optimum() { + let tuning = Tuning::standard_e(); + for weights in hand_weight_sets() { + let m = model(weights, 7); + let hands: Vec = m.hands().collect(); + for raw in sequences(&[40, 47, 52, 57, 64], 2) { + let pitches = pitches_of(&raw); + let problem = hand_problem(&pitches, &tuning, &m).unwrap(); + assert_eq!(problem.vars().len(), HAND_VARS_PER_NOTE * pitches.len()); + assert_eq!(problem.vars()[2].name, "h0"); + assert_eq!(problem.vars()[2].domain, vec![1, 2, 3, 4]); + let mut best: Option = None; + for line in candidate_lines(&pitches, &tuning, 7) { + for hs in sequences(&hands, line.len()) { + let witness = encode_hand_witness(&line, &hs).unwrap(); + match hand_cost(&line, &hs, &m) { + Ok(cost) => { + assert_eq!(problem.evaluate(&witness), Ok(cost)); + best = Some(best.map_or(cost, |b: i64| b.min(cost))); + } + Err(_) => assert!(matches!( + problem.evaluate(&witness), + Err(WitnessError::HardViolated { .. }) + )), + } + } + } + assert_eq!(best, solve_hand(&pitches, &tuning, &m).map(|s| s.cost)); + } + } +} + +#[test] +fn hand_problem_omits_zero_weight_terms_and_refuses_bad_lines() { + let tuning = Tuning::standard_e(); + let zeros = model(hand_weight_sets()[2], STANDARD_MAX_FRET); + let problem = hand_problem(&pitches_of(&[40, 45, 47]), &tuning, &zeros).unwrap(); + assert!(problem.objective().is_empty()); + assert_eq!(problem.hard().len(), 6); + assert_eq!(hand_problem(&[], &tuning, &zeros), Err(LabError::EmptyLine)); + assert_eq!( + hand_problem(&pitches_of(&[30]), &tuning, &zeros), + Err(LabError::UnpositionablePitch { + index: 0, + pitch: 30 + }) + ); +} + +// ── holdout ─────────────────────────────────────────────────────────────────── + +#[test] +fn song_key_folds_arrangements_of_one_song() { + assert_eq!( + song_key("A Lot Like Birds - Connector (ver 2 by LPFzCS_LMS).gp5"), + "a lot like birds - connector" + ); + assert_eq!( + song_key("A Lot Like Birds - Connector.gp5"), + "a lot like birds - connector" + ); + assert_eq!(song_key("Band - Song (Live) (ver 3).gpx"), "band - song"); + assert_eq!(song_key("Band - Title.gp"), "band - title"); + assert_eq!(song_key("No Extension"), "no extension"); +} + +#[test] +fn holdout_bucket_is_stable_and_bounded() { + let k = song_key("A Lot Like Birds - Connector.gp5"); + assert_eq!(holdout_bucket(&k, 5), holdout_bucket(&k, 5)); + assert!(holdout_bucket(&k, 5) < 5); + assert_eq!(holdout_bucket(&k, 0), 0); + assert_eq!(holdout_bucket(&k, 1), 0); + let spread: std::collections::BTreeSet = (0..200) + .map(|i| holdout_bucket(&format!("band - song {i}"), 5)) + .collect(); + assert_eq!(spread.len(), 5); +} + +// ── repeat consistency ──────────────────────────────────────────────────────── + +#[test] +fn repeat_pairs_find_non_overlapping_repeated_figures() { + let p = pitches_of; + assert_eq!(repeat_pairs(&p(&[40, 45, 47, 40, 45, 47]), 3), vec![(0, 3)]); + assert_eq!( + repeat_pairs(&p(&[50, 52, 55, 57, 50, 52, 55]), 3), + vec![(0, 4)] + ); + assert_eq!( + repeat_pairs(&p(&[50, 52, 50, 52, 50, 52]), 2), + vec![(0, 2), (2, 4)] + ); + assert_eq!(repeat_pairs(&p(&[40, 40, 40, 40, 40, 40]), 3), vec![]); + assert_eq!(repeat_pairs(&p(&[40, 45, 40, 45]), 0), vec![]); + assert_eq!(repeat_pairs(&p(&[40, 45, 40]), 2), vec![]); +} + +#[test] +fn repeat_consistency_admits_only_identically_fingered_repeats() { + let tuning = Tuning::standard_e(); + let pitches = pitches_of(&[52, 55, 57, 52, 55, 57]); + let base = v1_problem( + &pitches, + &tuning, + &FingeringWeights::v1(), + STANDARD_MAX_FRET, + ) + .unwrap(); + let pairs = repeat_pairs(&pitches, 3); + let constrained = with_repeat_consistency(&base, V1_VARS_PER_NOTE, &pairs, 3).unwrap(); + assert_eq!(constrained.hard().len(), base.hard().len() + 3); + let mut consistent = 0; + for line in candidate_lines(&pitches, &tuning, STANDARD_MAX_FRET) { + let witness = encode_v1_witness(&line); + let same = (0..3).all(|k| line[k] == line[3 + k]); + if same { + consistent += 1; + assert_eq!(constrained.evaluate(&witness), base.evaluate(&witness)); + } else { + assert!(matches!( + constrained.evaluate(&witness), + Err(WitnessError::HardViolated { index }) if index >= base.hard().len() + )); + } + } + assert!(consistent > 1); + assert!(matches!( + with_repeat_consistency(&base, V1_VARS_PER_NOTE, &[(0, 5)], 3), + Err(OptIrError::Ir(_)) + )); +} + +#[test] +fn string_tiebreak_scales_cost_and_prefers_lower_strings() { + let tuning = Tuning::standard_e(); + for weights in v1_weight_sets() { + let pitches = pitches_of(&[52, 57, 64, 59]); + let base = v1_problem(&pitches, &tuning, &weights, STANDARD_MAX_FRET).unwrap(); + let (tie, scale) = with_string_tiebreak(&base, V1_VARS_PER_NOTE).unwrap(); + assert_eq!(scale, 4 * 6 + 1); + let lines = candidate_lines(&pitches, &tuning, STANDARD_MAX_FRET); + for line in &lines { + let w = encode_v1_witness(line); + let strings: i64 = line.iter().map(|p| i64::from(p.string)).sum(); + assert_eq!( + tie.evaluate(&w).unwrap(), + scale * base.evaluate(&w).unwrap() + strings + ); + } + let best_base = lines + .iter() + .map(|l| base.evaluate(&encode_v1_witness(l)).unwrap()) + .min() + .unwrap(); + let best_tie = lines + .iter() + .map(|l| tie.evaluate(&encode_v1_witness(l)).unwrap()) + .min() + .unwrap(); + assert_eq!(best_tie.div_euclid(scale), best_base); + } + let hand = hand_problem( + &pitches_of(&[52, 57]), + &tuning, + &model(hand_weight_sets()[0], STANDARD_MAX_FRET), + ) + .unwrap(); + let (_, scale) = with_string_tiebreak(&hand, HAND_VARS_PER_NOTE).unwrap(); + assert_eq!(scale, 2 * 6 + 1); +} diff --git a/lab/tests/optir.rs b/lab/tests/optir.rs new file mode 100644 index 00000000..1aeeff95 --- /dev/null +++ b/lab/tests/optir.rs @@ -0,0 +1,495 @@ +//! Red → contract tests for the solver-neutral optimization IR (`optir`). +//! +//! Pins: construction refusals and canonical form, exact re-scoring of every +//! term kind (the only authority on a witness), the wire shape an external +//! solver adapter consumes and produces, and the verdict rules that decide +//! when a solver's optimality claim is accepted. + +#![allow( + clippy::expect_used, + clippy::unwrap_used, + clippy::panic, + clippy::missing_assert_message, + clippy::indexing_slicing, + clippy::arithmetic_side_effects +)] + +use griff_constraint_lab::{ + ir::{IntVar, IrError, VarId}, + manifest::SolverIdentity, + optir::{ + verify_agreement, verify_record, AgreementError, AgreementRecord, Hard, OptIrError, + OptProblem, ProblemRecord, SolveRecord, SolveStatus, Term, Verdict, WitnessError, + OPT_SCHEMA, OPT_SCHEMA_VERSION, + }, +}; + +/// x ∈ {0,1,2}, y ∈ {0,2,5}; (x, y) ∈ {(0,0),(1,2),(2,5),(2,2)}; +/// cost = unary(x: 1→4, 2→-3) + pair(x,y: (1,2)→7) + 2·|x−y| + 5·[x≠y]. +fn sample() -> OptProblem { + OptProblem::try_new( + "sample", + vec![ + IntVar::new("x", vec![2, 0, 1]), + IntVar::new("y", vec![5, 0, 2]), + ], + vec![Hard::Allowed { + a: VarId(0), + b: VarId(1), + tuples: vec![(2, 5), (0, 0), (1, 2), (2, 2)], + }], + vec![ + Term::Unary { + var: VarId(0), + costs: vec![(2, -3), (1, 4)], + }, + Term::Pair { + a: VarId(0), + b: VarId(1), + costs: vec![(1, 2, 7)], + }, + Term::AbsDiff { + a: VarId(0), + b: VarId(1), + weight: 2, + }, + Term::NotEqual { + a: VarId(0), + b: VarId(1), + weight: 5, + }, + ], + ) + .expect("valid sample") +} + +fn solver() -> SolverIdentity { + SolverIdentity { + name: "test".into(), + version: "0".into(), + } +} + +fn record( + problem: &OptProblem, + status: SolveStatus, + objective: i64, + witness: Vec, +) -> SolveRecord { + SolveRecord { + id: "r".into(), + fingerprint_hex: format!("{:016x}", problem.fingerprint()), + solver: solver(), + status, + objective: Some(objective), + bound: Some(objective), + witness: Some(witness), + wall_us: 1, + agreement: None, + } +} + +// ── construction ────────────────────────────────────────────────────────────── + +#[test] +fn refuses_dangling_ids_in_hard_and_objective() { + let vars = || vec![IntVar::new("x", vec![0, 1])]; + let hard = OptProblem::try_new( + "p", + vars(), + vec![Hard::Allowed { + a: VarId(0), + b: VarId(3), + tuples: vec![(0, 0)], + }], + vec![], + ); + assert_eq!( + hard, + Err(OptIrError::Ir(IrError::DanglingVarId { id: 3, vars: 1 })) + ); + for term in [ + Term::Unary { + var: VarId(1), + costs: vec![], + }, + Term::Pair { + a: VarId(0), + b: VarId(1), + costs: vec![], + }, + Term::AbsDiff { + a: VarId(1), + b: VarId(0), + weight: 1, + }, + Term::NotEqual { + a: VarId(0), + b: VarId(1), + weight: 1, + }, + ] { + assert_eq!( + OptProblem::try_new("p", vars(), vec![], vec![term]), + Err(OptIrError::Ir(IrError::DanglingVarId { id: 1, vars: 1 })) + ); + } +} + +#[test] +fn refuses_shared_ir_violations() { + assert!(matches!( + OptProblem::try_new("p", vec![IntVar::new("x", vec![])], vec![], vec![]), + Err(OptIrError::Ir(IrError::EmptyDomain { .. })) + )); + assert!(matches!( + OptProblem::try_new( + "p", + vec![IntVar::new("x", vec![0]), IntVar::new("x", vec![1])], + vec![], + vec![] + ), + Err(OptIrError::Ir(IrError::DuplicateName { .. })) + )); + assert!(matches!( + OptProblem::try_new("p", vec![IntVar::new("1x", vec![0])], vec![], vec![]), + Err(OptIrError::Ir(IrError::UnsafeName { .. })) + )); +} + +#[test] +fn refuses_ambiguous_cost_tables_and_empty_hard_tables() { + let vars = || vec![IntVar::new("x", vec![0, 1]), IntVar::new("y", vec![0, 1])]; + assert_eq!( + OptProblem::try_new( + "p", + vars(), + vec![], + vec![ + Term::AbsDiff { + a: VarId(0), + b: VarId(1), + weight: 1 + }, + Term::Unary { + var: VarId(0), + costs: vec![(1, 2), (1, 3)] + } + ] + ), + Err(OptIrError::DuplicateCostKey { term: 1 }) + ); + assert_eq!( + OptProblem::try_new( + "p", + vars(), + vec![], + vec![Term::Pair { + a: VarId(0), + b: VarId(1), + costs: vec![(0, 1, 2), (0, 1, 2)] + }] + ), + Err(OptIrError::DuplicateCostKey { term: 0 }) + ); + assert_eq!( + OptProblem::try_new( + "p", + vars(), + vec![ + Hard::Allowed { + a: VarId(0), + b: VarId(1), + tuples: vec![(0, 0)] + }, + Hard::Allowed { + a: VarId(0), + b: VarId(1), + tuples: vec![] + } + ], + vec![] + ), + Err(OptIrError::EmptyAllowedTable { index: 1 }) + ); +} + +#[test] +fn tables_are_canonical_so_fingerprints_ignore_input_order() { + let reordered = OptProblem::try_new( + "sample", + vec![ + IntVar::new("x", vec![0, 1, 2]), + IntVar::new("y", vec![0, 2, 5]), + ], + vec![Hard::Allowed { + a: VarId(0), + b: VarId(1), + tuples: vec![(0, 0), (2, 2), (1, 2), (2, 5), (0, 0)], + }], + vec![ + Term::Unary { + var: VarId(0), + costs: vec![(1, 4), (2, -3)], + }, + Term::Pair { + a: VarId(0), + b: VarId(1), + costs: vec![(1, 2, 7)], + }, + Term::AbsDiff { + a: VarId(0), + b: VarId(1), + weight: 2, + }, + Term::NotEqual { + a: VarId(0), + b: VarId(1), + weight: 5, + }, + ], + ) + .expect("valid"); + assert_eq!(reordered, sample()); + assert_eq!(reordered.fingerprint(), sample().fingerprint()); + let canonical = sample(); + let Hard::Allowed { tuples, .. } = &canonical.hard()[0]; + assert_eq!(tuples, &vec![(0, 0), (1, 2), (2, 2), (2, 5)]); +} + +#[test] +fn fingerprint_is_sensitive_to_a_weight() { + let base = sample(); + let mut objective = base.objective().to_vec(); + objective[2] = Term::AbsDiff { + a: VarId(0), + b: VarId(1), + weight: 3, + }; + let changed = OptProblem::try_new( + base.name(), + base.vars().to_vec(), + base.hard().to_vec(), + objective, + ) + .expect("valid"); + assert_ne!(changed.fingerprint(), base.fingerprint()); +} + +// ── evaluation ──────────────────────────────────────────────────────────────── + +#[test] +fn evaluates_every_term_kind_exactly() { + let p = sample(); + // (0,0): unary 0 (absent) + pair 0 + 2·0 + 5·0 = 0 + assert_eq!(p.evaluate(&[0, 0]), Ok(0)); + // (1,2): unary 4 + pair 7 + 2·1 + 5·1 = 18 + assert_eq!(p.evaluate(&[1, 2]), Ok(18)); + // (2,5): unary −3 + pair 0 + 2·3 + 5·1 = 8 + assert_eq!(p.evaluate(&[2, 5]), Ok(8)); + // (2,2): unary −3 + 0 + 0 + 0 = −3 + assert_eq!(p.evaluate(&[2, 2]), Ok(-3)); +} + +#[test] +fn evaluation_refuses_inadmissible_witnesses() { + let p = sample(); + assert_eq!( + p.evaluate(&[0]), + Err(WitnessError::Length { + expected: 2, + got: 1 + }) + ); + assert_eq!( + p.evaluate(&[3, 0]), + Err(WitnessError::OutOfDomain { + name: "x".into(), + value: 3 + }) + ); + assert_eq!( + p.evaluate(&[0, 2]), + Err(WitnessError::HardViolated { index: 0 }) + ); +} + +#[test] +fn evaluation_refuses_overflow() { + let p = OptProblem::try_new( + "big", + vec![ + IntVar::new("x", vec![i64::MIN, i64::MAX]), + IntVar::new("y", vec![i64::MIN, i64::MAX]), + ], + vec![], + vec![Term::AbsDiff { + a: VarId(0), + b: VarId(1), + weight: 2, + }], + ) + .expect("valid"); + assert_eq!( + p.evaluate(&[i64::MIN, i64::MAX]), + Err(WitnessError::Overflow) + ); + assert_eq!(p.evaluate(&[i64::MAX, i64::MAX]), Ok(0)); +} + +// ── wire contract ───────────────────────────────────────────────────────────── + +#[test] +fn problem_record_wire_shape_is_pinned() { + let p = sample(); + let fp = p.fingerprint(); + let rec = ProblemRecord::new("line-7", p, vec![(VarId(0), 2)]); + assert_eq!(rec.fingerprint_hex, format!("{fp:016x}")); + let json: serde_json::Value = serde_json::to_value(&rec).expect("serializes"); + assert_eq!(json["schema"], OPT_SCHEMA); + assert_eq!(json["version"], OPT_SCHEMA_VERSION); + assert_eq!(json["id"], "line-7"); + assert_eq!(json["problem"]["vars"][0]["name"], "x"); + assert_eq!( + json["problem"]["vars"][0]["domain"], + serde_json::json!([0, 1, 2]) + ); + assert_eq!(json["problem"]["hard"][0]["kind"], "allowed"); + assert_eq!( + json["problem"]["hard"][0]["tuples"][1], + serde_json::json!([1, 2]) + ); + let kinds: Vec<&str> = json["problem"]["objective"] + .as_array() + .unwrap() + .iter() + .map(|t| t["kind"].as_str().unwrap()) + .collect(); + assert_eq!(kinds, ["unary", "pair", "abs_diff", "not_equal"]); + assert_eq!( + json["problem"]["objective"][1]["costs"][0], + serde_json::json!([1, 2, 7]) + ); + assert_eq!(json["reference"], serde_json::json!([[0, 2]])); +} + +#[test] +fn solve_record_parses_the_adapter_output() { + let line = r#"{"id":"line-7","fingerprint_hex":"00000000000000ff", + "solver":{"name":"ortools/cp-sat","version":"9.15.6755"}, + "status":"optimal","objective":-3,"bound":-3,"witness":[2,2],"wall_us":1234, + "agreement":{"status":"optimal","matched":1,"witness":[2,2]}}"#; + let rec: SolveRecord = serde_json::from_str(line).expect("parses"); + assert_eq!(rec.status, SolveStatus::Optimal); + assert_eq!(rec.witness, Some(vec![2, 2])); + assert_eq!(rec.agreement.unwrap().matched, Some(1)); + let infeasible = r#"{"id":"x","fingerprint_hex":"0","solver":{"name":"s","version":"v"}, + "status":"infeasible","objective":null,"bound":null,"witness":null,"wall_us":0,"agreement":null}"#; + let rec: SolveRecord = serde_json::from_str(infeasible).expect("parses"); + assert_eq!(rec.status, SolveStatus::Infeasible); +} + +// ── verdicts ────────────────────────────────────────────────────────────────── + +#[test] +fn verdict_proven_only_for_a_verified_optimal_claim() { + let p = sample(); + assert_eq!( + verify_record(&p, &record(&p, SolveStatus::Optimal, -3, vec![2, 2])), + Verdict::Proven { optimum: -3 } + ); +} + +#[test] +fn verdict_refuses_every_broken_claim() { + let p = sample(); + let mut wrong_fp = record(&p, SolveStatus::Optimal, -3, vec![2, 2]); + wrong_fp.fingerprint_hex = "0000000000000000".into(); + assert_eq!(verify_record(&p, &wrong_fp), Verdict::FingerprintMismatch); + + assert_eq!( + verify_record(&p, &record(&p, SolveStatus::Feasible, -3, vec![2, 2])), + Verdict::NotProven { + status: SolveStatus::Feasible + } + ); + + let mut no_witness = record(&p, SolveStatus::Optimal, -3, vec![]); + no_witness.witness = None; + assert_eq!(verify_record(&p, &no_witness), Verdict::MissingWitness); + + assert_eq!( + verify_record(&p, &record(&p, SolveStatus::Optimal, 0, vec![0, 2])), + Verdict::WitnessInvalid(WitnessError::HardViolated { index: 0 }) + ); + + assert_eq!( + verify_record(&p, &record(&p, SolveStatus::Optimal, 0, vec![2, 2])), + Verdict::ObjectiveMismatch { + claimed: 0, + rescored: -3, + bound: Some(0) + } + ); + + let mut loose_bound = record(&p, SolveStatus::Optimal, -3, vec![2, 2]); + loose_bound.bound = Some(-5); + assert_eq!( + verify_record(&p, &loose_bound), + Verdict::ObjectiveMismatch { + claimed: -3, + rescored: -3, + bound: Some(-5) + } + ); +} + +#[test] +fn agreement_pass_is_recounted_and_pinned_to_the_optimum() { + let p = sample(); + let reference = vec![(VarId(0), 2), (VarId(1), 5)]; + let ok = AgreementRecord { + status: SolveStatus::Optimal, + matched: Some(1), + witness: Some(vec![2, 2]), + }; + assert_eq!(verify_agreement(&p, &reference, -3, &ok), Ok(1)); + + let off = AgreementRecord { + status: SolveStatus::Optimal, + matched: Some(2), + witness: Some(vec![2, 5]), + }; + assert_eq!( + verify_agreement(&p, &reference, -3, &off), + Err(AgreementError::OffOptimum { + optimum: -3, + rescored: 8 + }) + ); + + let miscount = AgreementRecord { + status: SolveStatus::Optimal, + matched: Some(2), + witness: Some(vec![2, 2]), + }; + assert_eq!( + verify_agreement(&p, &reference, -3, &miscount), + Err(AgreementError::CountMismatch { + claimed: 2, + recounted: 1 + }) + ); + + let unproven = AgreementRecord { + status: SolveStatus::Unknown, + matched: None, + witness: None, + }; + assert_eq!( + verify_agreement(&p, &reference, -3, &unproven), + Err(AgreementError::NotProven { + status: SolveStatus::Unknown + }) + ); +}