diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5aa513e..56dc713 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -33,9 +33,21 @@ jobs: - uses: actions/checkout@v4 - uses: dtolnay/rust-toolchain@stable - uses: Swatinem/rust-cache@v2 - # benchmark_proof brute-force cases skip gracefully without masterdata. + # External masterdata proofs are explicitly ignored, not counted as passes. - run: cargo test --all-features + exactness: + name: exhaustive search matrices + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: dtolnay/rust-toolchain@stable + - uses: Swatinem/rust-cache@v2 + - run: cargo test --locked --release --all-features --lib long_exact_all_scene_property_matrix -- --ignored --nocapture --test-threads=1 + - run: cargo test --locked --release --all-features --lib validation_oracle_extended -- --ignored --nocapture --test-threads=1 + env: + ALLIUM_VALIDATION_ORACLE_SEEDS: 16 + msrv: name: msrv (1.89) runs-on: ubuntu-latest diff --git a/docs/exactness-proof.md b/docs/exactness-proof.md index 884a839..40584be 100644 --- a/docs/exactness-proof.md +++ b/docs/exactness-proof.md @@ -98,11 +98,14 @@ Top-K set, and the best canonical representative is retained. The public `compare_deck_results` wrapper exposes this same order for aggregation paths; callers must not replace it with a score-only comparator. -Numeric branch-and-bound thresholds deliberately ignore later tie-break fields. -For maximizing searches, a branch is discarded only when its admissible upper -bound is strictly below the current K-th score. Equality is retained, including -the SIMD mask. For minimization, the dual rule discards only when the -admissible lower bound is strictly above the K-th value. +A numeric-only branch-and-bound test deliberately ignores later tie-break +fields: maximizing searches discard a branch only when its admissible upper +bound is strictly below the K-th score; minimization uses a lower bound +strictly above it. Equality survives these tests, including the SIMD mask. +The Power/Skill specializations may additionally reject equality when a proved +lower bound on the public-set key is strictly worse than the K-th set +(pruning-proof Sections 20.5 and 21.2). Their smallest-ID frontiers carry an +explicit occupied length: public ID 65535 is a value, never an empty slot. This strict relation is required even when K incumbents already exist: an equal-objective branch may contain a distinct public set or a canonically better @@ -207,8 +210,10 @@ every completion-relevant condition represented by the mode: - attribute and unit-membership semantics needed by the remaining deck are identical; - fixed public identities are never removed; -- for World Bloom, worst-case support-deck displacement is bounded and any - deficit is paid for by guaranteed base event-bonus surplus; +- for World Bloom, sorted support order statistics must not decrease, or the + guaranteed base surplus must exceed the outward-bounded support loss by + more than the proved two-deck floating-point error; equality over the reals + alone never authorizes compensation (pruning-proof Theorems 3a–3b); - for Final member-only dominance, leader-only numeric benefits are excluded from the comparison and the appropriate leader support profile is used. @@ -226,9 +231,14 @@ card by its surviving dominance root to obtain D'. By substitutability, objective(D') >= objective(D), -and when objectives tie, D' is not canonically worse. If D belongs to the true -Top-K, D' is therefore at or above the K-th threshold in the compacted pool. -Production search discovers the root set. Post-search substitution expansion +and when objectives tie, D' is not canonically worse. If K distinct compacted +public sets preceded the best compacted representative of D', their full-pool +representatives would also precede D, contradicting its true Top-K rank. Thus +the root set is retained. This is a full-order counting argument, not merely a +comparison with a numeric threshold. Production search discovers the root set. +Before inverse-score pruning, reconstruction enumerates every original +cultivation realization of a retained public set; the best realization can +change after another card is substituted. Post-search substitution expansion walks the inverse dominance chains, re-evaluates every substituted deck exactly, and merges legal distinct public sets through the canonical tracker. Multi-slot substitutions are recursive, so chains involving more than one dominated card @@ -335,8 +345,12 @@ bonus: the logarithm of the event-point ceiling of every deck that can reach the threshold is at most an affine function of its aggregate features (pruning-proof Section 18.8). Each group is weighted by its best card under that function, and a node is pruned when the sum of the weights it can still -reach is below the logarithm of the threshold's event point. Like the other -tests it only discards subtrees without a deck at or above the threshold. +reach is below the logarithm of the threshold's event point. All model preparation, logarithms, weights, +sums and threshold subtraction have outward interval bounds. Logarithms use +an atanh series with an explicit remainder, not a platform `ln` error +assumption. An uncertifiable near-degenerate chord falls back to the independent +bound. Like the other tests it only discards subtrees without a deck at or +above the threshold. ### 5.3 Support-deck upper bound @@ -543,7 +557,10 @@ same resolved skill tables / semantics used by evaluation. A bound may relax correlations upward, but it may not silently change numeric precision in a way that can underestimate a legal completion. -The floating-point side of these invariants is proved in +Cross-deck support compensation and the log-linear optimization have separate +floating-point proofs in pruning-proof Sections 5 and 18.8; neither follows +merely from a real-valued inequality. The aggregate floating-point invariants +are proved in [pruning-proof.md, Section 29](pruning-proof.md#29-numeric-admissibility): every integer or fixed-point ceiling dominates the `f64` leaf evaluator after its truncations, because the ceilings' integer grids are coarser than the @@ -584,6 +601,10 @@ state. ## 15. Verification evidence and what each class proves +The [2026-09-26 audit and repairs](proof-audit-20260926.md) records concrete +wrong-result counterexamples, their regression tests, and the distinction +between repaired proof obligations and empirical release evidence. + The runnable matrix and evidence boundaries are documented in [search-validation.md](search-validation.md). Final Top-K reconstruction must keep a forced leader in the concrete first slot: event bonuses and support diff --git a/docs/proof-audit-20260926.md b/docs/proof-audit-20260926.md new file mode 100644 index 0000000..a2c9ffb --- /dev/null +++ b/docs/proof-audit-20260926.md @@ -0,0 +1,141 @@ +# Proof audit: 2026-09-26 + +Base audited: `165ff63525be2c13d4ae9b6417924e0b789e5ff6`. + +This review compares the implementation with `exactness-proof.md` and +`pruning-proof.md`. It does not change the leaf evaluator to make search +counterexamples disappear. The two reproduced wrong-result cases are distinct +from arithmetic hazards and incomplete arguments found during the repair. + +## Reproduced wrong results + +### Floating-point support compensation + +Six cards give two possible public sets. Cards 100 and 200 have the same +character, attribute, unit mask, power (90,000 in every context) and skill (100). +Their base bonuses are 64.1% and 62.5%; four other characters have no bonus. +The support profile, count 4, is: + +```text +(100, 7.05), (200, 5.45), (300, 2.05), (301, 0.8), (302, 0.5) +``` + +Over the reals both choices total 72.9%. The unchanged evaluator produces +72.89999999999999147 and 72.90000000000000568, and MYSEKAI values 1728 and +1729. In Final Chapter with character 2 fixed as leader, the old dominance +predicate deleted card 200 and returned `Complete` with 1728. The exhaustive +ordered oracle and dominance-disabled search returned 1729. + +Repair: support order-statistic monotonicity handles the no-loss case; a +positive loss requires a strict outward-certified surplus exceeding the +proved two-deck floating error. Malformed profiles cannot certify deletion. +See pruning-proof Theorems 3a and 3b. The inverse substitution theorem now +inherits preservation of the implemented objective, not just a real formula. + +Permanent tests: `proof_audit::support_compensation_preserves_actual_floating_point_top_one`, +`strict_support_surplus_still_allows_certified_dominance`, and malformed-profile +regressions. The first also exercises K > 1, ordinary WL and other targets. + +### Public ID 65535 is not an empty slot + +The eight `(public ID, power)` rows are: + +```text +(101,107), (106,107), (104,105), (102,109), +(107,108), (105,101), (103,110), (65535,105) +``` + +They have distinct characters and identical composition contexts. Power K=20 +previously returned `Complete`, with rank 20 equal to +`534 / [101,103,104,106,65535]` instead of the canonical +`534 / [101,102,104,107,65535]`. + +Repair: both Power and generic numeric ID frontiers use `SmallestIds` with an +explicit occupied length. Every `u16` remains representable. No new candidate +filter or reduced public-ID range is introduced. + +Permanent tests include the exact failing box, deterministic tied boxes, +Power/Skill/MYSEKAI, constrained Power, minimization, and the builder's acceptance +of public ID 65535. See pruning-proof Sections 3.3, 20.5 and 21.2. + +## Additional repair obligations + +| Area | Defect or missing argument | Repair | +| --- | --- | --- | +| Log-linear bound | A fixed epsilon and a few-ulp claim do not certify a ratio of nearly equal logarithms | Outward interval preparation, an explicit atanh-series logarithm remainder, certified endpoint widening, and fallback for an uncertifiable chord | +| Log-bound consumers | Ordinary sums and last-group subtraction also need an error argument | Products/sums upward; threshold logarithm and threshold-minus-fixed terms downward at every consumer | +| Event cutoff inversion | Probe values can exceed legal-leaf maxima; narrowing event stages could wrap | Shared `i128` stages and a final monotone clip above every supported leaf output | +| Optional joint bound | Large coefficient/rational intermediates are not covered merely by bounded final scores | Checked coefficient/product/denominator operations; decline or return an infinite ceiling on overflow | +| Support-only identity | A card excluded from the main pool could still have its support ID clamped before deduplication | Checked conversion before constructing support seeds, including the standalone support operation | +| Raw character identity | A malformed character could be skipped before the later representation check | Validate before the unit-mask preparation filter | +| Root recovery proof | Numeric threshold alone does not establish membership in canonical Top-K | Full-order counting argument and explicit cultivation enumeration before inverse-score pruning | +| Floating operation count | Reference shares are not generally quarter-integral; Multi Average adds another dependency chain | Count the whole dependency path conservatively and distinguish loose bounds from legal-leaf maxima | +| Evidence reporting | Missing external data returned from tests as if successful | Explicit ignored tests; an explicit invocation without prerequisites fails | + +The log-linear analytic derivation remains in Section 18.8. Its machine +arithmetic now follows that derivation using interval enclosures. No platform +`ln` accuracy assumption or heuristic epsilon authorizes pruning. No claim of a +third end-to-end wrong-result counterexample is made for the old log bound. + +## Verification + +The core patch was checked on native x86-64, Rust 1.98.1, one pinned logical +CPU with an 80% quota and a 1536 MiB memory limit, without swap: + +```sh +cargo fmt --all --check +cargo clippy --locked --all-features --all-targets -- -D warnings +cargo test --locked --release --all-features +cargo test --locked --release --all-features --lib \ + long_exact_all_scene_property_matrix -- --ignored --nocapture --test-threads=1 +ALLIUM_VALIDATION_ORACLE_SEEDS=16 cargo test --locked --release --all-features \ + --lib validation_oracle_extended -- --ignored --nocapture --test-threads=1 +``` + +The native unit suite passes 308 tests with 8 explicitly ignored. The default +integration suite runs its corpus-classification test and explicitly ignores +three external-masterdata proofs; one doctest passes. The all-scene matrix +passes 256 cases / 3840 comparisons. The 16-seed extended matrix passes 4608 +contexts, 18,432 complete searches, 13,765,632 ordered assignments and 287,232 +compared rows (oracle digest `6c7ca192360864cb`). + +Additional checks on the same implementation: + +- the separate Server workspace passes 13 unit tests and 13 HTTP/engine parity + tests locally; hosted CI also passes its release tests and default/jemalloc/ + mimalloc lint configurations; +- hosted CI passes `cargo check --all-features --locked` on Rust 1.89; +- a real `wasm32-unknown-unknown` release module builds with Rust 1.94.0 and + version-matched wasm-bindgen 0.2.126 bindings; +- Node 22.17.0 executes nine synthetic cases, each three times, matching 288 + result rows against the native CLI. Cases cover Power, Power minimization, + Skill, Solo Average Score, Auto Score, Multi event Score, Cheerful Score, + MYSEKAI and Bonus. The comparison retains integer objective keys as decimal + strings, and compares order, power, skill and cultivation fields as well as + completion. Inputs include a legal public ID 65535; +- the native build of `wasm/` contains zero tests and is **not** counted as + execution of the WebAssembly module. + +The runtime fixture is derived solely from `server/fixtures/synthetic.rs`: +its full masterdata is retained while the account is restricted to eight +characters, with one public card identity changed consistently to 65535. +These are nine inputs, not 27 independent inputs. This smoke check does not +replace Final/WL coverage or a real-browser release gate. The PR records +hosted check status separately from these local results. + +The ordinary PR/push CI now executes both exhaustive synthetic matrices. +`ExactOracle` independently enumerates placements and canonical public sets, +but shares the leaf evaluator. It proves search equivalence only on the tested +finite boxes, not independent correctness of the game's scoring rules. + +## Scope + +The low-level search theorem assumes a pool and context preserving the handler's +numeric, representation, support-order and alignment invariants. It is not a +promise for arbitrary invalid mutations of `SearchContext`. + +This review repairs the counterexamples and the identified proof obligations; +it is not a machine-checked whole-program proof or a claim that no other bug +exists. No real-account corpus, production-tail latency, or real-browser +release acceptance is inferred from synthetic/native tests. In particular, +this correctness change does not certify a 20 ms performance target. diff --git a/docs/pruning-proof.md b/docs/pruning-proof.md index dad2b5c..dfd0f48 100644 --- a/docs/pruning-proof.md +++ b/docs/pruning-proof.md @@ -80,9 +80,11 @@ A branch with $U(N)=\tau$ cannot be discarded from the numeric bound alone. It may contain a distinct public card set, a better legal placement, or a better deterministic cultivation representative with the same primary objective. -This is why all maximizing comparisons in the exact path use strict -upper < threshold, and why the SIMD candidate mask retains -upper >= threshold. +This is why a **numeric-only** maximizing comparison uses strict +upper < threshold and the SIMD candidate mask retains upper >= threshold. +Equality may be pruned only with an additional proved lower bound on the +canonical public-set key (Sections 20.5 and 21.2), not from the numeric +bound alone. ### Lemma 1 — tighter admissible bounds stay admissible @@ -189,8 +191,24 @@ the dense `CardIdx` cannot represent the pool and the builder returns There is deliberately no theorem that “the best 512 are enough”; no such truncation exists in the exact path. +The public card-ID domain includes every `u16`, including 65535; its upper +endpoint is not a missing-card sentinel. `SmallestIds` stores a separate +occupied length and inserts only into its occupied prefix. By induction, +that prefix is exactly the smallest distinct IDs seen so far, limited by its +capacity. The Power and numeric equality bounds read only that prefix, so +“too few remaining IDs” cannot be inferred from a legal ID's value. This is +a representation obligation of their lexicographic lower-bound proofs. + +Support candidates are prepared before the main-deck hard filters. Their +public IDs are checked **before** narrowing and deduplication even if the main +pool later excludes the card; a support-only ID cannot alias 65535 by clamping. +The standalone support-card operation uses the same checked conversion. Raw +negative or out-of-range character identities likewise return explicit errors +rather than being clamped before validation. + Implementation: -src/handler/build.rs, src/handler/filter.rs, src/handler/capacity.rs. +src/handler/build.rs, src/handler/filter.rs, src/handler/capacity.rs, +src/handler/world_bloom.rs. ## 4. Same-character dominance @@ -206,7 +224,9 @@ The implementation requires all of the following: 2. skill type and all completion-observable skill semantics are substitutable, including skill_min, skill_max, unit-count / different-unit / reference tables; -3. required training-state semantics are equal; +3. training-dependent effects have already been resolved into the compared + power/skill/bonus columns; the leaf evaluator does not read a separate raw + training-state flag; 4. base and limited event bonus of $A$ are componentwise no worse; 5. limited-bonus zero/nonzero class is preserved when the event has a count cap; 6. attributes are equal; @@ -243,37 +263,89 @@ backward in the deterministic tie order. ∎ ## 5. World Bloom support-aware dominance A World Bloom main-deck card may also occupy a support-deck position. Replacing -a main card can therefore change support opportunity cost. +a main card can therefore change support opportunity cost. `SupportDimension` +checks every profile it uses: entries must be sorted by non-increasing finite, +non-negative bonus, with one entry per public ID. A malformed profile produces +an unusable dimension, **not** the absence of a support penalty; no dominance +pair is approved from it. Cultivation variants of one ID share its entry. + +Fix a leader profile with $q>0$ counted support slots. Let $R$ be the other +four main cards, and let $a,b$ be the stored `f64` support values of replacement +$A$ and removed card $B$, interpreted as exact real numbers (zero if absent). +For distinct IDs let $t$ be the $q$-th value after excluding $R,A,B$, padded +with zero. In exact arithmetic the support loss on replacing $B$ by $A$ is + +$$ +(a-t)^+-(b-t)^+ \le \Delta=\max(0,a-\max(b,f)), +$$ + +where $f$ is the value at one-based rank $q+5$ in the original profile (zero +past the end). If $b\ge f$, the loss is at most $(a-b)^+$ for every $t$. +If $b2^{-20}. +$$ -### Theorem 3 — World Bloom substitution +Each endpoint rounds outward, including the subtraction. Therefore the real +total improves by more than $2^{-20}$, exceeding the two-deck rounding error +by a factor of at least four. The implemented total cannot decrease. +Limited bonus is not used as payment, since its cap may omit it. Every possible +leader profile must pass Theorem 3a or 3b. The other substitution dimensions +of Theorem 2 then establish objective and canonical-order preservation. ∎ -When support_deficit_affordable succeeds, the combined -main-deck-bonus + support-deck contribution after replacing $B$ with $A$ -cannot decrease. Together with Theorem 2, $A$ is a valid substitute for every -legal completion containing $B$. ∎ +The permanent `proof_audit::support_compensation_preserves_actual_floating_point_top_one` +regression records the equal-real-total counterexample: 64.1 + 8.8 and +62.5 + 10.4 produce MYSEKAI scores 1728 and 1729 respectively in the unchanged +evaluator. The weaker candidate must survive, including Top-1 where alternatives +are not expanded. A separate strict-surplus regression confirms that safe +compensation remains enabled. ## 6. Top-K recovery after dominance @@ -284,7 +356,7 @@ Implementation: src/search/alternatives.rs. Let $D$ be any true Top-K deck containing one or more dominated cards. Replace each dominated card by its surviving dominance root, obtaining $R(D)$. -By Theorems 2 and 3, +By Theorem 2 and Theorems 3a–3b, $$ v(R(D)) \ge v(D), @@ -292,10 +364,23 @@ $$ and an equal primary objective is not canonically worsened by the replacement. -If $D$ is in the true Top-K, $v(D)\ge\tau^*$, where $\tau^*$ is the true -K-th primary value. Therefore $R(D)$ is at or above the same threshold and -must be represented among the compacted search's K best public sets, modulo -deduplication of roots. +Use the **full canonical order**, not just a numeric threshold. Let $D$ be +the best representative of a true Top-K public set and let $R(D)$ be its legal +root arrangement. The substitution theorems give $R(D)\preceq D$. The best +representative of the root set in the compacted pool is no worse than $R(D)$. +If K distinct compacted public sets preceded that representative, those same +K sets, with their possibly better full-pool representatives, would precede +$D$ in the full feasible set, contradicting $D$'s rank. Hence the root set is +retained by the compacted Top-K. This counting argument covers objective ties +and many-to-one root mappings without assuming that a numeric threshold alone +selects a canonical Top-K. + +A retained public set can have several cultivation realizations whose best +choice changes after substitution. The implementation enumerates its original +cultivation combinations **before** any alternative-score pruning. Each +realization is evaluated independently; scores of different realizations are +not monotone bounds on one another. Inverse-edge pruning is applied only after +this enumeration has fixed a concrete realization. The post-search alternatives pass recursively substitutes every recorded inverse dominance edge back into every slot and exact-evaluates the result. @@ -744,7 +829,7 @@ for every deck with $E\ge\tau$. The coefficients are non-negative and the five cards have distinct characters, so the right side is at most $K+a_B\epsilon$ plus the largest, over characters $x$, of the best leader term of a card of $x$ that may lead and the four largest per-character maxima of $w_c$ over the -other characters. When that value is below $\ln\tau-10^{-9}$, no deck of $R$ +other characters. When that upward-rounded value is below the certified lower endpoint for $\ln\tau$, no deck of $R$ has an event point of $\tau$ or more, so every deck of $R$ is below the cutoff, and the regime is skipped. The sum has fewer than twenty terms, so the numerics of Section 18.8 apply. A same-character search makes no such test. @@ -1252,7 +1337,11 @@ $C\ge 2\beta W$, and $C^2/(4\alpha\beta)$ otherwise. The search keeps that peak as an exact rational, adds $c_0$ times its denominator, divides by the denominator times $d\,10^6$ with floor, and takes the smaller of this and the separate-maxima ceiling as the branch ceiling. The weights only decide -which of the two is smaller. A regime takes the normal of the level curve of +which of the two is smaller. The potentially large rational products and +final numerator/denominator use checked arithmetic. Overflow returns +`u32::MAX`, so taking the smaller with the separate-maxima bound falls back +to that already-proved bound instead of interpreting wrapped arithmetic as a +small ceiling. An unrepresentable `LiveProduct` disables this optional component. A regime takes the normal of the level curve of $uw$ at its unconditioned ceiling, $\omega_S/\omega_P\approx bU/W$, and keeps the component only when every card's joint value is below $2^{26}$, so five of them fit the table and an unreachable entry stays negative. A class test @@ -1474,7 +1563,7 @@ slots. The comparison is performed in a member context that removes leader-only numeric benefits but preserves the card's real skill/training semantics and World Bloom support opportunity cost. -Therefore Theorems 2 and 3 apply to **member positions**: replacing a dominated +Therefore Theorem 2 and Theorems 3a–3b apply to **member positions**: replacing a dominated member by its root cannot worsen a completion in any dimension visible to that member role. The relation is never used to assert that the dominated card is also safe to remove as a leader. @@ -1505,7 +1594,8 @@ event point of `ObjectiveBound::ceiling` at these features, which bounds the event point of the deck by Section 18.5 and Section 29. **Lemma LL1 (product form).** Let $h$ be the honor bonus, $m$ and $\beta$ the -music and boost rates in percent, $\kappa=m\beta/10^6$, and +music and boost rates in percent, $\kappa\ge m\beta/10^6$ the upward-prepared +coefficient, and $(c,D)=(100,20000)$ for Solo and Auto, $(110+o,17000)$ for Multi, where $o=13$ when the opponent score is zero and $\min(\lfloor\text{other}/340000\rfloor,13)$ otherwise. Then @@ -1516,8 +1606,10 @@ $$ where $q(S,L)=(4\bar r(S,L)+a)/10^6$, $a$ is the active-score coefficient per unit power (five times $0.075\cdot10^6$ without a teammate power, once with -one), $c'=c+4\cdot0.075\,t/D$ for teammate power $t$ ($c'=c$ otherwise), and -$\bar r$ bounds the fixed-point live rate of Section 12: +one), $c'$ an upward-prepared bound on $c+4\cdot0.075\,t/D$ for teammate power $t$ +(on $c$ otherwise), and $\bar r$ bounds the fixed-point live rate of Section 12. +The following coefficients and intercepts are prepared upward; their stored +`f64` values define an exact-real majorant of the listed expressions: - Multi: $\max(4L+S,T)\rho\le(4L+S)\rho+\max(0,T-4L_{\min})\rho$ over leaders with skill at least $L_{\min}$, where $T$ is five times the teammate @@ -1549,7 +1641,7 @@ $\square$ **Lemma LL3 (affine bound).** Suppose $00$ and $Q_0=\ell(S_0,\hat L)>0$ for +$L\in[L_{\min},\hat L]$, and let $P_0>0$, $B_0\ge0$ and $Q_0=\ell(S_0,\hat L)>0$ for some $S_0$. Every deck of Lemma LL2 with $E\ge\tau_0$ satisfies $$ @@ -1597,7 +1689,8 @@ weights of distinct characters from the suffix start, and $a_B$ times the attribute and support bound of Section 18.3. A card-level node sums the terms of the chosen cards, the weights of the remaining planned groups and $a_B$ times the plan's diversity bonus and the current support ceiling. If -the sum is below $\ln\tau-10^{-9}$, where $\tau\ge\tau_0$ is the event point +the upward-rounded sum is below a certified lower endpoint for $\ln\tau$, +where $\tau\ge\tau_0$ is the event point of the current threshold, no deck of the subtree has $E\ge\tau$, so every leaf of the subtree is below the threshold and the subtree is pruned by Theorem 1. @@ -1616,33 +1709,79 @@ the suffix lists and attribute rows only shrink as the start index grows. The scan of a group stops when the rest maxima of Section 18.5 fail it, since the weight is non-decreasing in every term. -In the last member slot, let $F$ be $\ln\tau-10^{-9}$ less the leader's +In the last member slot, let $F$ be a certified lower endpoint for $\ln\tau$ less the leader's terms, the weights of the three selected groups and $a_B$ times the attribute and support bound of the suffix from the slot's first group. That bound is at least the one of every attribute union a group of the suffix completes, so a group whose weight is below $F$ fails the test of the four groups, and the scan moves to the next group whose weight reaches $F$; blocks of sixteen -groups whose largest weight is below $F$ are passed over whole. $F$ is -recomputed whenever the threshold changes. The comparison rearranges the sum -of the four-group test, which changes its rounding by far less than the -margin. A bound built for $\tau_0$ holds at +groups whose largest weight is below $F$ are passed over whole. The fixed +terms are summed upward and their subtraction from the cutoff is rounded +downward, so the stored $F$ is a lower bound on the weight needed. $F$ is +recomputed whenever the threshold changes. This rearrangement therefore has +an explicit directed-rounding proof, not an assumed small-error margin. A bound built for $\tau_0$ holds at every higher threshold, so the search rebuilds the weights only when the event-point threshold has risen by $1/128$ since the last build, which narrows the chord and moves the tangent point; every sum is recomputed from the current weights, never mixed across builds. When $u_{\mathrm{lo}}\le0$ or $u_{\mathrm{lo}}\ge u_{\mathrm{hi}}$ no log-linear test is made. -*Numerics.* The parameters $P_0$, $Q_0$, $B_0$ and $\sigma$ are `f64` -numbers, and Lemma LL3 holds for their exact values, except that $\sigma$, -$\varphi(t_{\mathrm{lo}})$ and the logarithms in $K$ carry an error of a few -units in the last place. The search uses a bound only when $\lambda\ge2^{-10}$, -so each weighted term $a_PP$, $a_SS$, $a_LL$ and $a_BB$ is at most $2^{10}$ -($P_0$, $Q_0$ and $100+B_0$ are at least $\lambda$ times the box values), -and only when $|K|<2^8$. A sum of fewer than twenty such terms in -`f64` therefore has an absolute error below $10^{-11}$, which together with -the parameter errors stays far below the margin of $10^{-9}$. -`log_linear::tests` checks the bound against `ObjectiveBound::ceiling` at -random feature points for every supported live type and skill order. +**Certified binary64 preparation and application.** The implementation does +not assume a fixed ulp accuracy for the platform `ln`, nor that the ratio of +two tiny logarithms has a small error. In `log_linear/interval.rs`, every +addition, subtraction, multiplication and division encloses its exact real +result by rounding endpoint operations outward with `next_down` / `next_up`. +Products and quotients take all four endpoint combinations; division through +zero is unavailable. Non-finite intermediate intervals cannot produce a bound. +Induction on the expression tree proves containment, including negative +intercepts and cancellation in the constant term. + +For logarithms, every positive finite binary64 value has the exact reduction +$x=2^e m$, $1\le m<2$. Subnormal values are first scaled exactly by $2^{52}$. +For $z=(m-1)/(m+1)\in[0,1/3]$, + +$$ +\ln m=2\sum_{j=0}^{31}\frac{z^{2j+1}}{2j+1}+R,\qquad +0\le R\le\frac{2z^{65}}{65(1-z^2)}. +$$ + +The identity follows by integrating the geometric series of $1/(1-z^2)$. +Every omitted denominator is at least 65, which proves the geometric remainder +bound. Both the finite sum and remainder are evaluated as outward intervals. +$\ln2$ is computed by the same series at $m=2$, cached, and multiplied by the +signed exact exponent using interval multiplication. Monotonicity of $\ln$ +extends this point procedure to an interval argument. Thus **no transcendental +library call** is trusted by a pruning decision. + +The calculated interval for $u_{lo}$ contributes its lower endpoint, and that +for $u_{hi}$ its upper endpoint. This widens the chord's domain rather than +excluding feasible endpoint values. The true chord slope is enclosed using +interval logarithms and interval division; if the denominator interval reaches +zero, or the slope interval cannot be certified inside $(0,1)$, construction +returns `None`. Nearly coincident endpoints therefore fall back, rather than +turning a rounded slope of zero into a certificate. + +The tangent's segment is selected by comparing with exact integer breakpoints, +not by flooring a rounded quotient. Its intercept is calculated upward; hence +it remains a supergradient majorant even at a breakpoint. Bisection chooses +only the tangent point and has no authority to prune. For its stored positive +point coordinates the interval expression encloses the exact constant $K$ and +coefficients of Lemma LL3. Choosing each coefficient's upper endpoint is safe +because all aggregate features are non-negative. + +Application is outward too: card products, leader weights, selected-group and +suffix sums, and the regime-level maximum are upper bounds on the exact affine +value. The threshold is the lower endpoint of the interval logarithm. A strict +comparison of upper value with lower threshold proves exclusion. Last-group +subtraction is downward as described above. No fixed `1e-9` error budget is +needed, and widening an interval can only weaken pruning. Finite/positive +constructor guards and the existing tangent-point heuristics merely decline +an optional optimization; they never delete a candidate. + +Tests exercise the logarithm at binary64 extremes, the coincident-endpoint +fallback, affine admissibility against `ObjectiveBound`, and every existing +regime/Final oracle comparison. They are falsification attempts for this +analytic and directed-arithmetic proof, not its replacement. ## 19. Constrained Power bounds @@ -1992,7 +2131,9 @@ soon small public sets are found. of one character. A deck holds at most one of them, and each is searched, so the canonical representative of every public set is among the leaves. Nothing is truncated per character or per partial state: the only removals -are the three bounds above and the feasibility checks. +are the three numeric bounds, the separately proved canonical equality test, +and the feasibility checks. The equality test's ID frontier uses the explicit +occupied length of Section 3.3, including public ID 65535. ## 22. Challenge bound frontier @@ -2215,8 +2356,8 @@ real formulas. ### 29.1 Floating-point facts Let $u=2^{-53}$ and let $\mathrm{fl}$ denote round-to-nearest. Every operand -below is finite and non-negative, and nonzero magnitudes stay far above the -subnormal range. +below is finite and non-negative. The relative form below is used on normal +operations; the absolute-error extension for subnormals is included in N2. - **(F1) Relative error.** $\mathrm{fl}(x\circ y)=(x\circ y)(1+\delta)$ with $|\delta|\le u$ for $\circ\in\{+,\times,/\}$. A chain of $k$ such operations @@ -2231,7 +2372,8 @@ subnormal range. of $1/4$ well inside that range, are exact, and so are their sums while they stay in range. Decimal constants such as $0.1$, $1.1$ or $1.15$ are not. - **(F4) Truncation.** On non-negative values the evaluator's `as i32` / - `as u32` / `as u64` casts and `floor` are the floor function; on non-negative + `as u32` / `as u64` casts are floor within the represented range + (as ensured for legal leaves), and `floor` is the floor function; on non-negative integers the ceilings' integer `/` is the floor function. ### 29.2 Numeric domain @@ -2265,15 +2407,35 @@ skill base plus maximum at most the card's skill maximum) they establish: $\hat I=\hat b\,m(\hat B+100)/10^4\le2^{27}$, $\hat E=\hat I\lambda\beta/100\le2^{30}$. -Every argument passed to an aggregate ceiling is a sum of at most five -per-card maxima (power, skill, bonus ceilings) plus request constants, and the -skill-peak argument is a single card's skill value. Hence every ceiling value -evaluated for a request is at most the corresponding a priori quantity, and -(D2) also keeps every `i64` numerator product below $2^{63}$ and every `u32` -power sum below $2^{32}$. The limits keep a factor of at least 2 below the -thresholds at which the lemmas stop holding; real master data lies one to three -orders of magnitude inside them. A `SearchContext` constructed directly for the -search API is expected to satisfy the same domain. +These are a priori bounds on **legal leaves**, not on every relaxed state or +inverse-cutoff probe. A relaxation may reuse a selected card's maximum, and +`needed_live` probes the whole non-negative `i32` range. Neither is a legal +five-card selection, so its value need not stay below $\hat X$ or $\hat E$. + +For actual live-numerator relaxations, the skill sum is at most five card +maxima and the peak at most one maximum. A power relaxation is at most five +times $\hat P$, even when the same card is reused. With a power cap, it is +still at most five times the capped $\hat P$. Upward coefficient preparation +adds less than one to the full rate over the input widths: in Multi the +largest multiplier is $5(2^{31}-1)$, whose quantization contribution is less +than $5(2^{31}-1)/(2^{20}10^6)<0.011$; the other orders have much smaller +multipliers. Thus the numerator's represented live bound is less than +$5\hat X+20\hat P<2^{30}$ (including preparation rounding), well inside +`i32`, and its numerator and intermediate rate products fit `i64`. + +Event-bound stages instead use `i128` and clip their final result upward-domain +safely to `i32::MAX`. The legal event-point maximum remains below that clip, +so oversized probes cannot wrap and destroy monotonicity. Optional joint-bound +coefficient construction uses checked `i64` arithmetic; unrepresentable +coefficients disable only that bound. Its potentially large rational products, +constant addition and final denominator use checked `i128` operations and +return an infinite (`u32::MAX`) ceiling on overflow. + +A directly constructed low-level `SearchContext` must preserve the builder's +numeric and representation invariants, sorted non-negative support profiles, +and pool/context alignment. The public search API does not re-run the handler's +validation. Its completeness theorem is conditional on these preconditions, +not an assertion that arbitrary mutated contexts are valid. ### 29.3 Lemma N1 — fixed-point coefficients @@ -2298,10 +2460,13 @@ base rate is the same `f64` value on both sides. Hence the live numerator satisfies $$ -N\ge10^6X_B(1-u)^8, +N\ge10^6X_B(1-u)^8-2^{-880}, $$ where $X_B$ is the real-valued ceiling evaluated at the exact `f64` constants. +The negligible absolute term covers underflow in an intermediate rate division +before fixed-point scaling; it is zero when every contributing operation is +normal (see the absolute-error discussion in N2). The ceiling of a rounded product can lie below the real product: the constant $1.1$ is stored as $1.1+8.9\cdot10^{-17}$ and $\mathrm{fl}(1.1\cdot10^6)$ is @@ -2309,76 +2474,100 @@ exactly $1\,100\,000$, so $K/10^6X_e$. ∎ +**Proof.** The legal evaluator value satisfies $X_e<5\cdot2^{25}$ by D2 and N2. +If $N/10^6\ge5\cdot2^{25}$, the claim is immediate. Otherwise N1 and N2 give + +$$ +X_e\le(N/10^6)(1+u)^{32}(1-u)^{-8}+2^{-898} +\le N/10^6+41u\,N/10^6+2^{-898}, +$$ + +where $41u\,N/10^6+2^{-898}<7.7\cdot10^{-7}<10^{-6}$. Since $N$ is an integer, +$\lfloor N/10^6\rfloor+1\ge(N+1)/10^6>X_e$. This covers both tight and loose +relaxations without assuming that the relaxed value is a legal-leaf maximum. ∎ -The argument needs no extra margin in the code: the $10^{-6}$ grid of the -numerator is the margin. It fails only beyond $N/10^6\approx3.2\cdot10^8$; at -real magnitudes (live scores near $10^7$) the rounding uses less than 4% of one -grid step. Section 10 compares the same integer $N$, and the packed live -component takes $\lfloor N/10^6\rfloor<2^{31}$ without wrapping. +No extra epsilon is needed: the numerator's integer grid supplies the margin +in the small-bound case. Section 10 compares this same integer numerator. +The arithmetic range argument in Section 29.2 keeps the packed live component +inside `i32`; a larger optional rational bound falls back as stated there. ### 29.6 Theorem N4 — event-point stages Write $b$ for the integer event base score, $t$ for the evaluator's `f64` bonus and $T$ for the integer bonus handed to the ceiling, with $t\le T$ (Lemma N5). -1. *Base score.* $b$ is non-decreasing in the live score, and Theorem N3 makes - the ceiling's live score at least the evaluator's. For Multi/Cheerful the - evaluator's `(live as f64 / 17000.0) as i32` equals the integer quotient: - for $0\le\text{live}<2^{31}$ the real quotient is either an integer or at - least $1/17000$ away from one. The opponent term is the same integer - expression on both sides; for live scores below $2^{29}$ neither the - saturating `i32` nor the `i64` product by 4 saturates. -2. *First stage.* The evaluator computes - $I_e=\lfloor\mathrm{fl}(\mathrm{fl}(b\cdot\mathrm{fl}(m/100))\cdot\mathrm{fl}(\mathrm{fl}(t/100)+1))\rfloor$ - and the ceiling $I_B=\lfloor V_B\rfloor$ with $V_B=b_Bm(T+100)/10^4$. The - float value is at most $V_B(1+5.1u)$. $V_B$ is a multiple of $10^{-4}$, so - $V_B\le\lfloor V_B\rfloor+1-10^{-4}$ unless it is an integer. Therefore - $I_e\le I_B$ whenever $5.1u\,V_B<10^{-4}$, that is for - $V_B<1.7\cdot10^{11}$; (D4) gives $V_B\le2^{27}$. -3. *Cheerful life stage.* The evaluator's life factor is - $\mathrm{fl}(\mathrm{fl}(1.15)+q)$ where $q=\mathrm{fl}(\ell/5000)$ clamped to - $[\mathrm{fl}(0.1),\mathrm{fl}(0.2)]$. Because $\mathrm{fl}(0.1)$ and - $\mathrm{fl}(0.2)$ are exactly $\mathrm{fl}(500/5000)$ and - $\mathrm{fl}(1000/5000)$, $q=\mathrm{fl}(c/5000)$ with - $c=\mathrm{clamp}(\ell,500,1000)$, the ceiling's integer clamp, and the - factor is at most $(1+u)^2(5750+c)/5000$. The ceiling's stage - $\lfloor I_B(5750+c)/5000\rfloor$ lies on a $1/5000$ grid; with - $I_B\le2^{27}$ the float error $1.35\cdot3.1u\,I_B<10^{-7}$ stays far below - the grid step $2\cdot10^{-4}$. -4. *Boost stage.* $\lfloor W\beta/100\rfloor$ lies on a $1/100$ grid and the - float error is at most $2.1u\,\hat E<10^{-6}$. For the normalized boost - values, multiples of 100, the stage is exact. -5. *Range.* By (D4) every intermediate is below $2^{30}$, so the ceiling's - `i64 → i32` casts are lossless and the evaluator's casts do not saturate. +1. *Base score.* $b$ is non-decreasing in live score, and N3 makes the + bound's live score at least the evaluator's. For legal live scores, division + by 17000 has either an integer result or distance at least $1/17000$ from + an integer; its floating rounding cannot cross that distance. The wide + opponent-score product is at least the evaluator's saturating product, and + both apply the same cap of 13. Thus oversized probes remain conservative. +2. *First stage.* Write $V_B=b_Bm(T+100)/10^4$ and $I_B=\lfloor V_B\rfloor$. + The evaluator's pre-floor value is at most $V_B(1+5.1u)$, but D4 bounds + only its legal value, not an oversized $V_B$. If $V_B\ge2^{28}$, then + $I_B$ already exceeds every legal first-stage value. Otherwise the absolute + error is less than $5.1u2^{28}<10^{-4}$, the grid spacing of $V_B$, and the + same next-grid-point argument as N3 proves $I_e\le I_B$. +3. *Cheerful life stage.* Let $c=\mathrm{clamp}(\ell,500,1000)$. The real + life factor is $(5750+c)/5000$; the evaluator's factor is at most this times + $(1+u)^2$. If $I_B\ge2^{28}$, its life-adjusted result already dominates + every legal life-stage value from D4. Otherwise the floating error of + multiplication and factor preparation is below $1.35\cdot3.1u2^{28}$, + smaller than the $1/5000$ pre-floor grid. Hence the integer life stage is + an upper bound too. +4. *Boost stage.* If the exact bound $W_B\beta/100\ge2^{31}$, clipping to + `i32::MAX` is still above every legal output (D4, including its negligible + rounding). Below $2^{31}$, the multiplication/division error is less than + $2.1u2^{31}<10^{-6}$, smaller than the $1/100$ grid, so flooring preserves + the bound. Normalized integral boost factors are a simpler exact case. +5. *Range and inversion.* All bound stages above are `i128`: even an `i32` + live probe and full-width `u32` music, bonus and boost operands fit before + their divisions. Only the final upper bound is clipped, never wrapped. + A non-negative monotone expression remains monotone after floors and the + final clip. Therefore the full-domain gallop/bisection in `needed_live` + preserves its bracket, including probes above the legal-leaf domain. Challenge event points use the same integer expression on both sides, and a MySekai live has event point 0 on both sides. Component-wise dominance of event @@ -2422,8 +2611,9 @@ The Skill key is $\lfloor\mathrm{fl}(\mathrm{fl}(10v)+10^{-6})\rfloor$, where $v$ is the leader's score-up plus $0.2$ times each other score-up, added in ascending order. The exact $10v^*$ is at most the integer ceiling $2S+8L$. For $10v^*<10^5$ the float error, including that of a reference share and -its mean, is below $10^{-9}$, so the float value is below $10v^*+1$. A key -above $2S+8L$ would need a float value of at least $2S+8L+1>10v^*+1$; hence +its mean, is below $10^{-9}$. Adding the explicit $10^{-6}$ encoding offset +still leaves the float value below $10v^*+1$. A key +above $2S+8L$ would need a float value of at least $2S+8L+1\ge10v^*+1$; hence the key is at most $2S+8L$. ### 29.9 Lemma N7 — correlated bound @@ -2436,17 +2626,20 @@ $\mathrm{fl}(cQ)$ is below $5\cdot10^{-4}$, so each coefficient exceeds $cQ$ by at least $1-5\cdot10^{-4}$, and the plane's real live expression exceeds the exact-constant live score by at least $4P(1+S+L)(1-5\cdot10^{-4})/Q$. The Solo/Auto Average evaluator exceeds that live score by at most -$((1+u)^{12}-1)\cdot4P(4+(S+L)/100)$. The first is more than 180 times the -second for all $S,L\ge0$, so every plane dominates the floating-point value +$((1+u)^{32}-1)\cdot4P(4+(S+L)/100)+2^{-900}$. For $P\ge1$ the first is more than 60 times the +second for all $S,L\ge0$; for $P=0$ both live values are zero. Thus every plane dominates the floating-point value before its outward integer steps. The final `+1` in **quadratic** is not required by this argument. ### 29.10 Scope -Everything else in the search is integer arithmetic on exact discrete state. -Floating-point values enter a ceiling only through the aggregate objective -coefficients (N1–N4, N6), the correlated coefficients (N7), support sums -(N5) and the MySekai value (N5). A MySekai live has no live score: the +In addition to the exact discrete state, floating-point values enter the +aggregate objective coefficients (N1–N4, N6), correlated coefficients (N7), +support sums and MySekai value (N5), support substitution (Theorems 3a–3b), +and the certified log-linear preparation/application (Section 18.8). The last +two need their own arguments; N5 alone does not prove cross-deck compensated +substitution, and IEEE basic-operation error bounds alone do not prove a +platform logarithm's accuracy. A MySekai live has no live score: the evaluator and every live-score ceiling use 0 for it. Verification: src/search/tests/numeric_soundness.rs enumerates every deck of diff --git a/docs/search-validation.md b/docs/search-validation.md index e63b92e..8d6bc3b 100644 --- a/docs/search-validation.md +++ b/docs/search-validation.md @@ -14,6 +14,19 @@ complete ranking. Unsupported capacity and empty feasible inputs are reported separately. Repeating one request measures timing variability; it does not add another input to correctness coverage. +## Default and explicit evidence + +`cargo test --all-features` runs the permanent synthetic regressions, including +`proof_audit`, but not the three external-masterdata `benchmark_proof` tests. +Those are explicitly `ignored`; they must never appear as successful real-data +proofs when no corpus was loaded. Running them explicitly with `--ignored` +without their required masterdata, or running the issue #2 proof with too small +a candidate budget, fails instead of returning a misleading success. + +The PR/push `exactness` CI job also runs the 256-case all-scene matrix and the +16-seed WL/Final matrix. They remain bounded synthetic search-equivalence +checks, not independent validation of game formulas or production latency. + ## Exhaustive matrix ```sh diff --git a/src/handler/build.rs b/src/handler/build.rs index 314e5fa..1c7e4cb 100644 --- a/src/handler/build.rs +++ b/src/handler/build.rs @@ -228,6 +228,9 @@ impl<'a> PreparedPoolBuild<'a> { { return Ok(()); } + // A malformed identity is not an absent unit match. Validate the + // raw value before preparation can silently skip or narrow it. + super::capacity::character_id(master.character_id)?; if card_data.unit_mask == 0 { return Ok(()); } @@ -838,7 +841,7 @@ pub(super) fn build_card_pool_fully_prepared_internal( let intermediate = CardIntermediate { game_card_id: master.id, card_rarity_type: master.card_rarity_type, - character_id: master.character_id.clamp(0, u8::MAX as i32) as u8, + character_id: super::capacity::character_id(master.character_id)?, attr, unit_mask_raw, default_image, @@ -862,7 +865,7 @@ pub(super) fn build_card_pool_fully_prepared_internal( indexes, params.support_master_max, params.support_skill_max, - ); + )?; if support_seen.insert(seed.card_id) { support_seeds.push(seed); } diff --git a/src/handler/capacity.rs b/src/handler/capacity.rs index 989ad9b..67e6b74 100644 --- a/src/handler/capacity.rs +++ b/src/handler/capacity.rs @@ -10,8 +10,8 @@ pub(crate) const NUMERIC_POWER_MAX: u64 = 1 << 24; /// Largest a priori live-score rate `base + score_up * sum(rates) / 100`. pub(crate) const NUMERIC_RATE_MAX: u64 = 1 << 16; /// Largest a priori live-score ceiling. The fixed-point live bound dominates -/// the floating-point evaluator while `28 * 2^-53 * live < 10^-6`, that is for -/// live scores below about `3.2e8`. +/// the floating-point evaluator while `41 * 2^-53 * live < 10^-6` on the tight-bound case; looser +/// bounds dominate the separately bounded legal leaf value directly. pub(crate) const NUMERIC_LIVE_SCORE_MAX: u64 = 1 << 27; /// Largest a priori total event bonus, in percent. pub(crate) const NUMERIC_BONUS_MAX: u64 = 1 << 20; @@ -24,8 +24,8 @@ pub(crate) const NUMERIC_EVENT_POINT_MAX: u64 = 1 << 30; /// fixed-point search ceiling provably dominates the floating-point leaf /// evaluator (`docs/pruning-proof.md`, "Numeric admissibility"). /// -/// All checked quantities are a priori maxima over every deck of the pool, so -/// every ceiling the search evaluates for this request is covered. Request +/// These are a priori maxima over legal decks, not over relaxed states or +/// inverse-cutoff probes. Wide/checking arithmetic covers those separately. Request /// parameters (teammate values, opponent score) are validated before pool /// construction. pub(crate) fn numeric_domain(pool: &CardPool, ctx: &SearchContext) -> Result<(), BuildError> { @@ -177,6 +177,27 @@ pub(super) fn score(value: i64, limit: Option, field: &'static str) -> Resu Ok(value as u8) } +/// Check identities before either the main pool or a support-only seed narrows them. +pub(super) fn public_card_id(value: i32) -> Result { + if value < 0 { + return Err(BuildError::InvalidConfig( + "card identity must be nonnegative".to_string(), + )); + } + ensure("public card id", value as u64, u64::from(u16::MAX))?; + Ok(value as u16) +} + +pub(super) fn character_id(value: i32) -> Result { + if value < 0 { + return Err(BuildError::InvalidConfig( + "character identity must be nonnegative".to_string(), + )); + } + ensure("character id", value as u64, 26)?; + Ok(value as u8) +} + pub(super) fn validate_cards(cards: &[CardIntermediate]) -> Result<(), BuildError> { // Dense indices are u16 because CardIdx is intentionally compact. The // 512-bit metadata mask is only a ZMM fast-path view; overflow cards stay @@ -186,16 +207,7 @@ pub(super) fn validate_cards(cards: &[CardIntermediate]) -> Result<(), BuildErro } let mut limited_values = Vec::new(); for card in cards { - if card.game_card_id < 0 { - return Err(BuildError::InvalidConfig( - "card identity must be nonnegative".to_string(), - )); - } - ensure( - "public card id", - card.game_card_id as u64, - u64::from(u16::MAX), - )?; + public_card_id(card.game_card_id)?; ensure("character id", u64::from(card.character_id), 26)?; ensure("attribute id", u64::from(card.attr), 5)?; ensure("unit mask", u64::from(card.unit_mask_raw), 63)?; diff --git a/src/handler/tests/capacity.rs b/src/handler/tests/capacity.rs index 21d4e31..9283afe 100644 --- a/src/handler/tests/capacity.rs +++ b/src/handler/tests/capacity.rs @@ -230,3 +230,66 @@ fn capacity_applies_a_real_event_cap_before_checking_skill_width() { } } } + +#[test] +fn capacity_maximum_public_id_is_supported() { + let mut fixture = pool_constraint_fixture(&[(1, 4, 100)]); + fixture.master_cards[0].id = 65_535; + fixture.card_params[0].card_id = 65_535; + let game = bonus_tier_game(&fixture); + let (pool, _) = checked_build(&fixture, &game, &BuildParams::default()).unwrap(); + assert_eq!(pool.game_id(pool.card_idx(0).unwrap()), u16::MAX); +} + +#[test] +fn capacity_support_only_id_is_checked_before_main_filtering() { + let mut fixture = pool_constraint_fixture(&[ + (1, 4, 100), + (2, 4, 100), + (3, 4, 100), + (4, 4, 100), + (5, 4, 100), + (6, 4, 100), + ]); + fixture.master_cards[5].id = 70_000; + fixture.card_params[5].card_id = 70_000; + let events = [types::Event { + id: 214, + event_type: "world_bloom".to_string(), + }]; + let chapters = [types::WorldBloom { + event_id: 214, + game_character_id: Some(1), + chapter_no: 1, + world_bloom_chapter_type: Some("game_character".to_string()), + }]; + let game = GameData { + events: &events, + world_blooms: &chapters, + ..bonus_tier_game(&fixture) + }; + let params = BuildParams { + event_id: Some(214), + excluded_cards: vec![70_000], + ..Default::default() + }; + assert!(matches!( + checked_build(&fixture, &game, ¶ms), + Err(BuildError::CapacityExceeded { + field: "public card id", + value: 70_000, + max: 65_535 + }) + )); +} + +#[test] +fn capacity_negative_character_is_not_silently_changed_to_zero() { + let mut fixture = pool_constraint_fixture(&[(1, 4, 100)]); + fixture.master_cards[0].character_id = -1; + let game = bonus_tier_game(&fixture); + assert!(matches!( + checked_build(&fixture, &game, &BuildParams::default()), + Err(BuildError::InvalidConfig(_)) + )); +} diff --git a/src/handler/world_bloom.rs b/src/handler/world_bloom.rs index 2d377fc..4c69f34 100644 --- a/src/handler/world_bloom.rs +++ b/src/handler/world_bloom.rs @@ -121,9 +121,9 @@ pub fn world_bloom_support_cards( event_id, Some(turn), Some(special_character_id), - master.id.clamp(0, u16::MAX as i32) as u16, + super::capacity::public_card_id(master.id)?, master.card_rarity_type, - master.character_id.clamp(0, u8::MAX as i32) as u8, + super::capacity::character_id(master.character_id)?, unit_mask_raw, !filter_other_unit, card.master_rank, @@ -165,7 +165,7 @@ pub(crate) fn support_seed_from_intermediate( indexes: &index::PoolIndexes, support_master_max: bool, support_skill_max: bool, -) -> SupportSeedSlim { +) -> Result { let master = indexes .card_data(card.game_card_id) .map(|entry| &entry.master); @@ -183,14 +183,14 @@ pub(crate) fn support_seed_from_intermediate( } else { card.skill_level }; - SupportSeedSlim { - card_id: card.game_card_id.max(0).min(u16::MAX as i32) as u16, + Ok(SupportSeedSlim { + card_id: super::capacity::public_card_id(card.game_card_id)?, rarity: card.card_rarity_type, character_id: card.character_id, unit_mask: card.unit_mask_raw, master_rank, skill_level, - } + }) } /// Precomputed per-(event, turn, special-character) support bonus rate tables. diff --git a/src/search.rs b/src/search.rs index fb5714d..368567d 100644 --- a/src/search.rs +++ b/src/search.rs @@ -42,6 +42,7 @@ use tracker::{TopKTracker, deck_result_cmp}; mod placement; mod problem; mod skill_ceiling; +mod small_ids; /// 角色感知的后缀上界，用于剪枝。 pub mod suffix; mod tuning; @@ -84,6 +85,11 @@ use budget::SearchBudget; /// Execute the complete search pipeline and return its completion certificate. /// Only `SearchCompletion::Complete` certifies canonical Top-K; `TimedOut` /// contains legal, exactly evaluated incumbents, not a proven ranking. +/// +/// `pool` and `ctx` must preserve the handler's numeric/representation invariants +/// and alignment. Mutating a built context does not re-run validation. In +/// particular, support profiles must remain sorted, finite and non-negative; +/// see `docs/pruning-proof.md`, Section 29.2, for the low-level preconditions. pub fn search( pool: &CardPool, ctx: &SearchContext, diff --git a/src/search/composition.rs b/src/search/composition.rs index d0838c6..e354d93 100644 --- a/src/search/composition.rs +++ b/src/search/composition.rs @@ -42,7 +42,7 @@ use super::budget::SearchBudget; use super::dfs::canonicalize_seed_result; -use super::log_linear::{FeatureBox, LogLinearBound}; +use super::log_linear::{FeatureBox, LogLinearBound, mul_up, sum_up}; use super::objective::ObjectiveBound; use super::tracker::TopKTracker; use super::{DeckResult, SearchContext, SearchParams, SearchStats, SupportDeck}; @@ -286,9 +286,11 @@ impl RegimePlan { ); member[character] = member[character].max(weight); if may_lead(pool, ctx, card) { - let leading = weight - + bound.leader_skill * f64::from(skill) - + bound.bonus * f64::from(leader_extra(pool, ctx, card)); + let leading = sum_up([ + weight, + mul_up(bound.leader_skill, f64::from(skill)), + mul_up(bound.bonus, f64::from(leader_extra(pool, ctx, card))), + ]); leader[character] = leader[character].max(leading); } } @@ -297,16 +299,22 @@ impl RegimePlan { let best = (0..CHARACTER_COUNT) .filter(|&character| leader[character].is_finite()) .map(|character| { - leader[character] - + ranked - .iter() - .filter(|&&other| other != character) - .take(DECK_SIZE - 1) - .map(|&other| member[other]) - .sum::() + sum_up( + std::iter::once(leader[character]).chain( + ranked + .iter() + .filter(|&&other| other != character) + .take(DECK_SIZE - 1) + .map(|&other| member[other]), + ), + ) }) .fold(f64::NEG_INFINITY, f64::max); - let value = bound.constant + bound.bonus * f64::from(self.shared_extra) + best; + let value = sum_up([ + bound.constant, + mul_up(bound.bonus, f64::from(self.shared_extra)), + best, + ]); bound.excludes( value, threshold_ep, diff --git a/src/search/dominance.rs b/src/search/dominance.rs index 5bf047f..c9f1f58 100644 --- a/src/search/dominance.rs +++ b/src/search/dominance.rs @@ -94,38 +94,49 @@ pub struct MemberDominance { pub alternatives: Vec>, } -/// Completion-safe support opportunity cost, including reserve entries and all -/// cultivation variants of each public card identity. +/// Support opportunity costs over every possible leader profile. /// -/// Let R be the other four main cards and t the q-th support value after removing -/// R, A and B. Replacing B by A loses at most -/// `(a - t)+ - (b - t)+ <= max(0, a - max(b, floor))`, where floor is the global -/// support value at one-based rank q+5. Removing at most five cards cannot push -/// the q-th remaining value below that rank. Outward rounding preserves the -/// inequality: a is rounded up, b and floor down. Taking the worst leader -/// profile is safe for every legal completion. +/// The zero-cost case preserves each sorted support term, hence also its f64 +/// sum. Compensation needs a STRICT real bonus surplus larger than the two +/// evaluator rounding errors; equality over the reals is not sufficient. struct SupportDimension { - /// Support profiles compared per card; each row below holds one value per - /// profile, card-major. profiles: usize, - upper_x100: Vec, - lower_x100: Vec, - replacement_floor_x100: Vec, + values: Vec, + replacement_floor: Vec, + compensation_safe: Vec, + valid: bool, } impl SupportDimension { - #[inline(always)] - fn deficit_x100(&self, lhs: CardIdx, rhs: CardIdx) -> i32 { - let upper = &self.upper_x100[lhs.raw() * self.profiles..][..self.profiles]; - let lower = &self.lower_x100[rhs.raw() * self.profiles..][..self.profiles]; + #[inline] + fn affordable(&self, lhs: CardIdx, rhs: CardIdx, surplus_x10: u32) -> bool { + if !self.valid { + return false; + } + let upper = &self.values[lhs.raw() * self.profiles..][..self.profiles]; + let lower = &self.values[rhs.raw() * self.profiles..][..self.profiles]; + let surplus_lower = (f64::from(surplus_x10) / 10.0).next_down(); upper .iter() .zip(lower) - .zip(&self.replacement_floor_x100) - .map(|((&upper, &lower), &floor)| upper - lower.max(floor)) - .max() - .unwrap_or(0) - .max(0) + .enumerate() + .all(|(profile, (&a, &b))| { + let refill = b.max(self.replacement_floor[profile]); + if a <= refill { + // No support order statistic decreases. No cancellation or + // real-to-float error estimate is needed for this branch. + return true; + } + if !self.compensation_safe[profile] { + return false; + } + let deficit_upper = (a - refill).next_up(); + let slack_lower = (surplus_lower - deficit_upper).next_down(); + // At most 255 support additions and three main/extra additions, + // at total magnitude < 2^21, give a two-deck error < 2^-22. + // 2^-20 is four times that bound (pruning-proof Section 5). + slack_lower > 1.0 / 1_048_576.0 + }) } } @@ -149,57 +160,59 @@ fn support_dimension( if !is_world_bloom || profiles.is_empty() { return None; } - // Every cultivation variant of a public card shares its support value. let span = pool .indices() .map(|card| usize::from(pool.game_id(card)) + 1) .max() .unwrap_or(0); - // One-based position in the current profile's card list, zero if absent. - let mut entry_by_game_id = vec![0u32; span]; let width = profiles.len(); - let mut upper_x100 = vec![0i32; pool.count() * width]; - let mut lower_x100 = vec![0i32; pool.count() * width]; - let mut replacement_floor_x100 = vec![0i32; width]; - let mut any = false; + let mut dimension = SupportDimension { + profiles: width, + values: vec![0.0; pool.count() * width], + replacement_floor: vec![0.0; width], + compensation_safe: vec![false; width], + valid: true, + }; + let mut value_by_id = vec![0.0; span]; for (profile, support) in profiles.iter().enumerate() { - let count = support.count as usize; + let count = usize::from(support.count); if count == 0 { continue; } - replacement_floor_x100[profile] = support - .cards - .get(count + crate::types::DECK_SIZE - 1) - .map(|(_, value)| (value * 100.0).floor() as i32) - .unwrap_or(0); - // A reserve may enter the counted prefix after another main card is - // excluded. Recording only the original q entries is not admissible. - for (entry, &(game_id, _)) in support.cards.iter().enumerate() { - if let Some(slot) = entry_by_game_id.get_mut(usize::from(game_id)) { - *slot = entry as u32 + 1; + let mut seen = std::collections::BTreeSet::new(); + let mut previous = f64::INFINITY; + let mut sum_upper = 0.0f64; + for (rank, &(id, value)) in support.cards.iter().enumerate() { + if !value.is_finite() || value < 0.0 || value > previous || !seen.insert(id) { + // None would mean "no support penalty" to the caller. Keep + // an explicit unusable dimension instead of approving a pair. + dimension.valid = false; + return Some(dimension); + } + previous = value; + if rank < count { + sum_upper = (sum_upper + value).next_up(); + } + if let Some(slot) = value_by_id.get_mut(usize::from(id)) { + *slot = value; } } + dimension.compensation_safe[profile] = sum_upper <= 1_048_576.0; + dimension.replacement_floor[profile] = support + .cards + .get(count + crate::types::DECK_SIZE - 1) + .map_or(0.0, |entry| entry.1); for card in pool.indices() { - let entry = entry_by_game_id[usize::from(pool.game_id(card))]; - if entry != 0 { - let value = support.cards[entry as usize - 1].1; - upper_x100[card.raw() * width + profile] = (value * 100.0).ceil() as i32; - lower_x100[card.raw() * width + profile] = (value * 100.0).floor() as i32; - any = true; - } + dimension.values[card.raw() * width + profile] = + value_by_id[usize::from(pool.game_id(card))]; } - for &(game_id, _) in &support.cards { - if let Some(slot) = entry_by_game_id.get_mut(usize::from(game_id)) { - *slot = 0; + for &(id, _) in &support.cards { + if let Some(slot) = value_by_id.get_mut(usize::from(id)) { + *slot = 0.0; } } } - any.then_some(SupportDimension { - profiles: width, - upper_x100, - lower_x100, - replacement_floor_x100, - }) + Some(dimension) } /// 终章 member 位支配裁剪：忽略队长专属称号/当期加成逐角色比较， @@ -302,13 +315,9 @@ fn support_deficit_affordable( let Some(support) = support else { return true; }; - let deficit = support.deficit_x100(lhs, rhs); - if deficit <= 0 { - return true; - } - let surplus_x10 = pool.event_bonus_exact(lhs).base_x10() as i32 - - pool.event_bonus_exact(rhs).base_x10() as i32; - deficit <= surplus_x10 * 10 + let surplus_x10 = + pool.event_bonus_exact(lhs).base_x10() - pool.event_bonus_exact(rhs).base_x10(); + support.affordable(lhs, rhs, surplus_x10) } /// `leader_bonuses` also requires the leader-only bonuses not to be worse; a diff --git a/src/search/log_linear.rs b/src/search/log_linear.rs index b93e38f..5afc433 100644 --- a/src/search/log_linear.rs +++ b/src/search/log_linear.rs @@ -16,14 +16,15 @@ //! the event point of every deck of a subtree. The derivation is "Log-linear //! event-point bound" in `docs/pruning-proof.md`. +mod interval; +use interval::Interval; +use interval::div_up; +pub(crate) use interval::{add_up, mul_up, sub_down, sum_up}; + use crate::types::{DECK_SIZE, LiveSkillOrder, LiveType, ScoreTarget}; use super::objective::{LIVE_SCORE_BOUND_SCALE, ObjectiveBound, RATE_FRACTION_SCALE}; -/// Slack below `ln(threshold)` that absorbs the floating-point error of a -/// bound and of the sums compared with it. -const LOG_MARGIN: f64 = 1e-9; - /// Largest aggregate features of every deck a bound covers. #[derive(Clone, Copy, Debug, PartialEq)] pub(crate) struct FeatureBox { @@ -64,29 +65,39 @@ impl LogLinearBound { threshold_ep: u64, ) -> Option { let model = EventModel::new(objective, feature_box)?; - if threshold_ep == 0 || feature_box.power == 0 { + if threshold_ep == 0 + || threshold_ep > u64::from(u32::MAX) + || feature_box.power == 0 + || feature_box.leader_skill_min > feature_box.leader_skill_max + { return None; } + let point = Interval::point; let honor = f64::from(objective.honor_bonus); let power_max = f64::from(feature_box.power) + honor; let skill_max = f64::from(feature_box.skill); let leader_max = f64::from(feature_box.leader_skill_max); let bonus_max = f64::from(feature_box.bonus); let tau = threshold_ep as f64; + let scale = point(LIVE_SCORE_BOUND_SCALE as f64); + let divisor = point(model.divisor); + let offset = point(model.offset); + let kappa = point(model.kappa); - // u = P * Q / D lies in [u_lo, u_hi] for every deck that can reach - // the threshold: below u_lo even the largest bonus falls short. + // Enclose the model's exact real endpoints, then WIDEN the chord + // interval. Inward-rounded endpoints could exclude a feasible deck. + let rate_max = model.rate_interval(skill_max, leader_max); let u_hi = - power_max * model.per_power(model.rate_1m(skill_max, leader_max)) / model.divisor; - let u_lo = tau / (model.kappa * (100.0 + bonus_max)) - model.offset; - if !(u_lo > 0.0 && u_lo < u_hi) { + point(power_max) * (point(4.0) * rate_max + point(model.active)) / scale / divisor; + let u_lo = point(tau) / (kappa * point(100.0 + bonus_max)) - offset; + if !u_lo.finite() || !u_hi.finite() || !(u_lo.lo > 0.0 && u_lo.lo < u_hi.hi) { return None; } - // Chord of the convex ln(c + e^t) over [ln u_lo, ln u_hi]. - let sigma = ((model.offset + u_hi) / (model.offset + u_lo)).ln() / (u_hi / u_lo).ln(); + let lo = point(u_lo.lo); + let sigma = chord_slope(model.offset, u_lo.lo, u_hi.hi)?; - // Tangent point: where the ray from the origin to the box maximum - // meets the threshold surface of the relaxed event point. + // This point is only a tightness heuristic. The certificate below + // holds for ANY positive finite point, including rounded bisection. let relaxed = |lambda: f64| { let rate = model.per_power(model.rate_1m(lambda * skill_max, leader_max)); let u = lambda * power_max * rate / model.divisor; @@ -101,42 +112,55 @@ impl LogLinearBound { high = mid; } } - // A tangent point near the origin would make every weighted term - // large; keeping it at 2^-10 of the box bounds each term by 2^10. if high < 1.0 / 1024.0 { return None; } - let power_0 = high * power_max; + let power_0 = point(high * power_max); let skill_0 = high * skill_max; - let bonus_0 = high * bonus_max; - // Per unit power, rate(S, L) <= intercept + skill * S + leader * L. + let bonus_0 = point(high * bonus_max); let tangent = model.tangent(skill_0); - let intercept = model.per_power(tangent.intercept); - let skill = model.slope(tangent.skill); - let leader_skill = model.slope(tangent.leader_skill); - let rate_0 = intercept + skill * skill_0 + leader_skill * leader_max; - if !(power_0 > 0.0 && rate_0 > 0.0) { + // These scalar coefficients themselves bound q; treat their stored + // f64 values as exact constants of the affine majorant. + let intercept = point(model.per_power(tangent.intercept)); + let skill = point(model.slope(tangent.skill)); + let leader_skill = point(model.slope(tangent.leader_skill)); + let rate_0 = intercept + skill * point(skill_0) + leader_skill * point(leader_max); + if !power_0.finite() || !rate_0.finite() || power_0.lo <= 0.0 || rate_0.lo <= 0.0 { return None; } - - let constant = model.kappa.ln() + (model.offset + u_lo).ln() - sigma * u_lo.ln() + let one = point(1.0); + let hundred = point(100.0); + let bonus_denominator = hundred + bonus_0; + let constant = kappa.ln() + (offset + lo).ln() - sigma * lo.ln() + sigma - * (power_0.ln() - 1.0 + honor / power_0 + rate_0.ln() - 1.0 + intercept / rate_0 - - model.divisor.ln()) - + (100.0 + bonus_0).ln() - - 1.0 - + 100.0 / (100.0 + bonus_0); - // Keeps the rounding error of the sums compared with the threshold - // far below LOG_MARGIN. - if !constant.is_finite() || constant.abs() >= 256.0 { + * (power_0.ln() - one + point(honor) / power_0 + rate_0.ln() - one + + intercept / rate_0 + - divisor.ln()) + + bonus_denominator.ln() + - one + + hundred / bonus_denominator; + let coefficients = [ + sigma / power_0, + sigma * skill / rate_0, + sigma * leader_skill / rate_0, + one / bonus_denominator, + ]; + if !constant.finite() + || constant.hi.abs() >= 256.0 + || coefficients + .iter() + .any(|value| !value.finite() || value.hi < 0.0) + { return None; } + // Every feature is non-negative, so choosing each upper endpoint + // yields a pointwise majorant of the real affine certificate. Some(Self { - power: sigma / power_0, - skill: sigma * skill / rate_0, - leader_skill: sigma * leader_skill / rate_0, - bonus: 1.0 / (100.0 + bonus_0), - constant, + power: coefficients[0].hi, + skill: coefficients[1].hi, + leader_skill: coefficients[2].hi, + bonus: coefficients[3].hi, + constant: constant.hi, floor_ep: threshold_ep, }) } @@ -144,9 +168,11 @@ impl LogLinearBound { /// Weight of one card's power, skill and bonus. #[inline(always)] pub(crate) fn weigh(&self, power: u32, skill: u32, bonus: u32) -> f64 { - self.power * f64::from(power) - + self.skill * f64::from(skill) - + self.bonus * f64::from(bonus) + sum_up([ + mul_up(self.power, f64::from(power)), + mul_up(self.skill, f64::from(skill)), + mul_up(self.bonus, f64::from(bonus)), + ]) } /// The weight below which [`Self::excludes`] rules a subtree out at @@ -154,7 +180,10 @@ impl LogLinearBound { /// threshold computes it once. #[inline(always)] pub(crate) fn log_cutoff(threshold_ep: u64) -> f64 { - (threshold_ep as f64).ln() - LOG_MARGIN + if threshold_ep == 0 || threshold_ep > u64::from(u32::MAX) { + return f64::NEG_INFINITY; + } + Interval::point(threshold_ep as f64).ln().lo } /// Whether a subtree whose features weigh at most `value` has no deck @@ -164,7 +193,32 @@ impl LogLinearBound { pub(crate) fn excludes(&self, value: f64, threshold_ep: u64, cutoff: f64) -> bool { debug_assert!(threshold_ep >= self.floor_ep); debug_assert_eq!(cutoff.to_bits(), Self::log_cutoff(threshold_ep).to_bits()); - value < cutoff + value.is_finite() && cutoff.is_finite() && value < cutoff + } +} + +/// The chord slope is certified, not assumed accurate because ln is accurate. +/// A denominator interval reaching zero makes the optional bound unavailable. +fn chord_slope(offset: f64, lo: f64, hi: f64) -> Option { + let c = Interval::point(offset); + let a = Interval::point(lo); + let b = Interval::point(hi); + let denominator = b.ln() - a.ln(); + if !denominator.finite() || denominator.lo <= 0.0 { + return None; + } + let sigma = ((c + b).ln() - (c + a).ln()) / denominator; + (sigma.finite() && sigma.lo > 0.0 && sigma.hi < 1.0).then_some(sigma) +} + +/// Upper conversion of a non-negative fixed-point integer. +fn integer_up(value: i64) -> f64 { + debug_assert!(value >= 0); + let rounded = value as f64; + if value <= (1_i64 << 53) { + rounded + } else { + rounded.next_up() } } @@ -217,8 +271,13 @@ impl EventModel { _ => return None, }; let scale = LIVE_SCORE_BOUND_SCALE as f64; - let kappa = - f64::from(objective.music_rate_pct) * f64::from(objective.boost_rate_pct) / scale; + let kappa = div_up( + mul_up( + f64::from(objective.music_rate_pct), + f64::from(objective.boost_rate_pct), + ), + scale, + ); let non_negative = objective.base_rate_1m >= 0 && objective.srs_div500_q >= 0 && objective.avg_sum5_1m >= 0 @@ -232,32 +291,35 @@ impl EventModel { } // The live numerator is 4 * rate_1m * P + active_1m, with active_1m = // coefficient * (P + 4 * teammate) or coefficient * 5 * P. - let coefficient = objective.active_1m_coeff as f64; + let coefficient = integer_up(objective.active_1m_coeff); let (active, fixed) = match objective.multi_teammate_power { - Some(power) => (coefficient, coefficient * 4.0 * f64::from(power)), - None => (coefficient * DECK_SIZE as f64, 0.0), + Some(power) => ( + coefficient, + mul_up(mul_up(coefficient, 4.0), f64::from(power)), + ), + None => (mul_up(coefficient, DECK_SIZE as f64), 0.0), }; - let base = objective.base_rate_1m as f64; + let base = integer_up(objective.base_rate_1m); let rate = match objective.effective_live_type { LiveType::Multi => { // max(4L + S, t) <= 4L + S + max(0, t - 4 L_min). - let excess = (objective.teammate_su_5x - - 4 * i64::from(feature_box.leader_skill_min)) - .max(0) as f64; + let excess = + (objective.teammate_su_5x - 4 * i64::from(feature_box.leader_skill_min)).max(0); + let excess = integer_up(excess); // The skill term rounds up by less than one. - let srs = objective.srs_div500_q as f64 / RATE_FRACTION_SCALE; + let srs = div_up(integer_up(objective.srs_div500_q), RATE_FRACTION_SCALE); RateModel::Affine(Tangent { - intercept: base + 1.0 + excess * srs, + intercept: add_up(add_up(base, 1.0), mul_up(excess, srs)), skill: srs, - leader_skill: 4.0 * srs, + leader_skill: mul_up(4.0, srs), }) } _ if matches!(objective.live_skill_order, LiveSkillOrder::Average) => { // Each ceil_div_positive adds less than one. RateModel::Affine(Tangent { - intercept: base + 2.0, - skill: objective.avg_sum5_1m as f64 / 500.0, - leader_skill: objective.avg_leader_rate_1m as f64 / 100.0, + intercept: add_up(base, 2.0), + skill: div_up(integer_up(objective.avg_sum5_1m), 500.0), + leader_skill: div_up(integer_up(objective.avg_leader_rate_1m), 100.0), }) } _ => { @@ -267,9 +329,9 @@ impl EventModel { let cap = f64::from(feature_box.card_skill); let sorted = objective .sorted_rates_q - .map(|rate| rate as f64 / RATE_FRACTION_SCALE); + .map(|rate| div_up(integer_up(rate), RATE_FRACTION_SCALE)); RateModel::Sorted { - intercept: base + 1.0 + cap * sorted[0], + intercept: add_up(add_up(base, 1.0), mul_up(cap, sorted[0])), cap, rates: core::array::from_fn(|slot| sorted[slot + 1]), } @@ -277,7 +339,7 @@ impl EventModel { }; Some(Self { kappa, - offset: offset + fixed / scale / divisor, + offset: add_up(offset, div_up(div_up(fixed, scale), divisor)), divisor, rate, active, @@ -303,14 +365,41 @@ impl EventModel { } } + /// Exact-real rate of the stored, upward-prepared model, enclosed. + fn rate_interval(&self, skill: f64, leader: f64) -> Interval { + let p = Interval::point; + match &self.rate { + RateModel::Affine(t) => { + p(t.intercept) + p(t.skill) * p(skill) + p(t.leader_skill) * p(leader) + } + RateModel::Sorted { + intercept, + cap, + rates, + } => { + let mut value = p(*intercept); + for (slot, &coefficient) in rates.iter().enumerate() { + // Callers pass integer skill sums; these differences and + // clamps are exact and within the u32 range. + value = + value + p(coefficient) * p((skill - slot as f64 * cap).clamp(0.0, *cap)); + } + value + } + } + } + /// Live score per unit power at fixed-point rate `rate_1m`. fn per_power(&self, rate_1m: f64) -> f64 { - (4.0 * rate_1m + self.active) / LIVE_SCORE_BOUND_SCALE as f64 + div_up( + add_up(mul_up(4.0, rate_1m), self.active), + LIVE_SCORE_BOUND_SCALE as f64, + ) } /// Live score per unit power of one unit of a fixed-point rate slope. fn slope(&self, rate_1m: f64) -> f64 { - 4.0 * rate_1m / LIVE_SCORE_BOUND_SCALE as f64 + div_up(mul_up(4.0, rate_1m), LIVE_SCORE_BOUND_SCALE as f64) } /// An affine function of `(S, L)` that bounds [`Self::rate_1m`] for every @@ -318,16 +407,24 @@ impl EventModel { fn tangent(&self, skill_0: f64) -> Tangent { match &self.rate { RateModel::Affine(tangent) => *tangent, - RateModel::Sorted { cap, rates, .. } => { - // The right slope of the concave fill is a supergradient. - let segment = if *cap > 0.0 { - (skill_0 / cap).floor() as usize - } else { - DECK_SIZE - }; + RateModel::Sorted { + intercept, + cap, + rates, + } => { + // Compare exact integer breakpoints instead of flooring a + // rounded quotient that could select the wrong segment. + let segment = (0..DECK_SIZE) + .find(|&slot| skill_0 < (slot + 1) as f64 * cap) + .unwrap_or(DECK_SIZE); let slope = rates.get(segment).copied().unwrap_or(0.0); + let p = Interval::point; + let mut constant = p(*intercept); + for &rate in &rates[..segment] { + constant = constant + p(*cap) * (p(rate) - p(slope)); + } Tangent { - intercept: self.rate_1m(skill_0, 0.0) - slope * skill_0, + intercept: constant.hi, skill: slope, leader_skill: 0.0, } @@ -432,7 +529,10 @@ mod tests { ); // The upper half of every range reaches the thresholds. let upper = |max: u32, draw: u32| max - draw % (max / 2 + 1); - let members = upper(4 * feature_box.card_skill, next(u32::MAX)); + let members = upper( + (feature_box.skill - leader).min(4 * feature_box.card_skill), + next(u32::MAX), + ); let power = upper(feature_box.power, next(u32::MAX)); let bonus = upper(feature_box.bonus, next(u32::MAX)); let skill = leader + members; @@ -470,6 +570,14 @@ mod tests { ); } + #[test] + fn nearly_coincident_chord_endpoints_fall_back() { + assert!(chord_slope(100.0, 100.0, 100.0_f64.next_up()).is_none()); + let slope = chord_slope(100.0, 100.0, 200.0).unwrap(); + let reference = 1.5_f64.ln() / 2.0_f64.ln(); + assert!(slope.lo <= reference && slope.hi >= reference); + } + #[test] fn unsupported_objectives_have_no_bound() { let feature_box = FeatureBox { diff --git a/src/search/log_linear/interval.rs b/src/search/log_linear/interval.rs new file mode 100644 index 0000000..c05879e --- /dev/null +++ b/src/search/log_linear/interval.rs @@ -0,0 +1,227 @@ +//! Outward binary64 intervals for preparing a pruning certificate. +//! No platform logarithm participates: ln uses range reduction and a positive +//! atanh series with an explicit geometric remainder (pruning-proof §18.8). +use std::ops::{Add, Div, Mul, Sub}; +use std::sync::OnceLock; + +#[derive(Clone, Copy, Debug)] +pub(super) struct Interval { + pub(super) lo: f64, + pub(super) hi: f64, +} + +impl Interval { + const INVALID: Self = Self { + lo: f64::NAN, + hi: f64::NAN, + }; + + pub(super) fn point(value: f64) -> Self { + Self { + lo: value, + hi: value, + } + } + + pub(super) fn finite(self) -> bool { + self.lo.is_finite() && self.hi.is_finite() && self.lo <= self.hi + } + + /// Monotonicity of ln reduces an interval argument to its endpoints. + pub(super) fn ln(self) -> Self { + if !self.finite() || self.lo <= 0.0 { + return Self::INVALID; + } + Self { + lo: ln_point(self.lo).lo, + hi: ln_point(self.hi).hi, + } + } +} + +impl Add for Interval { + type Output = Self; + fn add(self, other: Self) -> Self { + if !self.finite() || !other.finite() { + return Self::INVALID; + } + if self.lo == 0.0 && self.hi == 0.0 { + return other; + } + if other.lo == 0.0 && other.hi == 0.0 { + return self; + } + Self { + lo: (self.lo + other.lo).next_down(), + hi: (self.hi + other.hi).next_up(), + } + } +} +impl Sub for Interval { + type Output = Self; + fn sub(self, other: Self) -> Self { + if !self.finite() || !other.finite() { + return Self::INVALID; + } + Self { + lo: (self.lo - other.hi).next_down(), + hi: (self.hi - other.lo).next_up(), + } + } +} +impl Mul for Interval { + type Output = Self; + fn mul(self, other: Self) -> Self { + if !self.finite() || !other.finite() { + return Self::INVALID; + } + if (self.lo == 0.0 && self.hi == 0.0) || (other.lo == 0.0 && other.hi == 0.0) { + return Self::point(0.0); + } + let values = [ + self.lo * other.lo, + self.lo * other.hi, + self.hi * other.lo, + self.hi * other.hi, + ]; + Self { + lo: values.into_iter().fold(f64::INFINITY, f64::min).next_down(), + hi: values + .into_iter() + .fold(f64::NEG_INFINITY, f64::max) + .next_up(), + } + } +} +impl Div for Interval { + type Output = Self; + fn div(self, other: Self) -> Self { + if !self.finite() || !other.finite() || (other.lo <= 0.0 && other.hi >= 0.0) { + return Self::INVALID; + } + let values = [ + self.lo / other.lo, + self.lo / other.hi, + self.hi / other.lo, + self.hi / other.hi, + ]; + Self { + lo: values.into_iter().fold(f64::INFINITY, f64::min).next_down(), + hi: values + .into_iter() + .fold(f64::NEG_INFINITY, f64::max) + .next_up(), + } + } +} + +/// Encloses ln(m) for 1 <= m <= 2. With z=(m-1)/(m+1), 0 <= z <= 1/3: +/// ln(m)=2*sum(z^(2j+1)/(2j+1), j=0..31)+R, +/// 0 <= R <= 2*z^65/(65*(1-z^2)). All endpoints are rounded outward. +fn ln_mantissa(m: f64) -> Interval { + debug_assert!((1.0..=2.0).contains(&m)); + if m == 1.0 { + return Interval::point(0.0); + } + let one = Interval::point(1.0); + let two = Interval::point(2.0); + let mut z = (Interval::point(m) - one) / (Interval::point(m) + one); + z.lo = z.lo.max(0.0); + let square = z * z; + let mut power = z; + let mut sum = Interval::point(0.0); + for j in 0..32 { + sum = sum + power / Interval::point(f64::from(2 * j + 1)); + power = power * square; + } + let remainder = two * power / (Interval::point(65.0) * (one - square)); + two * sum + + Interval { + lo: 0.0, + hi: remainder.hi, + } +} + +fn ln_point(mut x: f64) -> Interval { + if !x.is_finite() || x <= 0.0 { + return Interval::INVALID; + } + let mut shift = 0; + if x < f64::MIN_POSITIVE { + // Exact power-of-two scaling, including the smallest subnormal. + x *= 4_503_599_627_370_496.0; + shift = 52; + } + let bits = x.to_bits(); + let exponent = ((bits >> 52) & 0x7ff) as i32 - 1023 - shift; + let mantissa = f64::from_bits((bits & ((1_u64 << 52) - 1)) | (1023_u64 << 52)); + static LN_TWO: OnceLock = OnceLock::new(); + let ln_two = *LN_TWO.get_or_init(|| ln_mantissa(2.0)); + ln_mantissa(mantissa) + Interval::point(f64::from(exponent)) * ln_two +} + +/// Outward primitives for applying the already-prepared affine certificate. +#[inline(always)] +pub(crate) fn add_up(left: f64, right: f64) -> f64 { + (left + right).next_up() +} +#[inline(always)] +pub(crate) fn mul_up(left: f64, right: f64) -> f64 { + (left * right).next_up() +} +#[inline(always)] +pub(crate) fn div_up(left: f64, right: f64) -> f64 { + (left / right).next_up() +} +#[inline(always)] +pub(crate) fn sub_down(left: f64, right: f64) -> f64 { + (left - right).next_down() +} +#[inline] +pub(crate) fn sum_up(values: impl IntoIterator) -> f64 { + values.into_iter().fold(0.0, add_up) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn interval_division_refuses_a_zero_crossing() { + assert!(!(Interval::point(1.0) / Interval { lo: -1.0, hi: 1.0 }).finite()); + } + + #[test] + // These are adjacent enclosing endpoints, deliberately not rounded constants. + #[allow(clippy::approx_constant)] + fn logarithm_encloses_reference_brackets() { + for (x, lo, hi) in [ + (1.0, 0.0, 0.0), + (2.0, 0.6931471805599453, 0.6931471805599454), + (0.5, -0.6931471805599454, -0.6931471805599453), + (10.0, 2.3025850929940455, 2.302585092994046), + (100.0, 4.605170185988091, 4.605170185988092), + ] { + let value = Interval::point(x).ln(); + assert!( + value.finite() && value.lo <= lo && value.hi >= hi, + "{x}: {value:?}" + ); + } + } + + #[test] + fn logarithm_is_finite_at_binary64_extremes() { + for x in [ + f64::from_bits(1), + f64::MIN_POSITIVE, + 1.0_f64.next_up(), + f64::MAX, + ] { + let value = Interval::point(x).ln(); + assert!(value.finite(), "{x}: {value:?}"); + // Diagnostic comparison only; production does not trust libm ln. + assert!(value.lo <= x.ln() && value.hi >= x.ln(), "{x}: {value:?}"); + } + } +} diff --git a/src/search/objective.rs b/src/search/objective.rs index 51c00eb..94b2734 100644 --- a/src/search/objective.rs +++ b/src/search/objective.rs @@ -14,7 +14,7 @@ //! comes from the integer grid instead. The live numerator is an integer on a //! `10^-6` grid and each event-point stage is a rational on a `10^-4` (or //! coarser) grid, while the evaluator's accumulated relative rounding is at -//! most `28 * 2^-53`. Inside the numeric domain that pool construction +//! bounded by the full dependency-path argument in the proof. Inside the domain that pool construction //! enforces (`handler::capacity::numeric_domain`) the rounding never reaches //! the next grid point, so every truncated ceiling dominates the truncated //! evaluator value. The full argument is "Numeric admissibility" in @@ -64,9 +64,16 @@ impl LiveProduct { /// `numerator / denominator`, for a positive denominator. #[inline] pub(crate) fn live(&self, numerator: i128, denominator: i128) -> u32 { - let live = (numerator + i128::from(self.constant) * denominator) - / (denominator * i128::from(self.divisor) * i128::from(LIVE_SCORE_BOUND_SCALE)); - live.clamp(0, i128::from(u32::MAX)) as u32 + // An unavailable tighter bound is +infinity, never a wrapped value. + let wide = || -> Option { + let numerator = + numerator.checked_add(i128::from(self.constant).checked_mul(denominator)?)?; + let denominator = denominator + .checked_mul(i128::from(self.divisor))? + .checked_mul(i128::from(LIVE_SCORE_BOUND_SCALE))?; + (denominator > 0).then(|| numerator / denominator) + }; + wide().map_or(u32::MAX, |live| live.clamp(0, i128::from(u32::MAX)) as u32) } } @@ -324,14 +331,7 @@ impl ObjectiveBound { }; let active_1m = self.active_1m_coeff * power_sum; let live_score = ((rate_1m * power_total as i64 * 4 + active_1m) / 1_000_000) as i32; - let other_score = if self.other_score == 0 { - (live_score as i64).saturating_mul(4) - } else { - self.other_score as i64 - }; - let base_score = 110 + live_score as i64 / 17_000 + (other_score / 340_000).min(13); - let inner = base_score * self.music_rate_pct as i64 * (bonus_total as i64 + 100) / 10_000; - let event_point = (inner * self.boost_rate_pct as i64 / 100) as i32; + let event_point = self.calc_event_point_bound(live_score, bonus_total); ((event_point as u64) << 32) | (live_score as u32 as u64) } @@ -430,10 +430,12 @@ impl ObjectiveBound { }; Some(LiveProduct { honor, - intercept: 4 * D * (self.base_rate_1m + 1) + D * per_power, - leader: 16 * self.srs_div500_q, - skill: 4 * self.srs_div500_q, - constant: D * constant, + intercept: (4 * D) + .checked_mul(self.base_rate_1m.checked_add(1)?)? + .checked_add(D.checked_mul(per_power)?)?, + leader: 16_i64.checked_mul(self.srs_div500_q)?, + skill: 4_i64.checked_mul(self.srs_div500_q)?, + constant: D.checked_mul(constant)?, divisor: D, floor: self.teammate_su_5x, }) @@ -446,9 +448,12 @@ impl ObjectiveBound { // rate + S * sum5. Some(LiveProduct { honor, - intercept: 4 * (500 * self.base_rate_1m + 1000), - leader: 20 * self.avg_leader_rate_1m, - skill: 4 * self.avg_sum5_1m, + intercept: 500_i64 + .checked_mul(self.base_rate_1m)? + .checked_add(1000)? + .checked_mul(4)?, + leader: 20_i64.checked_mul(self.avg_leader_rate_1m)?, + skill: 4_i64.checked_mul(self.avg_sum5_1m)?, constant: 0, divisor: 500, floor: 0, @@ -469,39 +474,35 @@ impl ObjectiveBound { if !self.has_event { return live_score; } - match self.effective_live_type { - LiveType::Challenge | LiveType::ChallengeAuto => (100 + live_score / 20_000) * 120, - LiveType::Solo | LiveType::Auto => { - let base_score = (100 + live_score / 20_000) as i64; - let inner = - base_score * self.music_rate_pct as i64 * (total_bonus as i64 + 100) / 10_000; - (inner * self.boost_rate_pct as i64 / 100) as i32 - } - LiveType::Multi => { - let other_score = if self.other_score == 0 { - (live_score as i64).saturating_mul(4) - } else { - self.other_score as i64 - }; - let base_score = 110 + live_score as i64 / 17_000 + (other_score / 340_000).min(13); - let inner = - base_score * self.music_rate_pct as i64 * (total_bonus as i64 + 100) / 10_000; - (inner * self.boost_rate_pct as i64 / 100) as i32 + // Inverse-cutoff probes cover all non-negative i32 live scores, + // not just the a-priori range of legal leaves. Keep all stages wide + // and clip the final UPPER bound instead of wrapping a narrowing cast. + // Every supported leaf event point is below this saturation value. + let base = match self.effective_live_type { + LiveType::Challenge | LiveType::ChallengeAuto => { + return (100 + live_score / 20_000) * 120; } - LiveType::Cheerful => { - let other_score = if self.other_score == 0 { - (live_score as i64).saturating_mul(4) + LiveType::Mysekai => return 0, + LiveType::Solo | LiveType::Auto => i128::from(100 + live_score / 20_000), + LiveType::Multi | LiveType::Cheerful => { + let other = if self.other_score == 0 { + i64::from(live_score) * 4 } else { - self.other_score as i64 + i64::from(self.other_score) }; - let base_score = 110 + live_score as i64 / 17_000 + (other_score / 340_000).min(13); - let inner = (base_score * self.music_rate_pct as i64 * (total_bonus as i64 + 100) - / 10_000) as i32; - let with_life = inner as i64 * self.life_rate_num as i64 / 5000; - (with_life * self.boost_rate_pct as i64 / 100) as i32 + i128::from(110 + i64::from(live_score) / 17_000 + (other / 340_000).min(13)) } - LiveType::Mysekai => 0, - } + }; + // Three u32-sized factors and the bounded live-base fit i128, + // including the later life and boost factors. + let inner = + base * i128::from(self.music_rate_pct) * (i128::from(total_bonus) + 100) / 10_000; + let with_life = if self.effective_live_type == LiveType::Cheerful { + inner * i128::from(self.life_rate_num) / 5000 + } else { + inner + }; + (with_life * i128::from(self.boost_rate_pct) / 100).clamp(0, i128::from(i32::MAX)) as i32 } #[inline(always)] diff --git a/src/search/small_ids.rs b/src/search/small_ids.rs new file mode 100644 index 0000000..2ba43b3 --- /dev/null +++ b/src/search/small_ids.rs @@ -0,0 +1,70 @@ +//! Smallest distinct public card IDs with an explicit occupied length. +//! Every u16, including 65535, is a legal ID; no value is a missing-entry sentinel. +#[derive(Clone, Copy)] +pub(super) struct SmallestIds { + ids: [u16; N], + len: u8, +} + +impl SmallestIds { + pub(super) fn new() -> Self { + assert!(N > 0 && N <= u8::MAX as usize); + Self { + ids: [0; N], + len: 0, + } + } + + #[inline] + pub(super) fn as_slice(&self) -> &[u16] { + &self.ids[..usize::from(self.len)] + } + + /// Retain the N smallest distinct IDs seen so far, in ascending order. + #[inline] + pub(super) fn insert(&mut self, id: u16) { + let pos = self.as_slice().partition_point(|&old| old < id); + if self.as_slice().get(pos) == Some(&id) || pos == N { + return; + } + let len = (usize::from(self.len) + 1).min(N); + for index in (pos + 1..len).rev() { + self.ids[index] = self.ids[index - 1]; + } + self.ids[pos] = id; + self.len = len as u8; + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn both_endpoints_are_values_not_padding() { + let mut ids = SmallestIds::<3>::new(); + assert!(ids.as_slice().is_empty()); + ids.insert(u16::MAX); + ids.insert(0); + ids.insert(u16::MAX); + assert_eq!(ids.as_slice(), &[0, u16::MAX]); + ids.insert(19); + assert_eq!(ids.as_slice(), &[0, 19, u16::MAX]); + ids.insert(5); + assert_eq!(ids.as_slice(), &[0, 5, 19]); + } + + #[test] + fn every_prefix_matches_sorted_distinct_ids() { + let mut ids = SmallestIds::<5>::new(); + let mut expected = Vec::new(); + for id in [65535, 65534, 3, 0, 3, 65535, 10, 9, 8, 7, 6, 5, 4, 2, 1] { + ids.insert(id); + expected.push(id); + expected.sort_unstable(); + expected.dedup(); + expected.truncate(5); + assert_eq!(ids.as_slice(), &expected); + } + } +} diff --git a/src/search/solver/bonus_tiers.rs b/src/search/solver/bonus_tiers.rs index ccfc0b9..a50ef62 100644 --- a/src/search/solver/bonus_tiers.rs +++ b/src/search/solver/bonus_tiers.rs @@ -1680,9 +1680,15 @@ impl JointCeiling { let (numerator, denominator) = if alpha * u + beta * w <= c { (u * w, 1) } else if c >= 2 * alpha * u { - (u * (c - alpha * u), beta) + let Some(numerator) = u.checked_mul(c - alpha * u) else { + return u32::MAX; + }; + (numerator, beta) } else if c >= 2 * beta * w { - (w * (c - beta * w), alpha) + let Some(numerator) = w.checked_mul(c - beta * w) else { + return u32::MAX; + }; + (numerator, alpha) } else { match c.checked_mul(c) { Some(square) => (square, 4 * alpha * beta), diff --git a/src/search/solver/final_chapter.rs b/src/search/solver/final_chapter.rs index 68ea1c1..0e1aca7 100644 --- a/src/search/solver/final_chapter.rs +++ b/src/search/solver/final_chapter.rs @@ -7,7 +7,7 @@ use crate::types::{DECK_SIZE, LiveSkillOrder, LiveType, ScoreTarget}; use crate::search::context::{SearchContext, SupportDeck}; use crate::search::dfs::SearchStats; -use crate::search::log_linear::{FeatureBox, LogLinearBound}; +use crate::search::log_linear::{FeatureBox, LogLinearBound, mul_up, sub_down, sum_up}; use crate::search::objective::{CeilingInputs, ObjectiveBound, ScoreCutoff}; use crate::search::skill_ceiling::{Composition, SkillCeiling}; use crate::search::types::{DeckResult, SearchParams}; @@ -367,13 +367,15 @@ impl GroupWeights { /// The leader's own terms. fn leader(&self, leader: &LeaderConst) -> f64 { - self.bound.constant - + self.bound.leader_skill * f64::from(leader.skill) - + self.bound.weigh( + sum_up([ + self.bound.constant, + mul_up(self.bound.leader_skill, f64::from(leader.skill)), + self.bound.weigh( leader.power, leader.skill, leader.base_bonus_const + leader.limited_bonus, - ) + ), + ]) } } @@ -1565,13 +1567,19 @@ impl CharacterSearchState<'_> { threshold: u64, ) -> f64 { let extra = extra_bonus_ceiling(&self.group_suffix[start], 1, prefix, &self.leader); - let fixed = self.leader_weight - + weights.bound.bonus * f64::from(extra) - + selected[..MEMBER_COUNT - 1] - .iter() - .map(|&group| weights.group[group]) - .sum::(); - self.log_cutoff(threshold >> 32) - fixed + let fixed = sum_up( + [ + self.leader_weight, + mul_up(weights.bound.bonus, f64::from(extra)), + ] + .into_iter() + .chain( + selected[..MEMBER_COUNT - 1] + .iter() + .map(|&group| weights.group[group]), + ), + ); + sub_down(self.log_cutoff(threshold >> 32), fixed) } #[inline(always)] @@ -1871,13 +1879,15 @@ impl CharacterSearchState<'_> { }; let remaining = MEMBER_COUNT - selected.len(); let extra = extra_bonus_ceiling(&self.group_suffix[start], remaining, prefix, &self.leader); - let value = self.leader_weight - + weights.bound.bonus * f64::from(extra) - + selected - .iter() - .map(|&group| weights.group[group]) - .sum::() - + weights.tail[start][..remaining].iter().sum::(); + let value = sum_up( + [ + self.leader_weight, + mul_up(weights.bound.bonus, f64::from(extra)), + ] + .into_iter() + .chain(selected.iter().map(|&group| weights.group[group])) + .chain(weights.tail[start][..remaining].iter().copied()), + ); let threshold_ep = threshold >> 32; weights .bound @@ -1907,18 +1917,20 @@ impl CharacterSearchState<'_> { self.ctx.extra_bonus_ub }; let open = depth + usize::from(candidate.is_some()); - let value = bound.constant - + bound.leader_skill * f64::from(self.leader.skill) - + bound.weigh( - partial.power, - partial.skill, - partial.base_bonus + partial.limited_sum + extra, - ) - + candidate.map_or(0.0, |terms| terms.weight(bound)) - + selected[open..] - .iter() - .map(|&group| weights.group[group]) - .sum::(); + let value = sum_up( + [ + bound.constant, + mul_up(bound.leader_skill, f64::from(self.leader.skill)), + bound.weigh( + partial.power, + partial.skill, + partial.base_bonus + partial.limited_sum + extra, + ), + candidate.map_or(0.0, |terms| terms.weight(bound)), + ] + .into_iter() + .chain(selected[open..].iter().map(|&group| weights.group[group])), + ); let threshold_ep = threshold >> 32; bound.excludes(value, threshold_ep, self.log_cutoff(threshold_ep)) } diff --git a/src/search/solver/numeric.rs b/src/search/solver/numeric.rs index 6a2c7b0..cae9abe 100644 --- a/src/search/solver/numeric.rs +++ b/src/search/solver/numeric.rs @@ -4,6 +4,7 @@ use crate::pool::{CardIdx, CardPool}; use crate::search::DeckResult; use crate::search::budget::SearchBudget; use crate::search::skill_ceiling::{Composition, SkillCeiling}; +use crate::search::small_ids::SmallestIds; use crate::search::{ SearchContext, SearchParams, SearchStats, TopKTracker, evaluate, placement, tuning, }; @@ -60,8 +61,8 @@ struct SimpleExactState<'a> { /// Skill target: [`SkillCeiling`] of every card, by pool index. skill_ceilings: Vec, /// For each position, the smallest distinct game ids of `cards[pos..]` - /// in ascending order, padded with `u16::MAX`. - suffix_small_ids: Vec<[u16; SMALL_IDS]>, + /// in ascending order, with an explicit occupied length. + suffix_small_ids: Vec>, global_power_max: u32, global_power_min: u32, global_skill_max: u32, @@ -645,15 +646,11 @@ fn is_free_slot_blocked(fixed_prefix: usize, depth: usize) -> bool { /// up to five ids already in the deck. const SMALL_IDS: usize = 2 * DECK_SIZE; -fn suffix_small_ids(pool: &CardPool, cards: &[CardIdx]) -> Vec<[u16; SMALL_IDS]> { - let mut table = vec![[u16::MAX; SMALL_IDS]; cards.len() + 1]; +fn suffix_small_ids(pool: &CardPool, cards: &[CardIdx]) -> Vec> { + let mut table = vec![SmallestIds::new(); cards.len() + 1]; for pos in (0..cards.len()).rev() { let mut ids = table[pos + 1]; - let id = pool.game_id(cards[pos]); - if !ids.contains(&id) && id < ids[SMALL_IDS - 1] { - ids[SMALL_IDS - 1] = id; - ids.sort_unstable(); - } + ids.insert(pool.game_id(cards[pos])); table[pos] = ids; } table @@ -666,19 +663,16 @@ fn suffix_small_ids(pool: &CardPool, cards: &[CardIdx]) -> Vec<[u16; SMALL_IDS]> /// only makes the result smaller. `None` when too few ids remain. fn smallest_public_set( selected: &[u16], - small_ids: &[u16; SMALL_IDS], + small_ids: &SmallestIds, slots: usize, ) -> Option<[u16; DECK_SIZE]> { - let mut set = [u16::MAX; DECK_SIZE]; + let mut set = [0; DECK_SIZE]; set[..selected.len()].copy_from_slice(selected); let mut len = selected.len(); - for &id in small_ids { + for &id in small_ids.as_slice() { if len == selected.len() + slots { break; } - if id == u16::MAX { - return None; - } if !selected.contains(&id) { set[len] = id; len += 1; diff --git a/src/search/solver/power.rs b/src/search/solver/power.rs index 0e8eeda..6827722 100644 --- a/src/search/solver/power.rs +++ b/src/search/solver/power.rs @@ -7,6 +7,7 @@ //! character-distinct decks runs against the one canonical tracker. use crate::pool::{CardIdx, CardPool}; use crate::search::budget::SearchBudget; +use crate::search::small_ids::SmallestIds; use crate::search::{ DeckResult, SearchContext, SearchParams, SearchStats, TopKTracker, evaluate, placement, }; @@ -241,7 +242,7 @@ impl PowerSearch<'_> { } let slots = DECK_SIZE - depth; let selected = &self.game_ids[..depth]; - let mut smallest = [u16::MAX; DECK_SIZE]; + let mut smallest = SmallestIds::::new(); for entry in entries[pos..] .iter() .take_while(|entry| entry.power >= least) @@ -250,22 +251,16 @@ impl PowerSearch<'_> { continue; } let id = self.pool.game_id(entry.card); - if id >= smallest[slots - 1] || selected.contains(&id) || smallest.contains(&id) { - continue; - } - let mut at = slots - 1; - while at > 0 && smallest[at - 1] > id { - smallest[at] = smallest[at - 1]; - at -= 1; + if !selected.contains(&id) { + smallest.insert(id); } - smallest[at] = id; } - if smallest[slots - 1] == u16::MAX { + let Some(tail) = smallest.as_slice().get(..slots) else { return true; - } + }; let mut set = [0u16; DECK_SIZE]; set[..depth].copy_from_slice(selected); - set[depth..].copy_from_slice(&smallest[..slots]); + set[depth..].copy_from_slice(tail); set.sort_unstable(); set > kth } diff --git a/src/search/tests/mod.rs b/src/search/tests/mod.rs index e183ef6..7be80c9 100644 --- a/src/search/tests/mod.rs +++ b/src/search/tests/mod.rs @@ -854,3 +854,5 @@ fn dfs_search_exact( assert_eq!(outcome.completion(), SearchCompletion::Complete); outcome.results } + +mod proof_audit; diff --git a/src/search/tests/proof_audit.rs b/src/search/tests/proof_audit.rs new file mode 100644 index 0000000..4890d1e --- /dev/null +++ b/src/search/tests/proof_audit.rs @@ -0,0 +1,279 @@ +//! Permanent counterexamples from the 2026-09-26 proof audit. +//! The oracle shares the leaf evaluator, but not pruning, placement or tracking. +use super::*; + +fn assert_complete_oracle(pool: &CardPool, context: &SearchContext, k: usize) { + let params = SearchParams { + top_k: k, + timeout_ms: 0, + }; + let actual = search(pool, context, ¶ms); + let (expected, _) = ExactOracle::new(pool, context).search(¶ms); + assert_eq!(actual.completion(), SearchCompletion::Complete); + assert_eq!( + actual.results, expected, + "target={:?} k={k}", + context.target + ); +} + +#[test] +fn maximum_public_id_participates_in_canonical_top_k() { + // Before the fix, rank 20 had the right score but the wrong public set: + // [101,103,104,106,65535], instead of [101,102,104,107,65535]. + let rows = [ + (101, 107), + (106, 107), + (104, 105), + (102, 109), + (107, 108), + (105, 101), + (103, 110), + (65535, 105), + ]; + let cards: Vec<_> = rows + .iter() + .enumerate() + .map(|(i, &(id, power))| { + let mut card = skill_card(id, i as u8 + 1, power, (power - 80) as u8); + card.attr = 1; + card.unit_mask = 1; + card + }) + .collect(); + let pool = build_pool(&cards); + for target in [ScoreTarget::Power, ScoreTarget::Skill, ScoreTarget::Mysekai] { + let mut context = ready_ctx(&pool, target); + if target == ScoreTarget::Mysekai { + context.live_type = LiveType::Mysekai; + } + for k in [1, 3, 8, 20, 40, 56] { + assert_complete_oracle(&pool, &context, k); + } + if target == ScoreTarget::Power { + // Also reach the generic numeric solver, in both directions. + context.power_total_cap = Some(10_000); + for minimize in [false, true] { + context.minimize = minimize; + for k in [1, 20, 56] { + assert_complete_oracle(&pool, &context, k); + } + } + } + } +} + +#[test] +fn maximum_public_id_randomized_ties_match_ordered_oracle() { + let mut state = 0xA110_2026_0926_u64; + for _case in 0..24 { + let cards: Vec<_> = (0..8_u16) + .map(|i| { + state = state.wrapping_mul(6364136223846793005).wrapping_add(1); + let power = 100 + ((state >> 32) % 12) as u32; + let id = if i == 7 { + u16::MAX + } else { + 101 + ((i * 5) % 7) + }; + let mut card = skill_card(id, i as u8 + 1, power, (power - 80) as u8); + card.attr = 1; + card.unit_mask = 1; + card + }) + .collect(); + let pool = build_pool(&cards); + for target in [ScoreTarget::Power, ScoreTarget::Skill] { + let context = ready_ctx(&pool, target); + for k in [1, 8, 20, 56] { + assert_complete_oracle(&pool, &context, k); + } + } + } +} + +fn cancellation_pool(base_a_x10: u16) -> CardPool { + let ids = [100_u16, 200, 1001, 1006, 1009, 1011]; + let mut builder = PoolBuilder::new(ids.len() as u16); + for (i, &id) in ids.iter().enumerate() { + let dense = i as u16; + let character = if i < 2 { 1 } else { i as u8 }; + let (values, lut) = encode_power(90_000); + builder.set_power_values(dense, values); + builder.set_power_lut(dense, lut); + builder.set_power_max(dense, 90_000); + builder.set_skill( + dense, + SkillSlot { + skill_type: 0, + value: 100, + }, + ); + builder.set_skill_min(dense, 100); + builder.set_skill_max(dense, 100); + builder.set_skill_reference(dense, 100); + builder.set_event_bonus( + dense, + EventBonusExact::from_x10( + if i == 0 { + base_a_x10 + } else if i == 1 { + 625 + } else { + 0 + }, + 0, + ), + ); + builder.set_game_id(dense, id); + builder.set_char_id(dense, character); + builder.set_attr(dense, 1); + builder.set_unit_mask(dense, 1); + builder.mark_char(character, dense); + builder.mark_attr(1, dense); + builder.mark_unit(0, dense); + } + builder.freeze() +} + +fn cancellation_context(pool: &CardPool) -> SearchContext { + let mut context = ready_ctx(pool, ScoreTarget::Mysekai); + context.live_type = LiveType::Mysekai; + context.is_world_bloom = true; + context.is_final_chapter = true; + context.event_type = Some(EventType::WorldBloom); + context.support_deck = SupportDeck { + cards: vec![ + (100, 7.05), + (200, 5.45), + (300, 2.05), + (301, 0.8), + (302, 0.5), + ], + count: 4, + }; + context.extra_bonus_ub = 16; + context.forced_leader_character_id = Some(2); + context.fixed_character_ids = vec![2]; + context.support_decks_by_character = vec![context.support_deck.clone(); 27]; + context +} + +#[test] +fn support_compensation_preserves_actual_floating_point_top_one() { + let pool = cancellation_pool(641); + let context = cancellation_context(&pool); + let deck_a = [ + CardIdx::new(2), + CardIdx::new(0), + CardIdx::new(3), + CardIdx::new(4), + CardIdx::new(5), + ]; + let deck_b = [ + CardIdx::new(2), + CardIdx::new(1), + CardIdx::new(3), + CardIdx::new(4), + CardIdx::new(5), + ]; + // Equal over decimal arithmetic, unequal under the unchanged evaluator. + assert_eq!(leaf_evaluate(&pool, &context, &deck_a), 1728); + assert_eq!(leaf_evaluate(&pool, &context, &deck_b), 1729); + let dominance = eliminate_dominated(&pool, &context); + assert_eq!(dominance.after, dominance.before); + for k in [1, 2, 8] { + assert_complete_oracle(&pool, &context, k); + } + for target in [ScoreTarget::Score, ScoreTarget::Bonus, ScoreTarget::Mysekai] { + for final_chapter in [false, true] { + let mut other = context.clone(); + other.target = target; + other.is_final_chapter = final_chapter; + other.live_type = if target == ScoreTarget::Mysekai { + LiveType::Mysekai + } else { + LiveType::Multi + }; + other.skill_scores[1] = [0.2; 6]; + for k in [1, 2] { + assert_complete_oracle(&pool, &other, k); + } + } + } +} + +#[test] +fn strict_support_surplus_still_allows_certified_dominance() { + let pool = cancellation_pool(642); + let context = cancellation_context(&pool); + let dominance = eliminate_dominated(&pool, &context); + assert_eq!(dominance.after, dominance.before - 1); + for k in [1, 2] { + assert_complete_oracle(&pool, &context, k); + } +} + +#[test] +fn malformed_support_profiles_do_not_certify_dominance() { + let pool = cancellation_pool(642); + for malformed in [ + vec![(100, 7.05), (100, 5.45)], + vec![(100, 1.0), (200, 2.0)], + vec![(100, f64::NAN)], + vec![(100, -1.0)], + ] { + let mut context = cancellation_context(&pool); + context.support_deck.cards = malformed; + context.support_decks_by_character = vec![context.support_deck.clone(); 27]; + let dominance = eliminate_dominated(&pool, &context); + assert_eq!(dominance.after, dominance.before); + } +} + +#[test] +fn event_upper_bound_remains_monotone_outside_the_legal_leaf_range() { + use crate::search::objective::ObjectiveBound; + let pool = cancellation_pool(641); + let mut context = ready_ctx(&pool, ScoreTarget::Score); + context.event_type = Some(EventType::Marathon); + context.music_rate_pct = 2_000_000; + for live_type in [LiveType::Solo, LiveType::Multi, LiveType::Cheerful] { + context.live_type = live_type; + let objective = ObjectiveBound::from_context(&context); + let mut previous = 0; + for live in [0, 1_800_000, 100_000_000, 1_000_000_000, i32::MAX] { + let current = objective.calc_event_point_bound(live, 0); + assert!( + current >= previous, + "{live_type:?}: {live} => {current} < {previous}" + ); + previous = current; + } + assert_eq!(previous, i32::MAX); + } +} + +#[test] +fn unrepresentable_joint_coefficients_disable_only_the_optional_bound() { + use crate::search::objective::{LiveProduct, ObjectiveBound}; + let pool = cancellation_pool(641); + let mut context = ready_ctx(&pool, ScoreTarget::Score); + context.live_type = LiveType::Multi; + context.skill_scores[1] = [1e15; 6]; + assert!( + ObjectiveBound::from_context(&context) + .live_product() + .is_none() + ); + let product = LiveProduct { + honor: 0, + intercept: 1, + leader: 1, + skill: 1, + constant: i64::MAX, + divisor: 1, + floor: 0, + }; + assert_eq!(product.live(i128::MAX, 2), u32::MAX); +} diff --git a/tests/benchmark_proof.rs b/tests/benchmark_proof.rs index 4b60f05..3fac81d 100644 --- a/tests/benchmark_proof.rs +++ b/tests/benchmark_proof.rs @@ -128,13 +128,10 @@ fn testdata_corpus_layers_are_classified() { } #[test] +#[ignore = "requires external masterdata; run explicitly with configured paths"] fn rust_bruteforce_matches_exact_on_full_testdata_pools() { - let Some(masterdata_hint) = usable_masterdata_hint() else { - eprintln!( - "skip BF proof: set ALLIUM_MASTERDATA_CN/JP or provide ../masterdata_* from repo root" - ); - return; - }; + let masterdata_hint = usable_masterdata_hint() + .expect("external proof requires ALLIUM_MASTERDATA_CN/JP or ../masterdata_*"); eprintln!( "BF proof using masterdata hint: {}", masterdata_hint.display() @@ -208,15 +205,14 @@ fn rust_bruteforce_matches_exact_on_full_testdata_pools() { /// 故单列一个用例锁住该 fixture（仍受 ALLIUM_BF_CANDIDATE_LIMIT 控制， /// 按 issue 验证命令以 ALLIUM_BF_CANDIDATE_LIMIT=100000000 运行）。 #[test] +#[ignore = "requires external masterdata; run explicitly with configured paths"] fn rust_bruteforce_matches_exact_top_k_on_issue2_fixture() { const ISSUE2_CASE: &str = "mass_392500_score_multi_ev"; - if usable_masterdata_hint().is_none() { - eprintln!( - "skip issue #2 Top-K proof: set ALLIUM_MASTERDATA_CN/JP or provide ../masterdata_* from repo root" - ); - return; - } + assert!( + usable_masterdata_hint().is_some(), + "external issue #2 proof requires ALLIUM_MASTERDATA_CN/JP" + ); let root = testdata_dir("real"); let manifest = load_manifest(&root).unwrap(); @@ -231,13 +227,11 @@ fn rust_bruteforce_matches_exact_top_k_on_issue2_fixture() { let game = game_for_region(¶ms.region).unwrap(); let (pool, ctx) = build_card_pool(&user, &game.as_ref(), ¶ms).unwrap(); let candidates = combination_count(pool.count(), allium_deck::DECK_SIZE); - if candidates > bf_candidate_limit() { - eprintln!( - "skip issue #2 Top-K proof: {candidates} candidates exceed ALLIUM_BF_CANDIDATE_LIMIT={}", - bf_candidate_limit() - ); - return; - } + assert!( + candidates <= bf_candidate_limit(), + "issue #2 needs {candidates} candidates; increase ALLIUM_BF_CANDIDATE_LIMIT (currently {})", + bf_candidate_limit() + ); let (exact, _) = search_instrumented(&pool, &ctx, &search_params); let (brute, _) = brute_force_search(&pool, &ctx, &search_params); @@ -245,13 +239,10 @@ fn rust_bruteforce_matches_exact_top_k_on_issue2_fixture() { } #[test] +#[ignore = "requires external masterdata; run explicitly with configured paths"] fn rust_bruteforce_matches_exact_on_large_filtered_pools() { - let Some(masterdata_hint) = usable_masterdata_hint() else { - eprintln!( - "skip large filtered BF proof: set ALLIUM_MASTERDATA_CN/JP or provide ../masterdata_* from repo root" - ); - return; - }; + let masterdata_hint = usable_masterdata_hint() + .expect("external filtered-pool proof requires ALLIUM_MASTERDATA_CN/JP"); eprintln!( "large filtered BF proof using masterdata hint: {}", masterdata_hint.display()