fix(search): close proof-audit counterexamples and certify pruning arithmetic

[nichinichisou0609]

审计结论与范围

基于 165ff63525be2c13d4ae9b6417924e0b789e5ff6，修复两处已复现的 Complete 错误结果，并处理修复过程中发现的数值范围、输入表示和证明缺口。不修改 leaf evaluator，不靠改变评分公式让反例通过；不合并 main。

详细推导与复现见新增 docs/proof-audit-20260926.md，以及更新后的 docs/pruning-proof.md / docs/exactness-proof.md。

已复现并修复

1. 支援抵扣错误删除真实 Top-1

六卡反例中，A 的主卡基础加成为 64.1%，B 为 62.5%，支援表为 (100,7.05),(200,5.45),(300,2.05),(301,0.8),(302,0.5)，计入 4 张。实数下两队都是 72.9%，实际 f64 求值却分别给出 MYSEKAI 1728 / 1729。旧终章搜索删除 B，返回 Complete / 1728；完整有序穷举为 1729。

现在区分两种可证明的替代：支援次序统计量不下降时直接用浮点单调性；需要基础加成抵扣时，向外计算严格余量，且余量必须超过已推导的两队舍入误差。实数恰好抵消不能再授权删除。

2. 公共卡 ID 65535 与空槽哨兵冲突

八卡 Power Top-20 旧结果第 20 名为 534 / [101,103,104,106,65535]，正确 canonical 集合为 534 / [101,102,104,107,65535]。

Power 和通用 numeric 的最小 ID 前沿改用显式 occupied length；65535 仍是合法 ID，没有新增候选裁剪或缩小合法 ID 范围。

其他修复与补证

• 对数线性剪枝保留，但不再依赖固定 1e-9 / “几个 ulp”假设。采用向外区间运算、带明确余项的 atanh 级数计算 logarithm、端点外扩、可认证弦斜率；近退化区间无法证明时回退。所有消费者的乘法、求和及最后一组阈值减法也按正确方向取整。
• 活动分阈值反推会探测超过合法叶子范围的值。活动分上界统一使用 i128 阶段计算及最终单调截断，避免窄化回绕；可选 joint bound 的大系数和有理式使用 checked arithmetic，溢出仅禁用更紧上界。
• 支援种子在主卡过滤前就会构建：现在先检查公共 ID，再窄化和去重，防止被主队排除的非法 ID 在支援中别名为 65535；独立支援接口使用相同检查。原始角色 ID 在准备阶段过滤前验证。
• Top-K 根集合恢复改为完整 canonical order 的计数论证，明确培养态组合必须先枚举再做逆支配分数剪枝。
• 修正合法叶子范围与松弛/反推探测范围的混淆；舍入依赖路径包含吸分技能和 Multi Average，而非假定技能总是整数或四分之一刻度。
• 三个依赖外部 masterdata 的证明测试改为显式 ignored；显式运行却缺少数据时失败，不再假报通过。PR/push CI 新增两个穷举矩阵 gate。

本轮已经完成的验证

Native x86-64，Rust 1.98.1，单逻辑核 CPU quota 80%，内存 1536 MiB，无 swap：

• cargo fmt --all --check：通过。
• cargo clippy --locked --all-features --all-targets -- -D warnings：通过。
• cargo test --locked --release --all-features：308 单元测试通过，8 ignored；1 集成分类测试通过，3 外部数据测试 ignored；1 doctest 通过。
• long_exact_all_scene_property_matrix：256 cases / 3840 comparisons 通过。
• ALLIUM_VALIDATION_ORACLE_SEEDS=16 ... validation_oracle_extended：4608 contexts / 18432 Complete searches / 13,765,632 ordered assignments / 287,232 compared rows 通过。

独立 Server / MSRV / WASM 检查另行记录，未完成前不计作通过。GitHub CI 以实际 check 状态为准。

证据边界

两个 wrong-result 反例是真正的修复前失败、修复后通过。旧 log bound 的问题是未闭合证明义务，不冒充第三个已复现漏解。Oracle 不复用剪枝、placement、tracker，但共享叶子评分实现；这些结果不是对游戏公式的独立认证，也不是全程序机器检查证明。真实账号语料、真实浏览器发布验收和生产长尾性能不从合成测试推出；本 PR 不声称满足 20 ms 指标或“已经找到所有可能的 bug”。

[nichinichisou0609]

