性能与语义审计

本指南记录了对构成仓库性能基线（发布版本 0.7.1）的各项优化的审计。它列出经过优化的路径、评审中发现的语义修复、每条快路径与通用路径返回完全相同结果的证明，以及性能结论的证据边界。此后的工作（包括当前分支）没有新增性能测量，因此本审计仍是这些优化路径的参考依据。

范围

审计覆盖发布 0.7.0 之后的提交 69084bc、7904016、23005ed 与 4fd41ad，以及在 0.7.1 发布评审期间加入的 GDA 系数辅助函数和区间回归修复。审计将观察到的行为、规范要求、实现选择和验收证据视为相互独立的事实。

问题矩阵

行	分类	观察结果	预期	变更	验收证据
GDA 系数内核	实现缺口	GDA 快路径增加了小表示、仅求余数的除法和半幂比较	系数恒等式、同值类、标志、陷阱和粘滞状态均不变	使用规范的 `GdaCoeff` 运算，并保留共享的 GDA 收尾函数（finalizer）	93 个包测试、8 个前端测试、`official` 64,986/64,986、`official0` 16,124/16,124
IEEE decimal 路径	语义风险优化	精确除法与有界除法路径跳过了重复的通用计算	精确十进制结果、舍入、量子、标志和特殊值均与 IEEE 行为一致	用有限域、因子、边界和收尾谓词保护快路径；不满足时回退	94 个包测试、四目标 IEEE 15,763/15,763
Binary IEEE 路径	语义风险优化	精确最高位排序、拆分的 round/sticky 位提取以及系数分派取代了更宽的中间计算	上下文下的值、舍入、标志、带符号零以及交换格式位模式完全相同	保留精确系数构造，并让每个结果都经过上下文舍入	68 个包测试、binary 7,464,503/7,464,503
区间端点分派	语义偏差，已修复	优化后的 `pown` 在不同符号区域间复用端点方向；负区间可能得到 $\underline{y} > \overline{y}$ 或损失一个 ulp	返回的每个区间都有序，且包含精确像集	按单调性选择端点，并对每个候选向外舍入；增加负半轴测试	42 个包测试，整数幂 174/174，严格 ITF1788 4,656/4,656
发布文档	文档缺口	0.7.0 仍被标为当前基线	当前引用指向新基线；历史记录保留在变更日志中	更新元数据并加入本审计	`python3 tools/doc_quality.py`

优化证明

精确系数路径

对系数 $a \ge 0$ 和除数 $d > 0$ ，余数为

r = a - \left\lfloor \frac{a}{d} \right\rfloor d, \qquad 0 \le r < d .

仅求余数的内核与同时求商和余数的内核返回相同的 $r$ ，因此保留了每个可观察的余数以及欧几里得算法的每一步。GDA 半幂谓词依据最高十进制位及其尾部是否非零，将 $a$ 与 $5 \cdot 10^{\,\operatorname{digits}(a) - 1}$ 进行比较；这是精确比较，而非浮点估计。

IEEE 十进制精确除法路径首先约去 $g = \gcd(c_x, c_y)$ 。商 $c_x / c_y$ 具有有限十进制展开，当且仅当约分后的分母 $c_y / g$ 不含 2 与 5 以外的素因子：

\frac{c_x}{c_y} = \frac{c_x / g}{2^{i} 5^{j}} = \frac{(c_x / g) \cdot 2^{k-i} 5^{k-j}}{10^{k}}, \qquad k = \max(i, j).

只有在这种情况下才走该路径。它构造精确的系数和指数，并调用现有的收尾函数；只要因子、边界或特殊值的前提条件有任何一项不满足，就回到通用算法。该优化改变的是到达精确值的路线，而不是 IEEE 的舍入或标志规则。

Binary contextual 路径

对有限二进有理值 $c \cdot 2^{e}$ ，binary_exact_top(c, e) 是最高置位的指数，即 $e + \operatorname{bitlen}(c) - 1$ 。比较这些最高位等价于在对齐之前比较绝对值，对末尾二的幂次不同的系数同样成立。当丢弃一个相距很远的加数时，拆分操作保留第一个被丢弃的位（round 位）以及其后所有位的 OR（sticky 位）。这两者恰好就是舍入决策的输入：设截断后的绝对值为 $t$ ，被丢弃的部分为一个 ulp 的 $f \in [0, 1)$ 倍，则

\text{round bit} = [f \ge \tfrac{1}{2}], \qquad \text{sticky bit} = [f \notin \{0, \tfrac{1}{2}\}],

