frontend/mpfr_expr 设计

设计目标

GNU MPFR 能在任意精度、任意舍入方向下计算初等函数的正确舍入结果。¹1 L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, P. Zimmermann, “MPFR: A multiple-precision binary floating-point library with correct rounding”, ACM TOMS 33(2), 2007. 本包将 MPFR 的输出转化为针对 bin_float 的可执行检查：一行通过即表明，对于该输入、精度和舍入模式，bin_float 返回了正确舍入的结果（以及正确的异常标志）。它是一个纯库；数据文件及其来源位于 testdata/bin_float/，生成器位于 tools/。

数学背景

正确舍入

设 $\mathbb{F}_p$ 为具有 $p$ 位有效数字且指数无界的二进制数集合，$\circ_{p,\rho}$ 为沿方向 $\rho$ 舍入到 $\mathbb{F}_p$。对于实函数 $f$ 和 $x \in \mathbb{F}_q$，正确舍入结果为

$$y = \circ_{p,\rho}\bigl(f(x)\bigr), \qquad \text{inexact} \iff f(x) \notin \mathbb{F}_p .$$

MPFR 返回 $y$ 以及一个三值结果（ternary value），其符号表明 $y$ 小于、等于还是大于 $f(x)$；生成器将其转换为 inexact 字段。在特殊点上适用 IEEE 754 的规则：无效运算（例如 $\sqrt{-1}$、$\ln(-1)$）返回 NaN 并置 invalid 标志，由有限操作数得到的精确无穷结果（$\ln 0 = -\infty$）则触发除以零。²2 IEEE 754-2019，第 7.2 条（无效运算）和第 7.3 条（除以零），以及关于推荐初等函数的第 9.2 条。

一行数据断言了什么

每种格式固定了 $f$、输入 $x$、目标精度 $p$ 和方向 $\rho$，并记录 MPFR 的 $y$（及标志）。执行器在 BinaryContext::unbounded(p, rounding=ρ) 中求值对应的 bin_float 方法，并检查：

格式	值检查	标志检查
平方根	$\hat y = y$，作为 BinFloat 值比较（==）	无
整数幂 $x^n$	$\hat y = y$ (==)	inexact 相等；无 underflow、overflow、division by zero、invalid
初等函数	$\hat y \simeq y$ (compare == 0)	inexact、invalid、division by zero 相等；无 underflow、overflow

BinFloat 上的 == 比较的是存储表示，而对于给定的值和精度，该表示是规范的，因此它能区分 $+0$ 与 $-0$ 以及 NaN 载荷。compare == 0 是数值相等的扩展：任意 NaN 与任意 NaN 比较相等，且 $+0 = -0$。

设计决策

无界指数范围

MPFR 的默认指数范围远宽于任何 IEEE 格式，数据中包含诸如由 binary64 次正规数范围输入计算得到的 $2^{-563}$ 之类的结果。在无界上下文中执行可以单独测试有效数字的舍入：范围效应（上溢、下溢、次正规数）由 TestFloat 语料通过 testfloat_expr 覆盖，那里的格式具有真实的界限。因此，MPFR 行中出现的下溢或上溢标志即为失败：它只可能来自缺陷。

以 512 位读取输入

输入以十六进制书写，是精确的二进制数。以 512 位读取初等函数和幂运算的输入，可以使所有有效位数不超过 512 的输入保持精确，从而使检查针对的是 $f$，而不是 $x$ 的解析。平方根格式自带输入精度，并按该精度读取。

初等函数行采用数值比较

初等函数矩阵针对 29 个函数生成，覆盖 binary32/64/128 精度和全部六种舍入模式。其中期望的 NaN 不携带载荷信息，而 IEEE 754 将生成的 NaN 的载荷交由实现决定，因此比较时将所有 NaN 视为相等。同样的数值比较也将 $+0$ 与 $-0$ 视为相同；因此这些行不检查精确零结果的符号。

认证失败即为失败

bin_float 以经过认证的误差界和有界的细化循环来求值初等函数；当它无法认证舍入时，会返回错误而不是一个可能错误的值。执行器将这种错误计为一个失败行，并附带专门的消息，因此一次语料运行同时也证明了认证在每一行上都成功了。

以行号作为 id

这些格式中的行没有名称，因此 id 为 op:LINE（或 sqrt:LINE、pow:LINE）。只要固定的文件不变，它们就是稳定的，而 testdata/bin_float/corpora.json 中的 SHA-256 固定值保证了这一点。

正确性 / 不变式

通过的可靠性。 若 MPFR 的 $y$ 是 $f(x)$ 的正确舍入值（MPFR 保证这一点），则通过的平方根行或幂运算行精确地表明 $\hat y = \circ_{p,\rho}(f(x))$，而通过的初等函数行表明同样的结论（除零的符号和 NaN 载荷外），并且标志与声明一致。

计数恒等式。 每个解析出的行都会被执行，因此 $\text{total} = \text{passed} + \text{failed}$，且解析出的行数等于 total_cases。

确定性。 每行的结果只依赖于该行本身。

解析的完全性。 每个非注释行都会成为一行数据或一条诊断，且仅当没有任何诊断时才返回文档。

已知的中止。 若 pow、hypot 或 atan2 的初等函数行的第二个操作数为 -，该行能通过解析器，但会在执行时中止（执行器对缺失的操作数调用了 unwrap）。

被否决的替代方案

• 比较十进制字符串。 十进制输出需要其自身的正确舍入转换；而十六进制有效数字可以精确比较。
• 在 IEEE 格式中运行。 这会混淆范围效应与舍入效应，并使大多数高精度行（精度 113 及以上）无法执行。
• 在测试时链接 MPFR。 数据由小型 C 程序一次性生成并固定，因此 MoonBit 测试运行无需任何 C 依赖，可在所有目标上运行。

边界

• 平方根行只检查值，不检查标志。
• 初等函数行不检查零结果的符号或 NaN 载荷。
• 不涉及指数范围、次正规数或上溢处理。
• 只支持上述三种格式；不存在通用的 MPFR 测试文件读取器。
• 文件读取、格式检测和退出码位于 cli/mpfr_expr_cli 中。

Footnotes

1. L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, P. Zimmermann, “MPFR: A multiple-precision binary floating-point library with correct rounding”, ACM TOMS 33(2), 2007. ↩

2. IEEE 754-2019，第 7.2 条（无效运算）和第 7.3 条（除以零），以及关于推荐初等函数的第 9.2 条。 ↩