补充验证结果

当前 PR HEAD：84a03dab836cf2225ae50226282af99a05f7059a。功能代码在 5b302d09df1bfb80154d56c9e1c46a4b7519ae46；后一个提交只更新证明细节和验证记录，没有修改功能代码。之前的 188cba1 仅因提交正文单行超过 100 字符被 commitlint 拒绝，修正说明时确认代码树完全相同；当前提交格式检查已通过。

已完成

检查	实际结果
Native release 单元测试	308 passed / 0 failed / 8 ignored
默认集成测试	1 个语料分类测试通过；3 个外部 masterdata 证明明确 ignored
Doc test	1 passed
全场景矩阵	256 cases / 3,840 comparisons，全通过
扩展 WL / Final oracle	16 seeds，4,608 contexts，18,432 Complete searches，13,765,632 ordered assignments，287,232 compared rows，全通过
Server 独立 workspace	本地 13 单元测试 + 13 HTTP/engine parity 测试通过；GitHub CI 的 release 测试和 default/jemalloc/mimalloc lint 也通过
MSRV 1.89	GitHub CI 的 cargo check --all-features --locked 通过
真实 WASM 构建	Windows 上以 Rust 1.94.0 完成 locked wasm32-unknown-unknown release 构建，使用版本匹配的 wasm-bindgen 0.2.126 生成 Node bindings
真实 WASM 执行	Node 22.17.0：9 个合成输入 × 3 次重复 = 27 次调用，288 行结果与 native CLI 一致

WASM 对照涵盖 Power、Power 最小化、Skill、Solo Average Score、Auto Score、Multi 活动 Score、Cheerful Score、MYSEKAI、Bonus。输入由仓库的 synthetic fixture 派生，保留完整合成 masterdata，账号限制为 8 个角色，并一致地引入合法公共 ID 65535。比较完整整数目标值时先保留为十进制字符串，避免 JS Number 丢失整数精度；同时比较队伍顺序、综合力、技能、培养态字段及 completion。未载入 masterdata 时也验证了显式报错。

这些是 9 个不同输入，不是 27 个独立样本。WASM workspace 的 native 编译包含 0 个测试，不被算作实际 WASM 执行；实际执行来自上述 Node 模块验证。没有声称完成真实浏览器、真实账号语料或生产延迟验收，也没有据此证明 20 ms 指标。

扩展矩阵 oracle digest：6c7ca192360864cb。验证命令、修复位置和证明边界已写入 docs/proof-audit-20260926.md。PR 未合并；最新 HEAD 的各平台 CI 状态以 Checks 页面实际结果为准。

[nichinichisou0609]

合并后的独立证明复审：仍不能通过

固定审计快照：5c6dff7387e57384b9b2c989ab4f535cdd74f098（当前 main、PR #43 的 squash merge）。只在独立副本添加测试，没有修改生产算法或评分器，也没有推送新代码。本轮找到以下四项新缺陷，不能由上一轮或本轮绿色矩阵推出全域精确性。

R1 / 高优先级：近似 tick 判定被误当作精确运算闭包，公开 engine 返回 Complete 空集

位置：src/search/solver/bonus_tiers.rs:503–524 的 ticks / tick_scale、约 608–614 的 exact_slack、约 1304–1310 的 selected slack 处理。失效证明：docs/pruning-proof.md §17.2 的 Exact slack。

令 δ = 6/2^26。支援条目 2−δ 和 1+δ 均通过近似整数刻度判定，分别得到 [20,20] / [10,10]；然而其差的负贡献 −(1−2δ) 得到 [-10,-9]，不是精确整数。代码仍令 exact_slack=true，在已选贡献中把 slack 上端点当精确值，可能抬高下界并错误判不可达。

低层五卡样例：唯一合法主队 [100,101,200,201,202]、零主卡加成，count=4 的支援表为 [(100,2−δ),(101,2−δ),(102,2−δ),(103,2−δ),(104,1+δ),(105,1+δ)]。实际剩余支援精确为 2(2−δ)+2(1+δ)=6，numeric_domain 接受，ordered oracle 找到一队，默认 search_targets 返回 Complete / []，没有访问叶子。

