bin_float 一致性说明
本文记录 0.8.0 二进制浮点语义与验证边界。有限测试全部通过是声明范围内的证据，不是对所有实数输入的形式化证明。
标准、论文与参考实现
- IEEE 754-2019：interchange format、舍入方向、带符号零、NaN、异常标志与 before/after rounding 的 tininess 语义。
- Fousse、Hanrot、Lefèvre、Pélissier、Zimmermann， MPFR: A Multiple-Precision Binary Floating-Point Library with Correct Rounding， ACM TOMS 33(2), 2007：任意精度的“精确结果、仅一次舍入”模型。
- John Hauser 的 Berkeley SoftFloat 与 TestFloat（release 3e）提供了独立生成的 IEEE 结果/标志向量。
数学语义与算法
有限非零的 BinFloat 表示二进有理实数
(-1)^negative * coefficient * 2^exponent2，其中 coefficient 是非负的 BinCoeff。
有限系数通过去除因子 2 来规范化，同时零的符号仍然可观察。无穷、qNaN、sNaN、NaN 载荷和 NaN 符号都是显式状态，而非以哨兵有限值表示。
add_ctx、sub_ctx、mul_ctx、div_ctx、sqrt_ctx 与 pow_int_ctx 的顺序固定为：先处理 IEEE 特殊值；在 dyadic/有理数或平方根界上计算精确数学结果；按目标精度和方向仅舍入一次；最后做指数范围/subnormal 量化，并从该过程导出五个 IEEE 标志。实现不会根据测试 ID、测试数值或向量格式选择分支。
- IEEE 特殊情形在有限算术之前处理。
- 有限值的加法、减法和乘法使用其精确的二进有理结果；除法使用精确的整数商/余数判定；平方根使用精确的整数平方根，并与舍入中点做精确比较；整数幂对定向包络进行认证（Ziv 循环），认证不成功时回退到精确幂。
- 精确结果按所请求的精度和舍入方向只舍入一次，随后再施加指数范围/次正规数量化。
- 返回的
BinaryFlags由该数学结果推导而来：不精确、下溢、上溢、除以零和无效运算。
例如 binary16 0x0400 * 0x3BFF 的结果位为 0x0400，标志仍为 inexact | underflow。after-rounding tininess 依据目标精度、无界指数的舍入结果，而不能由最终 normal 编码倒推。
没有任何运算会根据测试标识符、测试值或语料格式进行分支。语料解释器是包裹公开上下文运算的适配器。
固定语料与结果
BinaryInterchange 解码和编码 IEEE binary16、binary32、binary64 和 binary128 位模式。BinaryContext 携带精度、舍入方向、成对的指数界限以及舍入前/舍入后的微小性（tininess）检测方式。编码与上下文算术都返回状态标志；普通运算符使用无界的就近舍入（偶数优先）上下文，并有意不暴露这些标志。
TestFloat 适配器中的 NaN 比较仅在期望结果为 NaN 时才按类别进行。这并非弱化了有限值的比较：非 NaN 的编码位和所有异常位都必须完全一致。这反映了 IEEE 允许自行选择新生成 NaN 载荷的规定。实现本身会保留所选输入 NaN 的符号/载荷，并将信号 NaN 静默化。
声明的语料与结果
完整门禁定义见 testdata/bin_float/README.md。
| 来源 | 范围 | 结果 |
|---|---|---|
| TestFloat 3e level 1、seed 1 | 4 格式 × 5 个算术运算 × 5 舍入 × 2 tininess | 7,461,360 / 7,461,360 |
| TestFloat 3e level 1、seed 1 | 4 格式 × mulAdd（5 舍入 × 2 tininess）、rem、roundToInt 与四种整数转换（5 舍入 × exact/非 exact）、六个比较谓词 | 246,766,512 / 246,766,512 |
MPFR 4.2.2 tests/data/sqrt | 全部可执行十六进制 sqrt 行 | 1,055 / 1,055 |
MPFR 4.2.2 pow_si 固定语料 | 4 种精度 × 5 种受支持舍入 × 6 组输入 | 120 / 120 |
| MPFR 4.2.2 elementary 固定语料 | 29 运算 × 3 精度 × 6 舍入 × 4 组固定 seed 输入 | 2,088 / 2,088 |
| 可选 MPFR elementary 压力、seed 20260715 | 每个不少于三运算的 family 至少 100,000 例 | 966,744 / 966,744 |
| 提交的 smoke | TestFloat、sqrt、pow_si 与 elementary 见证 | 2,451 / 2,451 |
| TestFloat 3e level 2 | binary16 的全部已声明运算/方向/tininess | 50,205,600 / 50,205,600 |
binary16 的 level-2 结果是额外的流式压力证据，并不代表规模大得多的 binary32/64/128 level-2 套件也已通过。归档、文件及其摘要固定在 testdata/bin_float/corpora.json 中。运行器以经过校验的有界分块流式执行 TestFloat level 2，但 level 2 是可选的压力套件，不计入上述结果声明。966,744 行的 MPFR 运行同样是可选的生成式压力证据；可复现的发布边界仍是按哈希固定的 2,088 行测试数据。
声明边界
证据稳定性
固定矩阵是本版本的证据边界；新增操作必须单独定义语料合同和 oracle，不能从现有通过结果外推。
上述结果覆盖四个 interchange format 在所列舍入/tininess 模式下的 contextual 加、减、乘、除、平方根、融合乘加、remainder、roundToIntegral（普通与 exact）、到有/无符号 32/64 位整数的 convertToInteger（普通与 exact），以及 quiet/signaling 的相等、小于、小于等于谓词；另含 24、53、113 bit、全部六种项目舍入模式下声明的 29 个 elementary 运算。非法整数转换只比较标志：SoftFloat 返回平台相关的哨兵值，而 API 返回 None。不宣称格式间转换、min/max、total order、nextUp/nextDown、scaleB/logB 或十进制字符转换（由包内测试覆盖）的 TestFloat 一致性，也不宣称全部 IEEE 754 操作或全部实数输入的一致性。elementary 生成器通过 MPFR 要求的 mpfr_round_nearest_away_begin/end 协议实现 nearest-away，绝不把明确禁止的 MPFR_RNDNA 值直接传给通用 elementary 函数。
日常运行 just conformance smoke binary；完整固定门禁运行 just gate binary。