并且每个 IEEE 舍入方向都是 $t$ 的末位、符号以及这两个位的函数。因此快路径提供相同的舍入输入，同时从不显式构造巨大的对齐系数。

有向区间路径

区间运算必须保持包含不变量 $f(X) \subseteq [\underline{y}, \overline{y}]$ 与存储不变量 $\underline{y} \le \overline{y}$ 。对精确的端点候选 $y$ ， $\operatorname{RD}(y)$ 是有效的下界证书， $\operatorname{RU}(y)$ 是有效的上界证书。pown 的各个分支使用 $x \mapsto x^{n}$ 的如下单调性表：

数值域	$n > 0$ 为奇数	$n > 0$ 为偶数	$n < 0$ 为奇数	$n < 0$ 为偶数
负半轴	递增	递减	递减	递增
正半轴	递增	递增	递减	递减
含零区间	端点顺序	从 $0$ 到向外舍入后的最大值	极点：拆分或 Entire	极点：拆分或 Entire

实现先选出数学端点，再施加该端点角色所要求的舍入方向。对于跨越零且 $n > 0$ 为偶数的区间，两个有限极值候选都向上舍入以形成上界。随后 quantize_interval 再向外舍入一次。该证明仅限于已声明的运算与精度契约，不对尚未支持的逆运算作任何断言。

性能证据

领域	测量	解释
二进制、十进制、GDA 与区间内核	`just bench all --target native`	四套 Maremark 基准都生成了有效的产物
二进制平方策略	`just bench auto-tune --target native`	一份针对特定目标的策略产物；原始观测可能非单调，并不构成通用阈值
IEEE 与 GDA 快路径	基准测试包的测试以及符合性关卡	只有在语义判定（oracle）保持全部通过时，快路线才可采用
区间端点分派	`src/bench/ball_float` 与 strict ITF1788	只有有序且向外舍入的包络成立时，降低成本才可接受

生成的产物位于 .tmp/bench/ 之下，不作为 API 数据发布。在提升交叉点阈值之前，请在目标硬件上重新运行这些命令。该工作负载只是关于被审计代码树的证据；它并不证明每个发布版本都有加速、不同目标之间性能等价，也不提供延迟上界。

验收矩阵

检查	结果
`sh tools/run_moon_clean_exec.sh test src/decimal_gda --target native --deny-warn --frozen --no-parallelize`	93/93 通过
`sh tools/run_moon_clean_exec.sh test src/decimal --target native --deny-warn --frozen --no-parallelize`	94/94 通过
`sh tools/run_moon_clean_exec.sh test src/bin_float --target native --deny-warn --frozen --no-parallelize`	68/68 通过
`sh tools/run_moon_clean_exec.sh test src/ball_float --target native --deny-warn --frozen --no-parallelize`	42/42 通过
`just gate binary 8`	7,464,503/7,464,503 通过
`just gate decimal 8`	15,763/15,763 通过
`just gate decimal_gda 8`	64,986/64,986 与 16,124/16,124 通过
`just gate interval 8`	4,656/4,656 通过
`python3 tools/doc_quality.py`	通过

这些计数描述的是被审计的代码树。此后各关卡已有扩展（二进制关卡现已运行完整的 IEEE 运算矩阵）；当前的结论见验证。

评审者自查

贡献：通过。审计记录了具体的优化边界和一个已修复的语义故障，而非无法解释的加速。
清晰度：通过。每个证明都分别说明表示、单调性、舍入方向和证据。
实验强度：需要复现。原生产物有效，但在提升阈值之前，应重复那些噪声较大的自动调优观测。
完整性：对声明的固定语料通过；它并未覆盖每一个标准运算或每一种实数输入。
可靠性：在修复负半轴回归并通过完整的 IEEE 1788 关卡之后，对所覆盖的分支通过。

结论与证据对照

声明	证据	状态
快速系数路线保持所声明的数值结果	精确内核恒等式、包测试、IEEE 与 GDA 符合性	在声明 API 与前置条件内支持
区间 `pown` 保持有序的向外包络	单调性表、负半轴回归、4,656 条 strict ITF1788	对所声明的正向区间运算成立
优化路径已经过性能审计	native Maremark `all` 与 `auto-tune` artifact	作为测量证据成立，而非通用的速度结论
所有目标和运算都具有等价的性能	没有成对的跨目标产物	不作此结论

限制

语义结论受限于固定语料、公开运算、特定目标的精度规则以及显式的回退契约。0.6.1 的初等函数清单仍是初等函数性能关卡的比较基线，0.7.1 是其候选版本。不会仅为改善某个基准测试而更改任何公开 API、舍入规则、错误信号或包络契约。