进一步已通过未修改的公开建池和 engine复现：25 张拥有卡，普通 WL2 event 176，正常 count=20；4 条高支援 2−δ、16 条 1.5、2 条替补 1+δ、3 条零支援。固定主队移除两条高支援和三条零支援，真实支援为 2(2−δ)+16×1.5+2(1+δ)=30.0。build_card_pool 成功，summarize_deck 为30.0%，oracle 命中30档；engine::recommend 却返回 Complete / []。

这不是因手工构造不满足 handler 前提而产生的假反例，也不是最终显示小数误差。数据是合成的，不声称当前真实主数据含该值。相关 fuzzy tick / exact_slack 代码在 PR #43 之前已经存在，不将其误报为本 PR 新引入的回归。

修复义务：对派生 loss/base/refill/excess 传播保守区间，或者提供覆盖整条运算链的精确证书；近似整数的加减运算不能自动获得精确性。不能通过给 leaf 取整或改变“精确命中档位”的含义规避反例。

R2 / 高优先级：结构体 BuildParams 未验证 Specific 排列

src/handler/validate.rs:207–216 只判断 Some 是否存在，未校验0..4且互异。公开建池实测接受 [0,0,0,0,0]、[0,1,2,3,6] 和 [usize::MAX,1,2,3,4]。不是直接改写 SearchContext，而是正式 handler 输出非法上下文。

src/search/evaluate.rs:755–768 随后用 original.get_unchecked(order[i]) 访问长度6的数组。越界值到达此处会违反 unsafe 前提。本轮只执行建池拒绝性测试，没有调用非法索引叶子，也没有宣称已观察到内存破坏。 应把排列校验放入共享的 validate_build_params，不能只依赖 JSON parser。

R3 / 中优先级：WASM JSON 先 u64→usize 截断、后检查范围

src/engine.rs:757–802 的数组分支先 value as usize，再判断 <5。实际 JSON [4294967296,4294967297,4294967298,4294967299,4294967300] 在 native x86-64 被拒绝；在 WASM32 变成 [0,1,2,3,4] 并返回 Complete，与合法输入结果相同。

已经实际执行 Node 22.17.0。复用上一轮已构建模块，本轮未重新构建；确认对应 src/wasm/Cargo 源码与本轮 main 完全相同，engine.rs SHA256=9c9f5fe4003ab98dc976ac8b10a96803f14aad00ea58e6c617e8a9098148cd78。模块 SHA256=cea5577550252e90c72f935aa9532eaa5caa7f0092f6507c6f5d83d53641c18b。

应在原始 u64 上检查范围，再 checked-convert；该具体样例截断后仍界内，不与R2的越界风险混为一谈。

R4 / 中优先级：from_whole 在检查前 u16 乘法回绕

src/pool/types.rs:133–142 的 EventBonusExact::from_whole(6554,0) 在 release 实测返回 EventBonusExact { base_x10:4, limited_x10:0 }，而非文档保证的范围错误/panic。6554×10 先回绕成4，from_x10只能检查回绕后的值。应宽整数乘法和范围检查之后再窄化。尚未证明正常 handler 会调用此构造器制造线上错队，这是公共表示 API 缺陷。

本轮实际验证

• 新增 Rust 审计组：1 passed / 4 failed。R1含低层/公开engine两个失败用例；R2、R4各一个。R3另有实际WASM/native差异验证，因此不把失败函数数误当成独立搜索漏解数。
• 原有单元测试重跑：308 passed，8 ignored；1个语料分类集成测试、1个doctest通过，外部masterdata依赖测试仍明确ignored。
• 全场景矩阵重跑：256 cases / 3840 comparisons，通过。
• 16-seed WL/Final矩阵重跑：4608 contexts / 18432 Complete searches / 13765632 assignments / 287232 compared rows，通过，digest=6c7ca192360864cb。
• 新增标准小数支援档位差分：176次默认/eager路径比较通过，不是176个独立输入。
• 原新增logarithm区间实现：用独立Decimal110位精度检查4105个binary64输入，零反例，包括subnormal/normal边界、1和2的相邻值。

本轮没有发现原SmallestIds/严格支援抵扣回归再次失败，也未找到新log区间实现的反例。但R1已推翻当前“受支持输入Complete即精确Top-K”的全局结论，R2说明handler尚未真正建立unsafe叶子依赖的全部前提。新增测试补丁、原始日志和审计报告另有证据包；没有修改评分器以消除失败。

修复优先级：R1、R2先阻断；R3统一跨架构输入语义；R4补表示边界。真实账号数据、真实浏览器和性能分布未在本轮认证。