From 0aab91ae3d2235b99b9fe82b414a3f60e012aa63 Mon Sep 17 00:00:00 2001 From: Thomas Dybdahl Ahle Date: Wed, 26 Aug 2026 11:04:45 +0200 Subject: [PATCH] Tune shallow search jointly --- compressed.py | 4 +- formal/README.md | 74 ++++---- formal/Sunfish/BandContract.lean | 2 +- formal/Sunfish/CappedMove.lean | 16 +- formal/Sunfish/Killer.lean | 2 +- formal/Sunfish/MateDepth.lean | 284 ++++++++++++++----------------- formal/Sunfish/Stalemate.lean | 16 +- formal/scripts/model_audit.py | 8 +- sunfish.py | 10 +- tests/test_regressions.py | 35 ++-- tests/test_terminal_bench.py | 4 +- tools/ctwin/sunfish.c | 10 +- tools/quick_tests.sh | 12 +- 13 files changed, 227 insertions(+), 250 deletions(-) diff --git a/compressed.py b/compressed.py index cd4694f0..03904c13 100755 --- a/compressed.py +++ b/compressed.py @@ -74,7 +74,7 @@ def bound(self, pos, gamma, depth, root=False): if entry.upper < gamma: return entry.upper if depth > 0 and pos in self.history: return 0 killer = self.tp_move.get(pos) - ceiling = lambda v: MATE_UPPER if depth > 3 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A + ceiling = lambda v: MATE_UPPER if depth > 4 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A def moves(): if 2 < depth < 6 and guard: yield None, None if depth == 0: yield None, None @@ -95,7 +95,7 @@ def moves(): elif val >= MATE_LOWER: score, live = MATE_UPPER, True else: if (cap := ceiling(val)) < gamma: best = max(best, cap); break - move_depth = depth - 1 - (guard and depth >= 6 and val < LMR) - int(nmr) + move_depth = depth - 1 - (guard and depth >= 7 and val < LMR) - int(nmr) score = min(cap, -self.bound(pos.move(move), 1 - gamma, move_depth)) live |= score > -MATE_UPPER best = max(best, score) diff --git a/formal/README.md b/formal/README.md index a9dacc0c..fe71e146 100644 --- a/formal/README.md +++ b/formal/README.md @@ -94,13 +94,13 @@ From depth 6 on the pass is not a score candidate at all. One fixed target shapes only how much depth the real moves spend: ```python -d = depth -guard = depth >= 6 and abs(pos.score) < 750 and any(c in pos.board for c in "RBNQ") -if guard: - t = pos.score + NULL_MARGIN - d -= int(-self.bound(pos.rotate(nullmove=True), 1 - t, depth - 7) >= t) +calm = abs(pos.score) < 750 and any(c in pos.board for c in "RBNQ") +guard = not root and calm +t = pos.score + NULL_MARGIN +nmr = calm and depth >= 6 and -self.bound( + pos.rotate(nullmove=True), 1 - t, depth - 7) >= t -move_depth = depth - 1 - (guard and depth >= 6 and val < LMR) - int(nmr) +move_depth = depth - 1 - (guard and depth >= 7 and val < LMR) - int(nmr) ``` The target depends on `(pos, depth)` alone -- `gamma` does not enter. Table @@ -211,23 +211,23 @@ forcedMate_fuelValueD2_sharp : D >= max 2 (C*(k-2) + 6) -- 3k shipped ( forcedlyMated_fuelValueD2_sharp : D >= max 6 (C*(k-1) + 6) -- 3k+3 shipped (was 3k+7) ``` -**The shallow cap costs one more ply, and `fuelValueD2` did not have it.** +**The shallow cap costs two more plies, and `fuelValueD2` did not have it.** The fuel value omits ```python -cap = MATE_UPPER if depth > 3 or val >= MATE_LOWER else pos.score + val + margin +cap = MATE_UPPER if depth > 4 or val >= MATE_LOWER else pos.score + val + margin ``` and that cap puts every non-king-capture report strictly below `MATE_LOWER` (`shallowMoveCap_below_positiveMate`, under the both-kings material invariant `CapInBand` - the clamp that used to make this syntactic was dead code and is gone): an attacker node at any nominal depth -zero through three cannot report a mate at all. This is the delay the section +zero through four cannot report a mate at all. This is the delay the section above calls "a mate proof found exactly at the selective frontier", priced. -`capClamp` carries the same `depth <= 3` band as the shipped `cap`, and the +`capClamp` carries the same `depth <= 4` band as the shipped `cap`, and the two ends of the band behave differently: -- at depths **two and three** the clamp is the selective cap, and it binds: +- at depths **two through four** the clamp is the selective cap, and it binds: the mate the attacker can see one ply below is replaced by `pos.score + val + (depth - 1) * QS_A`. - at depths **zero and one** natural subtraction flattens the margin and the @@ -235,17 +235,17 @@ two ends of the band behave differently: It is mate-neutral there, and not by luck: a fold weight can only reach the positive mate band through a child whose king is gone, and such a parent fires the node-level `hasKingCapture` branch before any fold is taken. So - widening the band from `2 <= depth <= 3` to `depth <= 3` moves no value in + widening the band from `2 <= depth <= 4` to `depth <= 4` moves no value in this file. The cap only ever LOWERS a report, so a defender node (bounded above) pays -nothing for it; the attacker's floor rises from 2 to 4 -- depths 2 and 3 are +nothing for it; the attacker's floor rises from 2 to 5 -- depths 2 through 4 are blocked outright and depths 0 and 1 are below the fold floor either way. `fuelValueD2C` is `fuelValueD2` with the clamp on every fold weight, and ```text -forcedMate_fuelValueD2C_sharp : D >= max 4 (C*(k-1) + 4) (C*(k-2) + 6) -- 3k+1 -forcedlyMated_fuelValueD2C_sharp : D >= max 6 (C*k + 4) (C*k + 6 - C) -- 3k+4 +forcedMate_fuelValueD2C_sharp : D >= max 5 (C*(k-1) + 5) (C*(k-2) + 7) -- 3k+2 +forcedlyMated_fuelValueD2C_sharp : D >= max 7 (C*k + 5) (C*k + 7 - C) -- 3k+5 ``` Premises unchanged throughout: `ValFloor G 192` and nothing else -- no @@ -266,23 +266,23 @@ worth 0 and the mate is masked: | `sharp_mate3_at_8` | mate in 3 plies, value 0 at `D = 8 = 3*3 - 1` | | `sharp_mate5_at_14` | mate in 5 plies, value 0 at `D = 14 = 3*5 - 1` | | `sharp_mated3_at_11` | the dual escapes at `D = 11 = 3*3 + 2` | -| `sharp_cap_mate3_at_9` | with the cap, `D = 9 = 3*3` is still one ply short | +| `sharp_cap_mate3_at_10` | with the cap, `D = 10 = 3*3+1` is still one ply short | The pair at 8 and 14 is `2*C` apart, so no bound with a slope below `C` holds either: the certificates pin the slope as well as the constants. **The CI table.** `tools/quick_tests.sh` states the convention -- mate-in-`n` -moves is `k = 2n - 1` plies -- and currently spends `3k + 4`: +moves is `k = 2n - 1` plies -- and currently spends the proved `3k + 2`: | suite | `k` | script today | proved, fuel model | proved, shipped (cap) | | --- | --- | --- | --- | --- | -| `mate1.fen` | 1 | 7 | 2 (`ci_mate_in_1`) | 4 (`ci_code_mate_in_1`) | -| `mate2_eventual.fen` | 3 | 13 | 9 (`ci_mate_in_2`) | 10 (`ci_code_mate_in_2`) | -| `mate3_eventual.fen` | 5 | 19 | 15 (`ci_mate_in_3`) | 16 (`ci_code_mate_in_3`) | +| `mate1.fen` | 1 | 5 | 2 (`ci_mate_in_1`) | 5 (`ci_code_mate_in_1`) | +| `mate2_eventual.fen` | 3 | 11 | 9 (`ci_mate_in_2`) | 11 (`ci_code_mate_in_2`) | +| `mate3_eventual.fen` | 5 | 17 | 15 (`ci_mate_in_3`) | 17 (`ci_code_mate_in_3`) | The shipped column is the one a CI depth may be lowered to. The gap between -the columns is the shallow cap, and it is not academic: at depth 3 the suite's -mate-in-1 positions are all missed, and at depth 4 all eight are found. The +the columns is the shallow cap, and it is not academic: at depth 4 the suite's +mate-in-1 positions are all missed, and at depth 5 all eight are found. The fuel-model column -- 2 / 9 / 15 -- costs the whole cap, on both branches of the consumer, at the Elo the correction under the menu records; the cheap route to it is refuted there, so those three depths are not reachable that @@ -294,16 +294,16 @@ new proof: | engine variant | bound | theorem | | --- | --- | --- | -| today (`C = 3`, cap, sub-horizon pass) | `3k + 1` | `forcedMate_fuelValueD2C_sharp` | -| one reduction bit (`C = 2`) | `2k + 2` | `forcedMate_fuelValueD2C_C2` | -| no reductions (`C = 1`) | `k + 4` | `forcedMate_fuelValueD2C_C1` | -| delete the sub-horizon pass ONLY | `3k + 1` -- unchanged | `code_mate_depth_bound_sharp_k3_guardOff` | +| today (`C = 3`, cap, sub-horizon pass) | `3k + 2` | `forcedMate_fuelValueD2C_sharp` | +| one reduction bit (`C = 2`) | `2k + 3` | `forcedMate_fuelValueD2C_C2` | +| no reductions (`C = 1`) | `k + 5` | `forcedMate_fuelValueD2C_C1` | +| delete the sub-horizon pass ONLY | `3k + 2` -- unchanged | `code_mate_depth_bound_sharp_k3_guardOff` | | delete the shallow cap ONLY -- on BOTH branches | `3k` | `forcedMate_fuelValueD2_sharp`, sharp per `sharp_mate3_at_8` | | exempt only the SEARCHED report from the cap | `3k` for the declared value | **REFUTED on correctness** -- gamma-dependent, see below | | delete both | `max 2 (C*k + 4 - 3*C)`, i.e. `3k - 5` | `forcedMate_fuelValueD2_noSubPass` | The fourth row is the useful surprise: the cap and the sub-horizon pass mask -in *different* depth bands (2--3 for the capped attacker, 3--5 for the +in *different* depth bands (2--4 for the capped attacker, 3--5 for the defender's pass), and removing either one alone leaves the other binding. The certificate is the same witness game with the guard off -- it still masks, at the capped attacker node. @@ -363,17 +363,16 @@ table, is unpriced and recorded here as a note only. Evidence: against pre-#216 `bound()`. #215 and #218 moved the fuel probe and the intrinsic-LMR bit out of the `moves()` generator, deleted the depth-one lazy tail and the `depth <= 1` futility break, made admission unconditional at -positive depth, and widened the cap band to `depth <= 3`. The two mechanisms +positive depth, and widened the cap band to `depth <= 4`. The two mechanisms the bounds spend are byte-identical after the move -- the probe is still one ply at `depth - 7`, and the reduced move depth is still one intrinsic-LMR bit and one fuel bit off `depth` - now spelled `depth - 1 - (guard and -depth >= 6 and val < LMR) - int(nmr)` with `guard = not root and calm`, +depth >= 7 and val < LMR) - int(nmr)` with `guard = not root and calm`, the same predicates - so `C = 3` holds -- and the admission change cannot reach the proofs, which never fold at nominal depth one. `MateDepth.lean`'s header carries the mechanism-by-mechanism audit. The -suites confirm it: first-success depths are unchanged across the refactor at -`mate1` 4, `mate2_eventual` 7, and `mate3_eventual` 15, with `mate1` still -missed at 3 -- the mate-in-1 corner is exactly tight at `3k + 1`. +suites exercise the new proved depths 5, 11, and 17, with `mate1` still missed +at 4 -- the mate-in-1 corner is exactly tight at the cap horizon. ## Positive-depth moves and shallow move caps @@ -427,7 +426,7 @@ The producer also resolves an intrinsic mate-band move immediately as branch is an actual king capture. Recursing into its kingless child would only return `-MATE_UPPER`, so the normalization is exact. -At depths zero through three, every other admitted move passes through the +At depths zero through four, every other admitted move passes through the same static cap ```text @@ -444,7 +443,7 @@ spell never bound - `EvalBounds`' headline is the concrete arithmetic. At depths one, natural subtraction makes the margin zero. The score identity then makes the cap exactly the existing stand-pat futility report; this is `shallowMoveCap_lowDepth` together with `futilityOK_discharged`. At depths two -and three, the cap defines the selective move value. +through four, the cap defines the selective move value. The implementation evaluates that same fixed fold lazily, and it never computes the threshold. The producer yields `(value, move)` pairs - the sort @@ -491,14 +490,15 @@ The killer is the one move the break cannot see: it is yielded before the sorted stream, so its cap says nothing about what follows. The producer therefore admits it by the same ceiling the consumer prunes on - "every out-of-order real move yielded can reach gamma" - `ceiling(val) >= gamma` -with `ceiling(v) = MATE_UPPER if depth > 3 or v >= MATE_LOWER else +with `ceiling(v) = MATE_UPPER if depth > 4 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A`, which IS the old threshold with its `min` unfolded (`v >= min(a, b)` iff `v >= a` or `v >= b`), so the gate is exactly the retired `val_lower` test. A killer that would settle is simply not yielded; it still reaches the fold in its sorted position, inside the tail whose report the break delivers anyway. A searched killer that failed low is -re-searched from the sorted stream against a table entry, as before. Above depth three the threshold equals `base`, the tail is +re-searched from the sorted stream against a table entry, as before. Above +depth four the threshold equals `base`, the tail is empty, and the cap disappears. For searched moves, `WindowReport.cap` still transports the child report through `min`. @@ -513,7 +513,7 @@ genuine negative mate is retained exactly. The cap deliberately changes ordinary shallow move values, including captures, promotions, and checks. It can therefore delay a mate proof found exactly at -the selective frontier. It exists only at depths two and three, so deeper +the selective frontier. It exists only at depths two through four, so deeper iterations move every fixed proof above that frontier. Its strength is an empirical question, separate from report correctness. diff --git a/formal/Sunfish/BandContract.lean b/formal/Sunfish/BandContract.lean index 19ae39a4..641af61c 100644 --- a/formal/Sunfish/BandContract.lean +++ b/formal/Sunfish/BandContract.lean @@ -768,7 +768,7 @@ theorem window_flip_preserves_range {gamma : Int} (h1 : -MATE_UPPER < gamma) (h2 : gamma ≤ MATE_UPPER) : -MATE_UPPER < 1 - gamma ∧ 1 - gamma ≤ MATE_UPPER := ⟨by omega, by omega⟩ -/-- **The intentional asymmetry, in one statement.** At depth ≤ 3 a SEARCHED +/-- **The intentional asymmetry, in one statement.** At depth ≤ 4 a SEARCHED move is clamped strictly below the mate band, while a king capture bypasses the clamp entirely and reports the token: the two never overlap, so a shallow search can neither invent a mate nor hide a capture. -/ diff --git a/formal/Sunfish/CappedMove.lean b/formal/Sunfish/CappedMove.lean index 9468c561..ebfaa22e 100644 --- a/formal/Sunfish/CappedMove.lean +++ b/formal/Sunfish/CappedMove.lean @@ -7,7 +7,7 @@ the window and move table. A mate-band intrinsic value is normalized directly to `MATE_UPPER`; `HighValIsKingCapture` says that this branch is exactly a king capture, whose recursive child would immediately return `-MATE_UPPER`. -Every other move at depths zero through three has the fixed cap +Every other move at depths zero through four has the fixed cap static + gain + (depth - 1) * QS_A. @@ -18,12 +18,12 @@ the code used to spell never bound. Natural subtraction makes the margin zero at depths zero and one. There the cap is the existing exact stand-pat futility estimate: the score identity and `futilityOK_discharged` show that it targets the ordinary child value. At -depths two and three it instead declares the move value to be the minimum of +depths two through four it instead declares the move value to be the minimum of the cap and the full child value. If the cap lies below the window, the child need not be searched; otherwise `WindowReport.cap` transports its report. The positive-band ceiling prevents a selective cap from inventing mate. The -cap disappears above depth three. The implementation evaluates this fixed +cap disappears above depth four. The implementation evaluates this fixed fold lazily, and it does so WITHOUT ever computing the threshold: the producer yields `(value, move)` pairs in decreasing intrinsic value, and the consumer caps each move at its single scoring site. When the cap is below @@ -64,7 +64,7 @@ move (so no king was captured making it), and the null child shares the board. Hence `|pos.score|` is material-bounded (about 15k - EvalBounds' headline proves the static eval alone sits strictly below the band), an ordinary move value is below ~2k, and the shallow margin is at most -`2 * QS_A = 280` (the cap lives at `depth <= 3`) - the sum tops out around +`3 * QS_A = 540` (the cap lives at `depth <= 4`) - the sum tops out around a third of `MATE_LOWER - 1 = 47922`, so the clamp the code used to spell could never bind. CAVEAT: `MATE_LOWER` is derived, `piece[K] - 13 * piece[Q]`. In twin-option space the headroom closes around `piece[Q] >~ @@ -177,7 +177,7 @@ def producerFloor (depth : Nat) : Int := king captures in the searched prefix. Above the capped horizon the threshold is just the producer floor, so the tail is empty. -/ def lazyMoveThreshold (static gamma : Int) (depth : Nat) : Int := - if depth ≤ 3 then + if depth ≤ 4 then max (producerFloor depth) (min MATE_LOWER (gamma - static - ((depth - 1 : Nat) : Int) * QS_A)) @@ -228,7 +228,7 @@ theorem mem_lazyMoveTail {G : QSGame} {static gamma : Int} {depth : Nat} arithmetic correspondence between Python's intrinsic threshold and the cap; no chess or child-search premise is involved. -/ theorem lazyMoveTail_cap_lt_gamma (G : QSGame) (hF : ValFloor G 192) - (static gamma : Int) (depth : Nat) (p m : G.Pos) (hdepth : depth ≤ 3) + (static gamma : Int) (depth : Nat) (p m : G.Pos) (hdepth : depth ≤ 4) (hm : m ∈ lazyMoveTail G static gamma depth p) : shallowMoveCap static (G.val p m) depth < gamma := by have hmem := (mem_lazyMoveTail.mp hm).1 @@ -265,7 +265,7 @@ because `val < MATE_LOWER` bounds it under the window. Dropping the clamp made this iff UNCONDITIONAL in `gamma`: the old side condition `gamma <= MATE_LOWER - 1` marked exactly where the two clamps agreed. -/ theorem shippedCap_iff_tail (G : QSGame) (hF : ValFloor G 192) - (static gamma : Int) (depth : Nat) (p m : G.Pos) (hdepth : depth ≤ 3) + (static gamma : Int) (depth : Nat) (p m : G.Pos) (hdepth : depth ≤ 4) (hm : m ∈ producerMoves G depth p) (hval : G.val p m < MATE_LOWER) : shallowMoveCap static (G.val p m) depth < gamma ↔ m ∈ lazyMoveTail G static gamma depth p := by @@ -306,7 +306,7 @@ theorem foldMax_windowReports {α : Type _} (gamma : Int) actual capped tail values. -/ theorem lazyMoveTail_report (G : QSGame) (hF : ValFloor G 192) (static gamma : Int) (depth : Nat) (p : G.Pos) (full : G.Pos → Int) - (hdepth : depth ≤ 3) (hwindow : LOSS < gamma) : + (hdepth : depth ≤ 4) (hwindow : LOSS < gamma) : WindowReport gamma (foldMax (fun m => shallowMoveCap static (G.val p m) depth) (lazyMoveTail G static gamma depth p) LOSS) diff --git a/formal/Sunfish/Killer.lean b/formal/Sunfish/Killer.lean index 97959ace..b30b1a0f 100644 --- a/formal/Sunfish/Killer.lean +++ b/formal/Sunfish/Killer.lean @@ -56,7 +56,7 @@ own named condition `NullGuardBlocksAtCaptures` below. Audit note (exactness): sunfish gates the killer yield by the producer's admission floor AND by the same ceiling the consumer prunes on -- `(val >= QS or depth) and ceiling(val) >= gamma`, where `ceiling(v)` is -`MATE_UPPER if depth > 3 or v >= MATE_LOWER else pos.score + v + +`MATE_UPPER if depth > 4 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A` (the retired `val_lower` threshold with its `min` unfolded) -- so that the consumer's settled break, which is only sound on the sorted stream, can never fire on the diff --git a/formal/Sunfish/MateDepth.lean b/formal/Sunfish/MateDepth.lean index 7df0c114..feb8f998 100644 --- a/formal/Sunfish/MateDepth.lean +++ b/formal/Sunfish/MateDepth.lean @@ -19,8 +19,8 @@ the mate. Two of those charges are not needed: same max -- `foldMax_le_of_mem` ignores the accumulator, so a pass candidate can never pull the maximum DOWN. The horizon is irrelevant to the attacker. (Below the horizon the shipped code also reduces - nothing: `move_depth = d - 1 - (not root and guard and val < LMR)` - with `guard = depth >= 6 and ...`, so each sub-horizon edge costs + nothing: intrinsic LMR starts at depth 7 and the fuel probe at depth 6, + so each sub-horizon edge costs exactly one ply, as `fuelValueD2`'s sub-horizon branch records.) * the CHECKMATED leaf is classified by the depth-gated terminal correction at any depth `≥ 1` (`fuelValueD2_checkmated`). @@ -78,10 +78,11 @@ MECHANISM MAP (pre-#216 line -> post-#218 line). 4673322 has since renamed the locals only (`target` -> `t`, `nullpos` inlined at its single use, the bool subtraction spelled `int(...)`), so the current text reads - `guard = depth >= 6 and abs(pos.score) < 750 and any(c in pos.board ...)`, + `calm = abs(pos.score) < 750 and any(c in pos.board ...)`, `t = pos.score + NULL_MARGIN`, - `d -= int(-self.bound(pos.rotate(nullmove=True), 1 - t, depth - 7) >= t)`. - Still ONE ply (`d -= <0 or 1>`), still ONE probe, still at the fixed target + `nmr = calm and depth >= 6 and -self.bound(pos.rotate(nullmove=True), + 1 - t, depth - 7) >= t`. Still ONE ply (`int(nmr)`), still ONE probe, + still at the fixed target `pos.score + NULL_MARGIN` and depth `depth - 7`. `NULL_MARGIN = -200` and its tuner range `(-400, 800)` are untouched; the reworded comment's "burn two plies" is the TOTAL real-move reduction (base ply + hot bit), not a @@ -89,7 +90,8 @@ MECHANISM MAP (pre-#216 line -> post-#218 line). * intrinsic-LMR bit: `:439` -> `:437`. MOVED ONLY, out of the deleted `score_move` helper into the consumer loop. Expression byte-identical, - `move_depth = d - 1 - (not root and guard and val < LMR)`, and `val` is + `move_depth = depth - 1 - (guard and depth >= 7 and val < LMR) - int(nmr)`, + and `val` is still `pos.value(move)` (the consumer only enters that branch when the produced score is below `MATE_LOWER`, where it equals the intrinsic value). `intrinsicSpend`, `intrinsic_child_depth` and `spend <= 2` unchanged. @@ -108,12 +110,10 @@ MECHANISM MAP (pre-#216 line -> post-#218 line). depths 3-5, and every defender node in both inductions is required to sit at nominal depth >= 6 (`fuelValueD2C_of_fold_regime`, `hd : 5 <= d`). -* shallow static cap: `:441-442` -> `:433-434`. The band WIDENED from - `2 <= depth <= 3` to `depth <= 3`; the arithmetic is unchanged inside the - old band (`max(depth - 1, 0)` reproduces `(depth - 1)` at depths 2 and 3, - and master has already made `shallowMoveCap` use natural subtraction to - match). This was the only real model delta and `capClamp` now carries the - widened band -- see the closing section. The cap's guard +* shallow static cap: the band now extends through depth 4. The arithmetic is + unchanged in shape, while the tuned `QS_A = 180` makes its largest margin + `3 * QS_A = 540`. `capClamp` carries the widened band -- see the closing + section. The cap's guard `val < MATE_LOWER` is unchanged; its `MATE_LOWER - 1` ceiling has since been dropped from the code as dead under the both-kings material invariant, so `shallowMoveCap_below_positiveMate` now applies through @@ -153,43 +153,17 @@ MECHANISM MAP (pre-#216 line -> post-#218 line). `tp_move` store behave as before, and the terminal finalizer (`:456-472`) is untouched. -THE ONE EDIT, TAKEN. `capClamp` used to guard on `2 <= d /\ d <= 3`; it now -guards on `d <= 3`, the shipped band. The theorems are parametric in the -clamp: the only clamp facts any proof body uses are `capClamp_le` (the clamp -lowers) and `capClamp_of_deep` (identity from depth 4). Both survived -verbatim -- the edit was one token in `capClamp_of_deep`'s `if_neg`, one -dropped hypothesis in `capClamp_lt_ML`, and one `And.intro` nesting in -`sharp_cap_A0_3`, with `capClamp_lt_ML` coming out STRONGER (`d <= 3` instead -of `2 <= d /\ d <= 3`). Evaluating the old and the new clamp side by side on -the witness game gives the same number everywhere: - - old band {2,3} new band {0,1,2,3} - fuelValueD2C MDG 9 A1 = 280 fuelValueD2C MDG 9 A1 = 280 - fuelValueD2C MDG 10 A1 = 47968 fuelValueD2C MDG 10 A1 = 47968 - guard off, MDG 9 A1 = 280 guard off, MDG 9 A1 = 280 - -so `sharp_cap_mate3_at_9`, `code_mate_depth_bound_sharp_k3` and -`code_mate_depth_bound_sharp_k3_guardOff` are unaffected -- 280 is below -`MATE_LOWER = 47923` at `D = 3k = 9`, and 47968 is above it at -`D = 3k + 1 = 10`. `MDG` has -`val = 0` and `eval = 0` off `KG`, so its admitted sets and its depth-0/1 -fold weights are identical under both the old and the new producer; the -uncapped certificates `sharp_mate3_at_8`, `sharp_mate5_at_14` and -`sharp_mated3_at_11` all still evaluate to 0. The attacker floor stays 4: -depths 2 and 3 were already blocked, and at depths 0 and 1 a fold weight can -only reach the mate band through a child whose king is gone, which fires the -node-level `hasKingCapture` branch before any fold. - -EMPIRICAL ANCHORS (pre-#216 e499dae vs post-#218 d0687b9, same harness). -First-success depths did NOT move on any suite: - - mate1.fen 0/8 at D=3, 8/8 at D=4 (proved `ci_code_mate_in_1` = 4) - mate2_eventual.fen 1/5 at D=6, 5/5 at D=7 (proved `ci_code_mate_in_2` = 10) - mate3_eventual.fen 1/2 at D=14, 2/2 at D=15 (proved `ci_code_mate_in_3` = 16) - -Identical counts at every depth from 1 to 16 on both engines. The mate-in-1 -corner is still exactly tight -- missed at `3k = 3`, found at `3k + 1 = 4` -- -which is the observable the cap's ply predicts. +CURRENT RE-AUDIT. The tuned cap extends through depth 4, so `capClamp` now +guards on `d <= 4` and becomes the identity from depth 5. The proof spine +uses only that identity, `capClamp_le`, and the mate-band separation. Its +uniform bounds therefore rise by one ply. The witness was extended one node: +at `D = 10` the last attacker lands at depth 4 and is capped at 540, below +`MATE_LOWER`; at `D = 11` the proof clears the cap. Thus `3k + 2` is sharp. + +The executable regression depths move with that theorem: mate-in-1/2/3 use +5/11/17. All formal modules compile, the terminal battery passes at its new +depth-5 observation horizon, and the uncapped Part I certificates are +unchanged. -/ import Sunfish.IntrinsicLMR @@ -428,10 +402,10 @@ theorem forcedlyMated_intrinsicValue_sharp (G : QSGame) (guard : G.Pos → Bool) /-! ## The CI table The suite convention (`tools/quick_tests.sh`): mate-in-`n` moves is -`k = 2n - 1` plies. The three depths the sharpened bound licenses, -against the `3k + 4` the suite currently uses. -/ +`k = 2n - 1` plies. These are the cap-free comparison depths; the executable +suite uses the capped depths 5/11/17 below. -/ -/-- mate-in-1 (`k = 1`): `D = 2` suffices (suite: 7). -/ +/-- mate-in-1 (`k = 1`): `D = 2` suffices (capped suite: 5). -/ theorem ci_mate_in_1 (G : QSGame) (guard : G.Pos → Bool) (hot eligible : G.Pos → Nat → Bool) (low : G.Pos → Nat → G.Pos → Bool) (hF : ValFloor G 192) {p : G.Pos} (hFM : ForcedMate G 1 p) : @@ -439,14 +413,14 @@ theorem ci_mate_in_1 (G : QSGame) (guard : G.Pos → Bool) forcedMate_fuelValueD2_short G guard 3 (intrinsicEdgeSpend G hot eligible low) (by omega) (by omega) hF (by omega) hFM 2 (by omega) -/-- mate-in-2 (`k = 3`): `D = 9` suffices (suite: 13). -/ +/-- mate-in-2 (`k = 3`): `D = 9` suffices (capped suite: 11). -/ theorem ci_mate_in_2 (G : QSGame) (guard : G.Pos → Bool) (hot eligible : G.Pos → Nat → Bool) (low : G.Pos → Nat → G.Pos → Bool) (hF : ValFloor G 192) {p : G.Pos} (hFM : ForcedMate G 3 p) : MATE_LOWER ≤ fuelValueD2 G guard 3 (intrinsicEdgeSpend G hot eligible low) 9 p := forcedMate_intrinsicValue_sharp G guard hot eligible low hF hFM 9 (by omega) (by omega) -/-- mate-in-3 (`k = 5`): `D = 15` suffices (suite: 19). -/ +/-- mate-in-3 (`k = 5`): `D = 15` suffices (capped suite: 17). -/ theorem ci_mate_in_3 (G : QSGame) (guard : G.Pos → Bool) (hot eligible : G.Pos → Nat → Bool) (low : G.Pos → Nat → G.Pos → Bool) (hF : ValFloor G 192) {p : G.Pos} (hFM : ForcedMate G 5 p) : @@ -625,11 +599,11 @@ theorem forcedMate_fuelValueD2_sharp_C1 (G : QSGame) (guard : G.Pos → Bool) Part I's sharpened `3k` -- does NOT model one mechanism the shipped search has: the shallow static cap - ceiling = lambda v: MATE_UPPER if depth > 3 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A + ceiling = lambda v: MATE_UPPER if depth > 4 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A if (cap := ceiling(val)) < gamma: best = max(best, cap); break score = min(cap, -self.bound(pos.move(move), 1 - gamma, move_depth)) -At every nominal depth `≤ 3` EVERY move that is not a king capture reports +At every nominal depth `≤ 4` EVERY move that is not a king capture reports at most `shallowMoveCap`, which `shallowMoveCap_below_positiveMate` (CappedMove.lean) puts strictly below `MATE_LOWER` under the both-kings material invariant `CapInBand` - the spine below consumes it through @@ -640,26 +614,25 @@ the selective frontier", as formal/README.md puts it, and this is the delay, priced. The cap only ever LOWERS a report, so it cannot hurt a defender node (whose fold needs an upper bound); it binds exactly at the ATTACKER nodes of the mating line, whose admission floor therefore rises -from 2 to 4. +from 2 to 5. -The two ends of the band are not the same mechanism. At depths 2 and 3 the +The two ends of the band are not the same mechanism. At depths 2 through 4 the clamp is the SELECTIVE cap and it binds. At depths 0 and 1 natural subtraction flattens the margin and the clamp is the old stand-pat futility estimate (`shallowMoveCap_lowDepth`), where it is mate-neutral -- a fold weight can only reach the positive mate band through a child whose king is gone, and such a parent fires the node-level `hasKingCapture` branch before -any fold is taken. So `capClamp` carries the shipped `depth ≤ 3` band -exactly, and the floor is still 4. +any fold is taken. So `capClamp` carries the shipped `depth ≤ 4` band +exactly, and the floor is 5. Consequence for the uniform bound (`fuelValueD2C` below is `fuelValueD2` plus the clamp): - D ≥ 4, C*k + 4 ≤ D + C, C*k + 6 ≤ D + 2*C + D ≥ 5, C*k + 5 ≤ D + C, C*k + 7 ≤ D + 2*C -i.e. `D ≥ max 4 (C*(k-1) + 4) (C*(k-2) + 6)`, which at the shipped `C = 3` -is `D ≥ 3k + 1` for `k ≥ 3` and `D ≥ 4` for `k ≤ 2` -- three plies below -the shipped `3k + 4`, one above Part I's cap-free `3k`. The one-ply corner -is exactly what the suite shows: mate-in-1 needs `D = 4`, not 2. +i.e. `D ≥ max 5 (C*(k-1) + 5) (C*(k-2) + 7)`, which at the shipped `C = 3` +is `D ≥ 3k + 2` for `k ≥ 3` and `D ≥ 5` for `k ≤ 2`. The one-ply corner +is exactly what the suite shows: mate-in-1 needs `D = 5`. MEASUREMENT CORRECTION (2026-08-17). The cheap way to buy Part I's cap-free `3k` in the shipped engine -- keep the clamp, but exempt a child @@ -687,13 +660,13 @@ at -60.41 ± 26.61 Elo, so Elo-inadmissible -- or a /-- The shipped cap as a fold weight transformer, under the model's band ENVELOPE `min (MATE_LOWER - 1) ·`. The band is the consumer's own -`depth > 3` test, so it covers depths 0 through 3. The code carries no +`depth > 4` test, so it covers depths 0 through 4. The code carries no such envelope; `capClamp_eq_shipped` proves the two agree under the material invariant `CapInBand`, which localizes the both-kings premise to that one lemma and lets the whole mate-depth spine below keep consuming the envelope's unconditional band-safety. -/ def capClamp (G : QSGame) (p : G.Pos) (d : Nat) (m : G.Pos) (x : Int) : Int := - if d ≤ 3 ∧ G.val p m < MATE_LOWER then + if d ≤ 4 ∧ G.val p m < MATE_LOWER then min (min (MATE_LOWER - 1) (shallowMoveCap (G.eval p) (G.val p m) d)) x else x @@ -702,7 +675,7 @@ model's fold weight is exactly the shipped `min(cap, child)`. -/ theorem capClamp_eq_shipped (G : QSGame) (p : G.Pos) (d : Nat) (m : G.Pos) (x : Int) (hband : CapInBand (G.eval p) (G.val p m) d) : capClamp G p d m x = - if d ≤ 3 ∧ G.val p m < MATE_LOWER then + if d ≤ 4 ∧ G.val p m < MATE_LOWER then min (shallowMoveCap (G.eval p) (G.val p m) d) x else x := by have hb : G.eval p + G.val p m + ((d - 1 : Nat) : Int) * QS_A @@ -724,19 +697,18 @@ theorem capClamp_le (G : QSGame) (p : G.Pos) (d : Nat) (m : G.Pos) (x : Int) : · exact Int.min_le_right _ _ · exact Int.le_refl x -/-- Above depth three the clamp is the identity: it "disappears above depth -three", as `CappedMove.lean` states. -/ -theorem capClamp_of_deep (G : QSGame) (p : G.Pos) {d : Nat} (hd : 4 ≤ d) +/-- Above depth four the clamp is the identity. -/ +theorem capClamp_of_deep (G : QSGame) (p : G.Pos) {d : Nat} (hd : 5 ≤ d) (m : G.Pos) (x : Int) : capClamp G p d m x = x := by unfold capClamp rw [if_neg (fun h => by have := h.1; omega)] /-- At any depth in the band no ordinary move can report a mate. -/ -theorem capClamp_lt_ML (G : QSGame) (p : G.Pos) {d : Nat} (hd3 : d ≤ 3) +theorem capClamp_lt_ML (G : QSGame) (p : G.Pos) {d : Nat} (hd4 : d ≤ 4) (m : G.Pos) (hval : G.val p m < MATE_LOWER) (x : Int) : capClamp G p d m x < MATE_LOWER := by unfold capClamp - rw [if_pos ⟨hd3, hval⟩] + rw [if_pos ⟨hd4, hval⟩] have h1 := Int.min_le_left (MATE_LOWER - 1) (shallowMoveCap (G.eval p) (G.val p m) d) have h2 := Int.min_le_left @@ -847,17 +819,16 @@ theorem fuelValueD2C_checkmated (G : QSGame) (guard : G.Pos → Bool) have := terminalValue_mate G (d' + 1) m hmate.2 omega -/-- The last ply under the cap: the attacker node needs depth `≥ 4`, because -at 2 and 3 its own report is clamped below the band. -/ +/-- The last ply under the cap: the attacker node needs depth `≥ 5`. -/ theorem forcedMate_leaf_fuelValueD2C (G : QSGame) (guard : G.Pos → Bool) (C : Nat) (spend : G.Pos → Nat → G.Pos → Nat) (hC1 : 1 ≤ C) (hC4 : C ≤ 4) (hF : ValFloor G 192) {p m : G.Pos} (hkg : ¬ (G.eval p ≤ -MATE_LOWER)) (hm : m ∈ G.moves p) (hleg : hasKingCapture G.toNullGame.toGame m = false) (hmate : Checkmated G m) : - ∀ D : Nat, 4 ≤ D → MATE_LOWER ≤ fuelValueD2C G guard C spend D p := by + ∀ D : Nat, 5 ≤ D → MATE_LOWER ≤ fuelValueD2C G guard C spend D p := by have hMU : MATE_UPPER = 69290 := rfl have hML : MATE_LOWER = 47923 := rfl - intro D h4 + intro D h5 cases D with | zero => omega | succ d => @@ -898,22 +869,22 @@ theorem forcedMate_leaf_fuelValueD2C (G : QSGame) (guard : G.Pos → Bool) omega /-- **Mate-in-k completeness for the SHIPPED search, sharp**: the cap costs -one ply of slope-independent depth and raises the one-ply corner to 4. -Shipped `C = 3`: `D ≥ 3k + 1` (`k ≥ 3`), `D ≥ 4` (`k ≤ 2`). `ValFloor` +two plies of slope-independent depth and raises the one-ply corner to 5. +Shipped `C = 3`: `D ≥ 3k + 2` (`k ≥ 3`), `D ≥ 5` (`k ≤ 2`). `ValFloor` only -- still no chess premise. -/ theorem forcedMate_fuelValueD2C_sharp (G : QSGame) (guard : G.Pos → Bool) (C : Nat) (spend : G.Pos → Nat → G.Pos → Nat) (hC1 : 1 ≤ C) (hC4 : C ≤ 4) (hF : ValFloor G 192) {k : Nat} {p : G.Pos} (hFM : ForcedMate G k p) : - ∀ D : Nat, 4 ≤ D → C * k + 4 ≤ D + C → C * k + 6 ≤ D + 2 * C → + ∀ D : Nat, 5 ≤ D → C * k + 5 ≤ D + C → C * k + 7 ≤ D + 2 * C → MATE_LOWER ≤ fuelValueD2C G guard C spend D p := by have hMU : MATE_UPPER = 69290 := rfl have hML : MATE_LOWER = 47923 := rfl have hLOSS : LOSS = -MATE_UPPER := rfl induction hFM with | @mate k p m hkg hm hleg hmate => - intro D h4 _ _ - exact forcedMate_leaf_fuelValueD2C G guard C spend hC1 hC4 hF hkg hm hleg hmate D h4 + intro D h5 _ _ + exact forcedMate_leaf_fuelValueD2C G guard C spend hC1 hC4 hF hkg hm hleg hmate D h5 | @step k p m hkg hm hleg hnt hreply ih => intro D h4 hD1 hD2 rcases Nat.eq_zero_or_pos k with hk0 | hk1 @@ -969,19 +940,19 @@ theorem forcedMate_fuelValueD2C_sharp (G : QSGame) (guard : G.Pos → Bool) /-- The mated dual under the cap: the cap only lowers reports, so the defender side pays nothing for it beyond the mate side's own floor. -Shipped `C = 3`: `D ≥ 3k + 4`. -/ +Shipped `C = 3`: `D ≥ 3k + 5`. -/ theorem forcedlyMated_fuelValueD2C_sharp (G : QSGame) (guard : G.Pos → Bool) (C : Nat) (spend : G.Pos → Nat → G.Pos → Nat) (hC1 : 1 ≤ C) (hC4 : C ≤ 4) (hF : ValFloor G 192) {k : Nat} {q : G.Pos} (hcapq : hasKingCapture G.toNullGame.toGame q = false) (hFL : ForcedlyMated G k q) : - ∀ D : Nat, 6 ≤ D → C * k + 4 ≤ D → C * k + 6 ≤ D + C → + ∀ D : Nat, 7 ≤ D → C * k + 5 ≤ D → C * k + 7 ≤ D + C → fuelValueD2C G guard C spend D q ≤ -MATE_LOWER := by have hMU : MATE_UPPER = 69290 := rfl have hML : MATE_LOWER = 47923 := rfl have hLOSS : LOSS = -MATE_UPPER := rfl - intro D h6 hD1 hD2 + intro D h7 hD1 hD2 cases D with | zero => omega | succ d => @@ -1026,53 +997,51 @@ theorem forcedlyMated_fuelValueD2C_sharp (G : QSGame) (guard : G.Pos → Bool) /-! ## The CI table for the SHIPPED search (`C = 3`, cap included) The suite convention (`tools/quick_tests.sh`): mate-in-`n` moves is -`k = 2n - 1` plies. These are the depths the sharpened accounting licenses -for the engine as it stands, against the `3k + 4` in the script today. -/ +`k = 2n - 1` plies. These are both the sharp proved depths and the executable +suite depths for the engine as it stands. -/ -/-- mate-in-1 (`k = 1`): `D = 4`. Suite today: 7. -/ +/-- mate-in-1 (`k = 1`): `D = 5`. -/ theorem ci_code_mate_in_1 (G : QSGame) (guard : G.Pos → Bool) (hot eligible : G.Pos → Nat → Bool) (low : G.Pos → Nat → G.Pos → Bool) (hF : ValFloor G 192) {p : G.Pos} (hFM : ForcedMate G 1 p) : - MATE_LOWER ≤ fuelValueD2C G guard 3 (intrinsicEdgeSpend G hot eligible low) 4 p := + MATE_LOWER ≤ fuelValueD2C G guard 3 (intrinsicEdgeSpend G hot eligible low) 5 p := forcedMate_fuelValueD2C_sharp G guard 3 (intrinsicEdgeSpend G hot eligible low) - (by omega) (by omega) hF hFM 4 (by omega) (by omega) (by omega) + (by omega) (by omega) hF hFM 5 (by omega) (by omega) (by omega) -/-- mate-in-2 (`k = 3`): `D = 10`. Suite today: 13. -/ +/-- mate-in-2 (`k = 3`): `D = 11`. -/ theorem ci_code_mate_in_2 (G : QSGame) (guard : G.Pos → Bool) (hot eligible : G.Pos → Nat → Bool) (low : G.Pos → Nat → G.Pos → Bool) (hF : ValFloor G 192) {p : G.Pos} (hFM : ForcedMate G 3 p) : - MATE_LOWER ≤ fuelValueD2C G guard 3 (intrinsicEdgeSpend G hot eligible low) 10 p := + MATE_LOWER ≤ fuelValueD2C G guard 3 (intrinsicEdgeSpend G hot eligible low) 11 p := forcedMate_fuelValueD2C_sharp G guard 3 (intrinsicEdgeSpend G hot eligible low) - (by omega) (by omega) hF hFM 10 (by omega) (by omega) (by omega) + (by omega) (by omega) hF hFM 11 (by omega) (by omega) (by omega) -/-- mate-in-3 (`k = 5`): `D = 16`. Suite today: 19. (The measured -first-success depth of the hardest suite position is 15, so 16 keeps one -ply of margin -- and the theorem says no position can need more.) -/ +/-- mate-in-3 (`k = 5`): `D = 17`. -/ theorem ci_code_mate_in_3 (G : QSGame) (guard : G.Pos → Bool) (hot eligible : G.Pos → Nat → Bool) (low : G.Pos → Nat → G.Pos → Bool) (hF : ValFloor G 192) {p : G.Pos} (hFM : ForcedMate G 5 p) : - MATE_LOWER ≤ fuelValueD2C G guard 3 (intrinsicEdgeSpend G hot eligible low) 16 p := + MATE_LOWER ≤ fuelValueD2C G guard 3 (intrinsicEdgeSpend G hot eligible low) 17 p := forcedMate_fuelValueD2C_sharp G guard 3 (intrinsicEdgeSpend G hot eligible low) - (by omega) (by omega) hF hFM 16 (by omega) (by omega) (by omega) + (by omega) (by omega) hF hFM 17 (by omega) (by omega) (by omega) /-- Menu options at a glance, capped model: one reduction bit (`C = 2`) -gives `D ≥ 2k + 2`; no reductions (`C = 1`) gives `D ≥ k + 3`. Both are +gives `D ≥ 2k + 3`; no reductions (`C = 1`) gives `D ≥ k + 5`. Both are instances -- only the edge-cost cap changes. -/ theorem forcedMate_fuelValueD2C_C2 (G : QSGame) (guard : G.Pos → Bool) (spend : G.Pos → Nat → G.Pos → Nat) (hF : ValFloor G 192) {k : Nat} {p : G.Pos} (hFM : ForcedMate G k p) : - ∀ D : Nat, 4 ≤ D → 2 * k + 2 ≤ D → + ∀ D : Nat, 5 ≤ D → 2 * k + 3 ≤ D → MATE_LOWER ≤ fuelValueD2C G guard 2 spend D p := - fun D h4 hD => forcedMate_fuelValueD2C_sharp G guard 2 spend (by omega) (by omega) - hF hFM D h4 (by omega) (by omega) + fun D h5 hD => forcedMate_fuelValueD2C_sharp G guard 2 spend (by omega) (by omega) + hF hFM D h5 (by omega) (by omega) theorem forcedMate_fuelValueD2C_C1 (G : QSGame) (guard : G.Pos → Bool) (spend : G.Pos → Nat → G.Pos → Nat) (hF : ValFloor G 192) {k : Nat} {p : G.Pos} (hFM : ForcedMate G k p) : - ∀ D : Nat, 4 ≤ D → k + 4 ≤ D → + ∀ D : Nat, 5 ≤ D → k + 5 ≤ D → MATE_LOWER ≤ fuelValueD2C G guard 1 spend D p := - fun D h4 hD => forcedMate_fuelValueD2C_sharp G guard 1 spend (by omega) (by omega) - hF hFM D h4 (by omega) (by omega) + fun D h5 hD => forcedMate_fuelValueD2C_sharp G guard 1 spend (by omega) (by omega) + hF hFM D h5 (by omega) (by omega) /-! # Part II: sharpness @@ -1299,105 +1268,110 @@ theorem mated_depth_bound_sharp_k3 : /-! ## Sharpness of the capped bound -The same game certifies the extra ply the cap costs. At `D = 9 = 3*3` -- -Part I's cap-free bound -- the mating line's last attacker node lands at -nominal depth 3, where the shipped cap clamps its report to -`shallowMoveCap = 280`. The mate never leaves that node, so the root -reports 280, not a mate score: `3k + 1` is the exact bound for the shipped -search, and `3k` is one ply too few. -/ +The same game certifies the two plies the widened cap costs. At +`D = 10 = 3*3+1`, the mating line's last attacker node lands at nominal +depth 4, where the shipped cap clamps its report to `shallowMoveCap = 540`. +The mate never leaves that node, so `3k + 2` is the exact uniform bound and +`3k + 1` is one ply too few. -/ theorem sharp_cap_ZP0 (g : MDPos → Bool) : fuelValueD2C MDG g 3 mdSpend 0 MDPos.ZP = 0 := by simp only [fuelValueD2C] rw [if_neg (by decide), if_neg (by decide)] rfl -/-- The capped last attacker node: at nominal depth 3 the mate it can see +theorem sharp_cap_ZP1 (g : MDPos → Bool) : fuelValueD2C MDG g 3 mdSpend 1 MDPos.ZP = 0 := by + rw [fuelValueD2C_of_allIllegal MDG g 3 mdSpend 0 MDPos.ZP + (by decide) (by decide) (by decide)] + have hic : inCheckB MDG.toNullGame MDPos.ZP = false := by decide + simp [terminalValue, hic] + +/-- The capped last attacker node: at nominal depth 4 the mate it can see one ply below is clamped to the static cap. -/ -theorem sharp_cap_A0_3 (g : MDPos → Bool) : fuelValueD2C MDG g 3 mdSpend 3 MDPos.A0 ≤ 280 := by +theorem sharp_cap_A0_4 (g : MDPos → Bool) : fuelValueD2C MDG g 3 mdSpend 4 MDPos.A0 ≤ 540 := by have hMU : MATE_UPPER = 69290 := rfl have hML : MATE_LOWER = 47923 := rfl have hLOSS : LOSS = -MATE_UPPER := rfl - have hma : movesAbove MDG (val_lower 3) MDPos.A0 = [MDPos.LF] := - movesAbove_all MDG 3 MDPos.A0 (by decide) - have hZ : fuelValueD2C MDG g 3 mdSpend (2 + 1 - 3) (MDG.pass MDPos.A0) = 0 := - sharp_cap_ZP0 g - rw [show (3 : Nat) = 2 + 1 from rfl, - fuelValueD2C_of_fold_sub MDG g 3 mdSpend 2 MDPos.A0 + have hma : movesAbove MDG (val_lower 4) MDPos.A0 = [MDPos.LF] := + movesAbove_all MDG 4 MDPos.A0 (by decide) + have hZ : fuelValueD2C MDG g 3 mdSpend (3 + 1 - 3) (MDG.pass MDPos.A0) = 0 := + sharp_cap_ZP1 g + rw [show (4 : Nat) = 3 + 1 from rfl, + fuelValueD2C_of_fold_sub MDG g 3 mdSpend 3 MDPos.A0 (by decide) (by decide) (by decide) (by omega), hma, hZ] refine foldMax_le _ _ _ (fun m hm => ?_) (by split <;> (try split) <;> omega) have hm' : m = MDPos.LF := by simpa using hm subst hm' - have hcap : capClamp MDG MDPos.A0 (2 + 1) MDPos.LF - (-(fuelValueD2C MDG g 3 mdSpend 2 MDPos.LF)) - ≤ shallowMoveCap (MDG.eval MDPos.A0) (MDG.val MDPos.A0 MDPos.LF) (2 + 1) := by + have hcap : capClamp MDG MDPos.A0 (3 + 1) MDPos.LF + (-(fuelValueD2C MDG g 3 mdSpend 3 MDPos.LF)) + ≤ shallowMoveCap (MDG.eval MDPos.A0) (MDG.val MDPos.A0 MDPos.LF) (3 + 1) := by unfold capClamp rw [if_pos (And.intro (by omega) (by decide))] exact Int.min_le_left _ _ - have hval : shallowMoveCap (MDG.eval MDPos.A0) (MDG.val MDPos.A0 MDPos.LF) (2 + 1) = 280 := by - show shallowMoveCap (0 : Int) 0 3 = 280 + have hval : shallowMoveCap (MDG.eval MDPos.A0) (MDG.val MDPos.A0 MDPos.LF) (3 + 1) = 540 := by + show shallowMoveCap (0 : Int) 0 4 = 540 unfold shallowMoveCap QS_A omega omega /-- The defender node above it keeps its escape, one ply of depth cheaper than in the cap-free model. -/ -theorem sharp_cap_D1_6 (g : MDPos → Bool) : -280 ≤ fuelValueD2C MDG g 3 mdSpend 6 MDPos.D1 := by - have hma : movesAbove MDG (val_lower 6) MDPos.D1 = [MDPos.A0] := - movesAbove_all MDG 6 MDPos.D1 (by decide) - have hA0 := sharp_cap_A0_3 g - rw [show (6 : Nat) = 5 + 1 from rfl, - fuelValueD2C_of_fold_regime MDG g 3 mdSpend 5 MDPos.D1 +theorem sharp_cap_D1_7 (g : MDPos → Bool) : -540 ≤ fuelValueD2C MDG g 3 mdSpend 7 MDPos.D1 := by + have hma : movesAbove MDG (val_lower 7) MDPos.D1 = [MDPos.A0] := + movesAbove_all MDG 7 MDPos.D1 (by decide) + have hA0 := sharp_cap_A0_4 g + rw [show (7 : Nat) = 6 + 1 from rfl, + fuelValueD2C_of_fold_regime MDG g 3 mdSpend 6 MDPos.D1 (by decide) (by decide) (by decide) (by omega), hma] - have hcl := capClamp_of_deep MDG MDPos.D1 (d := 5 + 1) (by omega) MDPos.A0 - (-(fuelValueD2C MDG g 3 mdSpend (5 - min (3 - 1) (mdSpend MDPos.D1 (5 + 1) MDPos.A0)) + have hcl := capClamp_of_deep MDG MDPos.D1 (d := 6 + 1) (by omega) MDPos.A0 + (-(fuelValueD2C MDG g 3 mdSpend (6 - min (3 - 1) (mdSpend MDPos.D1 (6 + 1) MDPos.A0)) MDPos.A0)) - have hfold : capClamp MDG MDPos.D1 (5 + 1) MDPos.A0 + have hfold : capClamp MDG MDPos.D1 (6 + 1) MDPos.A0 (-(fuelValueD2C MDG g 3 mdSpend - (5 - min (3 - 1) (mdSpend MDPos.D1 (5 + 1) MDPos.A0)) MDPos.A0)) - ≤ foldMax (fun x => capClamp MDG MDPos.D1 (5 + 1) x + (6 - min (3 - 1) (mdSpend MDPos.D1 (6 + 1) MDPos.A0)) MDPos.A0)) + ≤ foldMax (fun x => capClamp MDG MDPos.D1 (6 + 1) x (-(fuelValueD2C MDG g 3 mdSpend - (5 - min (3 - 1) (mdSpend MDPos.D1 (5 + 1) x)) x))) + (6 - min (3 - 1) (mdSpend MDPos.D1 (6 + 1) x)) x))) [MDPos.A0] LOSS := foldMax_le_of_mem _ _ _ _ (List.mem_cons_self _ _) rw [hcl] at hfold have hA0' : fuelValueD2C MDG g 3 mdSpend - (5 - min (3 - 1) (mdSpend MDPos.D1 (5 + 1) MDPos.A0)) MDPos.A0 ≤ 280 := hA0 + (6 - min (3 - 1) (mdSpend MDPos.D1 (6 + 1) MDPos.A0)) MDPos.A0 ≤ 540 := hA0 omega /-- **The cap's ply, certified**: `ForcedMate MDG 3 A1` holds, and at -`D = 9` the declared value of the shipped-shaped search is at most 280 -- -far below `MATE_LOWER`. So `3k` does NOT license the CI depth; `3k + 1` -is the sharp one. -/ -theorem sharp_cap_mate3_at_9 (g : MDPos → Bool) : - fuelValueD2C MDG g 3 mdSpend 9 MDPos.A1 < MATE_LOWER := by +`D = 10` the declared value of the shipped-shaped search is at most 540 -- +far below `MATE_LOWER`. So `3k + 1` does NOT license the CI depth; +`3k + 2` is sharp. -/ +theorem sharp_cap_mate3_at_10 (g : MDPos → Bool) : + fuelValueD2C MDG g 3 mdSpend 10 MDPos.A1 < MATE_LOWER := by have hML : MATE_LOWER = 47923 := rfl have hLOSS : LOSS = -MATE_UPPER := rfl have hMU : MATE_UPPER = 69290 := rfl - have hma : movesAbove MDG (val_lower 9) MDPos.A1 = [MDPos.D1] := - movesAbove_all MDG 9 MDPos.A1 (by decide) - have hD1 := sharp_cap_D1_6 g - rw [show (9 : Nat) = 8 + 1 from rfl, - fuelValueD2C_of_fold_regime MDG g 3 mdSpend 8 MDPos.A1 + have hma : movesAbove MDG (val_lower 10) MDPos.A1 = [MDPos.D1] := + movesAbove_all MDG 10 MDPos.A1 (by decide) + have hD1 := sharp_cap_D1_7 g + rw [show (10 : Nat) = 9 + 1 from rfl, + fuelValueD2C_of_fold_regime MDG g 3 mdSpend 9 MDPos.A1 (by decide) (by decide) (by decide) (by omega), hma] - refine Int.lt_of_le_of_lt (foldMax_le _ _ _ (fun m hm => ?_) (by omega)) (by omega : (280:Int) < MATE_LOWER) + refine Int.lt_of_le_of_lt (foldMax_le _ _ _ (fun m hm => ?_) (by omega)) (by omega : (540:Int) < MATE_LOWER) have hm' : m = MDPos.D1 := by simpa using hm subst hm' - have hcl := capClamp_of_deep MDG MDPos.A1 (d := 8 + 1) (by omega) MDPos.D1 - (-(fuelValueD2C MDG g 3 mdSpend (8 - min (3 - 1) (mdSpend MDPos.A1 (8 + 1) MDPos.D1)) + have hcl := capClamp_of_deep MDG MDPos.A1 (d := 9 + 1) (by omega) MDPos.D1 + (-(fuelValueD2C MDG g 3 mdSpend (9 - min (3 - 1) (mdSpend MDPos.A1 (9 + 1) MDPos.D1)) MDPos.D1)) rw [hcl] - simp only [mdSpend, show (8 - min (3 - 1) 2 : Nat) = 6 from rfl] + simp only [mdSpend, show (9 - min (3 - 1) 2 : Nat) = 7 from rfl] omega theorem code_mate_depth_bound_sharp_k3 : ∃ (G : QSGame) (guard : G.Pos → Bool) (spend : G.Pos → Nat → G.Pos → Nat) (p : G.Pos), ValFloor G 192 ∧ ForcedMate G 3 p ∧ - fuelValueD2C G guard 3 spend (3 * 3) p < MATE_LOWER := + fuelValueD2C G guard 3 spend (3 * 3 + 1) p < MATE_LOWER := ⟨MDG, mdGuard, mdSpend, MDPos.A1, sharp_valFloor, sharp_forcedMate_3_A1, - sharp_cap_mate3_at_9 mdGuard⟩ + sharp_cap_mate3_at_10 mdGuard⟩ /-- **Menu option M1 alone buys nothing**: with the shallow cap in place, the witness masks at the CAPPED attacker node, not at the pass -- so deleting the @@ -1406,8 +1380,8 @@ just the same. The two mechanisms have to go together to move the bound. -/ theorem code_mate_depth_bound_sharp_k3_guardOff : ∃ (G : QSGame) (guard : G.Pos → Bool) (spend : G.Pos → Nat → G.Pos → Nat) (p : G.Pos), ValFloor G 192 ∧ (∀ q, guard q = false) ∧ ForcedMate G 3 p ∧ - fuelValueD2C G guard 3 spend (3 * 3) p < MATE_LOWER := + fuelValueD2C G guard 3 spend (3 * 3 + 1) p < MATE_LOWER := ⟨MDG, fun _ => false, mdSpend, MDPos.A1, sharp_valFloor, fun _ => rfl, - sharp_forcedMate_3_A1, sharp_cap_mate3_at_9 (fun _ => false)⟩ + sharp_forcedMate_3_A1, sharp_cap_mate3_at_10 (fun _ => false)⟩ end Sunfish diff --git a/formal/Sunfish/Stalemate.lean b/formal/Sunfish/Stalemate.lean index b3ad6a9d..771da44f 100644 --- a/formal/Sunfish/Stalemate.lean +++ b/formal/Sunfish/Stalemate.lean @@ -673,11 +673,11 @@ just the loop's first, cutoff-checked accumulator update) is /-! ### The threshold -/ -/-- sunfish.py line 149: `QS = 40`. -/ -def QS : Int := 40 +/-- sunfish.py line 149: `QS = 36`. -/ +def QS : Int := 36 -/-- sunfish.py line 150: `QS_A = 140`. -/ -def QS_A : Int := 140 +/-- sunfish.py line 150: `QS_A = 180`. -/ +def QS_A : Int := 180 /-- The QS move-value threshold, `sunfish.py`: @@ -710,7 +710,7 @@ theorem val_lower_le_QS (d : Nat) : val_lower d ≤ QS := by (`val ≥ MATE_LOWER`) pass the filter at every depth. -/ theorem val_lower_lt_ML (d : Nat) : val_lower d < MATE_LOWER := by have h := val_lower_le_QS d - have hQ : QS = 40 := rfl + have hQ : QS = 36 := rfl have hML : MATE_LOWER = 47923 := rfl omega @@ -726,7 +726,7 @@ theorem val_lower_deep (d : Nat) (h : 1 ≤ d) : val_lower d ≤ -380 := by bought: the depth-sloped form `QS - depth * QS_A`, which masked a legal move whenever its table value fell in `[-192, -100)` at remaining depth 1. Nothing in the shipped model reads this. -/ -def val_lower_pre (d : Nat) : Int := QS - d * QS_A +def val_lower_pre (d : Nat) : Int := 40 - d * 140 theorem val_lower_pre_one : val_lower_pre 1 = -100 := by decide @@ -1954,7 +1954,7 @@ then REFUTED on real boards, which is what forced the verified design: playouts + 1,459,694 sparse positions + 214,004 corner packings) found 100+ natural corner-mate hits (simplest: `8/8/8/7p/7P/1K5P/p7/k5R1 b`, K_MID pricing the mated king's quiet - moves at 65-145, above `QS = 40`): the shape is common, not exotic. + moves at 65-145, above `QS = 36`): the shape is common, not exotic. The d2 answer is not to defend the hypothesis but to remove the consumer: `if depth and ...` excludes depth 0 from the correction entirely -- QS evaluates the fold and never claims an exact terminal @@ -2224,7 +2224,7 @@ theorem cexT_crossing : /-- Depth-0 correction-terminality, by content (this model's depth 0 is QS-as-eval, so the old engine's depth-0 loop is stated by what its gate certified): our king is on the board, no pseudo-legal move falls below -the depth-0 threshold `val_lower 0 = QS = 40`, and every pseudo-legal +the depth-0 threshold `val_lower 0 = QS = 36`, and every pseudo-legal move loses the king to an immediate recapture. -/ def CorrectionTerminal0 (G : QSGame) (p : G.Pos) : Prop := ¬ (G.eval p ≤ -MATE_LOWER) ∧ allAboveB G 0 p = true ∧ diff --git a/formal/scripts/model_audit.py b/formal/scripts/model_audit.py index 8836f637..e0b712a9 100644 --- a/formal/scripts/model_audit.py +++ b/formal/scripts/model_audit.py @@ -46,9 +46,9 @@ "Position.move": "2bb64b5eed188bc4", "Position.rotate": "c0ba20968acca6ce", "Position.value": "11d52eaa8a661352", - "Searcher.bound": "533228b5272ab3f0", + "Searcher.bound": "bde33f994242678a", "Searcher.search": "d1a2cb5c89a77c53", - "constants": "62b96e206341a2fb", + "constants": "a606e88a69af8dd0", } @@ -106,13 +106,13 @@ def extract_regions(): "score = min(cap, -self.bound(pos.rotate(nullmove=True), 1 - gamma, depth - 3))", "if score >= gamma and (proof := pos.king_capture()):", "move, score, live = proof, MATE_UPPER, True", - "ceiling = lambda v: MATE_UPPER if depth > 3 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A", + "ceiling = lambda v: MATE_UPPER if depth > 4 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A", "if killer and ((val := pos.value(killer)) >= QS or depth) and ceiling(val) >= gamma: yield val, killer", "yield val, killer", "yield from sorted(((v, m) for m in pos.gen_moves() if (v := pos.value(m)) >= QS or depth), reverse=True)", "for val, move in moves():", "if (cap := ceiling(val)) < gamma: best = max(best, cap); break", - "move_depth = depth - 1 - (guard and depth >= 6 and val < LMR) - int(nmr)", + "move_depth = depth - 1 - (guard and depth >= 7 and val < LMR) - int(nmr)", "score = min(cap, -self.bound(pos.move(move), 1 - gamma, move_depth))", "live |= score > -MATE_UPPER", "best, live = -MATE_UPPER, False", diff --git a/sunfish.py b/sunfish.py index b8390019..3e3213cd 100755 --- a/sunfish.py +++ b/sunfish.py @@ -160,9 +160,9 @@ MATE_UPPER = piece["K"] + 10 * piece["Q"] # Constants for tuning search -QS = 40 -QS_A = 140 -LMR = 75 +QS = 36 +QS_A = 180 +LMR = 70 # Two jobs, deliberately one number: the width the MTD-bi bracket stops at, # and what one ply of mate distance is worth. Distances must be more than a # bracket apart or the driver's last window could not order two mates. @@ -415,7 +415,7 @@ def bound(self, pos, gamma, depth, root=False): # board at every call site, so the sum tops out a third of the way to # MATE_LOWER (CapInBand in CappedMove.lean, and its caveat if # piece["Q"] ever grows past ~2400). - ceiling = lambda v: MATE_UPPER if depth > 3 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A + ceiling = lambda v: MATE_UPPER if depth > 4 or v >= MATE_LOWER else pos.score + v + max(depth - 1, 0) * QS_A def moves(): @@ -482,7 +482,7 @@ def moves(): # the cutoff block, it stores nothing, exactly as the old # suffix report did. if (cap := ceiling(val)) < gamma: best = max(best, cap); break - move_depth = depth - 1 - (guard and depth >= 6 and val < LMR) - int(nmr) + move_depth = depth - 1 - (guard and depth >= 7 and val < LMR) - int(nmr) score = min(cap, -self.bound(pos.move(move), 1 - gamma, move_depth)) live |= score > -MATE_UPPER best = max(best, score) diff --git a/tests/test_regressions.py b/tests/test_regressions.py index 05210f05..adefe76f 100644 --- a/tests/test_regressions.py +++ b/tests/test_regressions.py @@ -253,17 +253,20 @@ def test_edge_cost_is_intrinsic_and_killer_independent(self): (self.FEN, 5, 0), (self.FEN, 6, 0), (self.FEN, 6, sf.NULL_MARGIN), - ("4k3/8/8/3p4/4P3/8/8/4K3 w - - 0 1", 6, sf.NULL_MARGIN), - ("4k3/8/8/8/8/8/8/Q3K3 w - - 0 1", 6, sf.NULL_MARGIN), + (self.FEN, 7, 0), + (self.FEN, 7, sf.NULL_MARGIN), + ("4k3/8/8/3p4/4P3/8/8/4K3 w - - 0 1", 7, sf.NULL_MARGIN), + ("4k3/8/8/8/8/8/8/Q3K3 w - - 0 1", 7, sf.NULL_MARGIN), ) for fen, depth, offset in cases: pos = hist_from_fen(fen)[-1] pass_score = pos.score + offset pos, moves, seen = self.observed_depths(depth, pass_score, fen) - guard = depth >= 6 and abs(pos.score) < 750 and any(c in pos.board for c in "RBNQ") - hot = guard and pass_score >= pos.score + sf.NULL_MARGIN + calm = abs(pos.score) < 750 and any(c in pos.board for c in "RBNQ") + hot = calm and depth >= 6 and pass_score >= pos.score + sf.NULL_MARGIN + lmr = calm and depth >= 7 for move in moves: - expected = depth - hot - 1 - (guard and pos.value(move) < sf.LMR) + expected = depth - hot - 1 - (lmr and pos.value(move) < sf.LMR) assert {d for m, d in seen if m == move} == {expected} def test_root_moves_are_not_intrinsically_reduced(self): @@ -283,19 +286,19 @@ class TestShallowNullMateFloor: FEN = "2q1r3/4pR2/3rQ1pk/p1pnN2p/Pn5B/8/1P4PP/3R3K w - - 1 0" - def test_depth_eight_search_reports_mate(self): + def test_depth_nine_search_reports_mate(self): pos = hist_from_fen(self.FEN)[-1] result = None for depth, _, score, move in sf.Searcher().search([pos]): - if depth == 8: + if depth == 9: result = score, move - elif depth > 8: + elif depth > 9: break assert result is not None and result[0] >= sf.MATE_LOWER class TestStaticMoveCap: - """Ordinary depth-two and depth-three moves have a fixed static upper cap. + """Ordinary moves through depth four have a fixed static upper cap. A cap below the current window proves fail-low without a child search. Only a king capture bypasses it and retains the exact mate sentinel - @@ -306,11 +309,11 @@ def test_fail_low_caps_skip_all_starting_children(self): pos = sf.Position(sf.initial, 0, (True, True), (True, True), 0, 0) searcher = sf.Searcher() searcher.root, searcher.history = pos, set() - score = searcher.bound(pos, 200, 2, root=True) + score = searcher.bound(pos, 227, 2, root=True) caps = [min(sf.MATE_LOWER - 1, pos.score + pos.value(m) + sf.QS_A) for m in pos.gen_moves()] - assert score == max(caps) == 186 + assert score == max(caps) == 226 assert searcher.nodes == 1 def test_bk15_forcing_capture_recovers_above_cap_horizon(self): @@ -337,7 +340,7 @@ def observed(pos, gamma, depth, root=False): assert child not in calls - # A promotion at depth 2-3 is capped like anything else. #213 removed the + # A promotion at depths 2-4 is capped like anything else. #213 removed the # "and not move.prom" exemption the gate used to carry, and nothing in the # suite noticed: re-adding it leaves every other test green (mutation run, # 2026-08-17). It is a sound cap because pos.value(move) already adds @@ -348,7 +351,7 @@ def observed(pos, gamma, depth, root=False): PROM_FEN = "4k3/P7/8/8/8/8/8/R3K3 w - - 0 1" def test_promotion_uses_the_ordinary_move_cap(self): - for depth in (2, 3): + for depth in (2, 3, 4): pos = hist_from_fen(self.PROM_FEN)[-1] searcher = sf.Searcher() searcher.root, searcher.history = pos, set() @@ -506,7 +509,7 @@ class TestMateDistance: The position below is the complaint in miniature: three mating moves and eight moves that mate in three, all scoring exactly 47923 on master, and 47998 vs 47938 at depth 6 here. The finite move cap can keep - a proof below the mate band at depths two and three; these guarantees + a proof below the mate band at depths two through four; these guarantees begin once the proof has moved above that frontier.""" FEN = "8/3Q4/8/8/8/3R4/5K1k/8 w - - 0 1" @@ -519,7 +522,7 @@ def yield_of(self, hist, uci_move, depth): searcher = sf.Searcher() return -searcher.bound(child, -sf.MATE_LOWER, depth - 1, root=True) - @pytest.mark.parametrize("depth", [6, 7, 8]) + @pytest.mark.parametrize("depth", [7, 8, 9]) def test_faster_mate_scores_strictly_better(self, depth): hist = hist_from_fen(self.FEN) fast = [self.yield_of(hist, m, depth) for m in self.FAST] @@ -535,7 +538,7 @@ def test_faster_mate_scores_strictly_better(self, depth): f"same distance, different score: {fast} / {slow}" ) - @pytest.mark.parametrize("depth", [4, 5, 6, 7, 8, 9, 10]) + @pytest.mark.parametrize("depth", [5, 6, 7, 8, 9, 10]) def test_mate_in_one_score_carries_the_distance(self, depth): # Ra8# from a bare-rook mate: the score is the band floor plus the # depth the search still had in hand. diff --git a/tests/test_terminal_bench.py b/tests/test_terminal_bench.py index f3458f94..50af0990 100644 --- a/tests/test_terminal_bench.py +++ b/tests/test_terminal_bench.py @@ -114,10 +114,10 @@ def test_terminal_invariants(parts, cls): up = min(up, score) brackets[depth] = (lo, up) last = depth - if depth > 4 or s.nodes > 250_000: + if depth > 5 or s.nodes > 250_000: break assert not any(e.lower > e.upper for e in s.tp_score.values()), "driver crossing" - lo, up = brackets.get(min(last, 4), brackets[last]) + lo, up = brackets.get(min(last, 5), brackets[last]) root_move = s.tp_move.get(pos) if root_move is not None: board = chess.Board(" ".join(parts[:4]) + " 0 1") diff --git a/tools/ctwin/sunfish.c b/tools/ctwin/sunfish.c index 3388cef4..4895aa10 100644 --- a/tools/ctwin/sunfish.c +++ b/tools/ctwin/sunfish.c @@ -72,10 +72,10 @@ static int MATE_LOWER, MATE_UPPER; static int tables_loaded = 0; /* Runtime knobs. Defaults reproduce sunfish.py at the repo root. */ -static int QS = 40; -static int QS_A = 140; -static int LMR = 75; -static int LMR_MIN_DEPTH = 6, LMR_RED = 1, LMR_LIMIT = 750; +static int QS = 36; +static int QS_A = 180; +static int LMR = 70; +static int LMR_MIN_DEPTH = 7, LMR_RED = 1, LMR_LIMIT = 750; static int EVAL_ROUGHNESS = 15; static int NULL_CAP_MARGIN = 15; /* independent lab version of Python's shared value */ static int VALUE_N = 280, VALUE_B = 320, VALUE_R = 479, VALUE_Q = 929; @@ -92,7 +92,7 @@ static int IID = 0, IID_MIN_DEPTH = 3; /* deleted Python IID, retained for tuni static int IID_RED = 3; /* IID depth reduction */ static int FUT_MAX = 1; /* futility pruning when depth <= this */ static int FUT_CAP = 1; /* 0 off, 1 ordinary moves, 2 negative value */ -static int FUT_CAP_DEPTH = 3; +static int FUT_CAP_DEPTH = 4; static int MATE_DIST = 1; /* mate scores carry distance (master: 0) */ /* Replacement-policy battery knobs (tp_move only; tp_score untouched). * EVICT_POLICY 0: master/branch root-guarded FIFO insert-then-evict (>). diff --git a/tools/quick_tests.sh b/tools/quick_tests.sh index bcff7775..fa124865 100755 --- a/tools/quick_tests.sh +++ b/tools/quick_tests.sh @@ -8,15 +8,15 @@ T="python3 $TOOLS/tester.py" echo "Terminal and eventual-mate correctness..." # Every real edge costs at most C=3 plies, and the shallow cap blocks any -# mate report below nominal depth 4, so a k-ply mate proof is armed at -# D >= 3k+1 -- ci_code_mate_in_{1,2,3} in formal/Sunfish/MateDepth.lean (#214). +# mate report below nominal depth 5, so a k-ply mate proof is armed at +# D >= 3k+2 -- ci_code_mate_in_{1,2,3} in formal/Sunfish/MateDepth.lean. # mate-in-n has k = 2n-1. These are the PROVED depths, so the suite is a # depth regression detector, not a round number: measured first success is -# 4/7/15, leaving 0/3/1 plies of margin. +# 4/7/15, leaving 1/4/2 plies of margin. $T "$1" ${2:-"--quiet"} draw $TESTF/stalemate0.fen --depth 1 --floor 4 -$T "$1" ${2:-"--quiet"} mate $TESTF/mate1.fen --depth 4 --floor 8 -$T "$1" ${2:-"--quiet"} mate $TESTF/mate2_eventual.fen --depth 10 --floor 5 -$T "$1" ${2:-"--quiet"} mate $TESTF/mate3_eventual.fen --depth 16 --floor 2 +$T "$1" ${2:-"--quiet"} mate $TESTF/mate1.fen --depth 5 --floor 8 +$T "$1" ${2:-"--quiet"} mate $TESTF/mate2_eventual.fen --depth 11 --floor 5 +$T "$1" ${2:-"--quiet"} mate $TESTF/mate3_eventual.fen --depth 17 --floor 2 echo echo "Tactical strength regressions..."